Formule atomiqueEn logique mathématique, une formule atomique ou atome est une formule qui ne contient pas de sous-formules propres. La structure d'une formule atomique dépend de la logique considérée, p. ex. en logique des propositions, les formules atomiques sont les variables propositionnelles. Les atomes sont les formules les plus simples dans un système logique et servent à construire les formules les plus générales.
Isabelle (logiciel)The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring yet supporting explicit proof objects. Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories as well as implementations for code-generation, documentation, and specific support for a variety of formal methods.
Skolem normal formIn mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers. Every first-order formula may be converted into Skolem normal form while not changing its satisfiability via a process called Skolemization (sometimes spelled Skolemnization). The resulting formula is not necessarily equivalent to the original one, but is equisatisfiable with it: it is satisfiable if and only if the original one is satisfiable.
Valuation (logic)In logic and model theory, a valuation can be: In propositional logic, an assignment of truth values to propositional variables, with a corresponding assignment of truth values to all propositional formulas with those variables. In first-order logic and higher-order logics, a structure, (the interpretation) and the corresponding assignment of a truth value to each sentence in the language for that structure (the valuation proper). The interpretation must be a homomorphism, while valuation is simply a function.
Predicate variableIn mathematical logic, a predicate variable is a predicate letter which functions as a "placeholder" for a relation (between terms), but which has not been specifically assigned any particular relation (or meaning). Common symbols for denoting predicate variables include capital roman letters such as , and , or lower case roman letters, e.g., . In first-order logic, they can be more properly called metalinguistic variables.
Boolean-valued functionA Boolean-valued function (sometimes called a predicate or a proposition) is a function of the type f : X → B, where X is an arbitrary set and where B is a Boolean domain, i.e. a generic two-element set, (for example B = {0, 1}), whose elements are interpreted as logical values, for example, 0 = false and 1 = true, i.e., a single bit of information. In the formal sciences, mathematics, mathematical logic, statistics, and their applied disciplines, a Boolean-valued function may also be referred to as a characteristic function, indicator function, predicate, or proposition.
Wilhelm AckermannWilhelm Ackermann (1896-1962) est un mathématicien allemand, célèbre pour la fonction d'Ackermann (1925) qui est un exemple important de la théorie de la calculabilité. Sa thèse (1924) donne une preuve détaillée de la cohérence de l'. Il fut professeur dans le secondaire, à Burgsteinfurt de 1929 à 1948, puis à Lüdenscheid jusqu'à sa retraite en 1961. Il fut membre correspondant de l'Académie des sciences de Göttingen et professeur honoraire de l'université de Münster.
