Concept# First-order logic

Summary

First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.
A theory about a topic, such as set theory, a theory for groups, or a formal theory of arithmetic, is usually a first-order logic together with a specified domain of discourse (over which the quantified variables range), finitely many functions from that domain to itself, finit

Official source

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications

Loading

Related people

Loading

Related units

Loading

Related concepts

Loading

Related courses

Loading

Related lectures

Loading

Related people (12)

Related publications (61)

Loading

Loading

Loading

Related concepts (155)

Mathematical logic

Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research i

Logic

Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or logical truths. It studies how conclusions follo

Propositional calculus

Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions

We present a new second-order method, based on the MAC scheme on cartesian grids, for the numerical simulation of two-dimensional incompressible flows past obstacles. In this approach, the solid boundary is embedded in the cartesian computational mesh. Discretizations of the viscous and convective terms are formulated in the context of finite volume methods ensuring local conservation properties of the scheme. Classical second-order centered schemes are applied in mesh cells which are sufficiently far from the obstacle. In the mesh cells cut by the obstacle, first-order approximations are proposed. The resulting linear system is nonsymmetric but the stencil remains local as in the classical MAC scheme on cartesian grids. The linear systems are solved by a fast direct method based on the capacitance matrix method. The time integration is achieved with a second-order projection scheme. While in cut-cells the scheme is locally first-order, a global second-order accuracy is recovered. This property is assessed by computing analytical solutions for a Taylor-Couette problem. The efficiency and robustness of the method is supported by numerical simulations of 2D flows past a circular cylinder at Reynolds number up to 9500. Good agreement with experimental and published numerical results are obtained. (c) 2012 Elsevier Ltd. All rights reserved.

The electrical discharge machining process (EDM) was discovered in the 1950s, and was then used essentially to destroy unrecoverable damaged screws. Since then, huge progress has been achieved in making this process reliable and able to perform the most complex machining operations on the most sophisticated materials. Two main processes use electrical discharge machining. First, Die Sinking EDM (DSEDM) in which an electrode, moved along a usually vertical axis, makes an imprint into a mechanical element ; second, Wire EDM (WEDM), uses a wire as an electrode and makes it possible to perform cut operations. Two specific aspects of the EDM process make it particularly challenging for optimization. First, the process evolves with the machining position. In the DSEDM process, where the electrode sinks deeply into the material, the fragments spawn by erosion (contamination) are trapped, thus modifying the sparking conditions. In the WEDM process, the main factors that drive the evolution of the process are the machining operations. Second, the measurements are very noisy, which is due to underlying, mainly random, physical phenomenon ; this is particularly true to spark triggering. The process evolution influences the single criterion to be minimized : total machining time. However, the latter is only known once the operations are completed. As a result, the whole history of manipulated variables influences the final criterion to minimize in this case of dynamic optimization. A major contribution of this work is a proof that a first-order model of the DSEDM process, with the machining position as a state variable, makes it possible to transform a dynamic optimization problem into a static optimization problem. The tools used in this demonstration are Pontryagin's Minimum Principle as well as Parametric Programming. The conclusion is that in order to achieve minimum machining time, maximum speed must be sought all along the trajectory. The online search for maximum speed is another important contribution of this thesis. Noisy efficiency functions are, indeed, known to be a significant challenge to the reliability of optimization algorithms. To address this issue the Golden Ratio Search and the Nelder-Mead Simplex algorithms were chosen as the starting point, as they do not rely explicitly on the gradient of the efficiency function. The addition of a further dilation condition makes these algorithms more effective in stochastic mode. This condition is based on the detection of contradictory measurement samples as compared to the shape of the efficiency function, which is assumed to be unimodal. As a result of this modification, the density of the final optimization points is well centred relative to the theoretical optimum, and dispersion is small. Moreover, the size of the search region for both algorithms never approaches zero. Consequently, as the machining conditions evolve, the optimizer can target a new optimum. This adaptability proves to be a significant improvement over existing algorithms. In the case of the DSEDM process, a simple model of the efficiency surface as a function of the control variables, which has been calibrated on sample measures, has allowed for a validation of the static optimization. For the WEDM process, conclusive results for the modified algorithms have been obtained both by simulation and during machine-based tests.

Related courses (56)

EE-110: Logic systems (for MT)

Ce cours couvre les fondements des systèmes numériques. Sur la base d'algèbre Booléenne et de circuitscombinatoires et séquentiels incluant les machines d'états finis, les methodes d'analyse et de synthèse de systèmelogiques sont étudiées et appliquée

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and the practice behind them.

CS-101: Advanced information, computation, communication I

Discrete mathematics is a discipline with applications to almost all areas of study. It provides a set of indispensable tools to computer science in particular. This course reviews (familiar) topics as diverse as mathematical reasoning, combinatorics, discrete structures & algorithmic thinking.

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we make progress towards a better verification experience in general-purpose programming languages by contributing improvements both to the automated checking and the specification of safety properties in languages combining functional and imperative features. We present our extensions in two parts -- reasoning about shared mutable data, and types as specifications -- both of which ultimately rely on reductions of expressive surface languages to a functional core. Throughout, we instantiate our techniques for the particular example of Scala, a mixed-paradigm language widely-used in industry.The first part shows how to extend a verifier for higher-order functions and immutable data to support imperative programs with shared mutable data. We build upon Stainless, a contract-based verification system that relies on SMT solvers to automatically verify a large fragment of Scala. Our technique extends Stainless to check general heap-manipulating programs against modular specifications in the style of dynamic frames. A novelty of our approach is the translation of imperative function contracts that encodes frame conditions using quantifier-free formulas in first-order logic, instead of relying on quantifiers or on dedicated separation logic reasoning. Our quantifier-free encoding enables SMT solvers to both prove safety and to report counterexamples relative to the semantics of procedure contracts.In the second part we turn to types and type-level programming as an alternative means of specifying correctness properties. While dependent types have been studied extensively for purely-functional languages, we investigate their applications to languages with subtyping and (abstractions of) imperative features. We first study a calculus that provides type-level computation through singleton types and allows abstraction of state and IO through a non-deterministic choice operator. This allows for modelling interactions with existing imprecisely-typed and impure code. Our calculus is formalized and mechanically proven correct using the Coq proof assistant. In addition, we develop a prototypical implementation in the Scala compiler and study typical type-level programming use cases in the Scala ecosystem.

Related lectures (135)

Related units (6)