Concept
Proof calculus
Concepts associés (13)
Deep inference
Deep inference names a general idea in structural proof theory that breaks with the classical sequent calculus by generalising the notion of structure to permit inference to occur in contexts of high structural complexity. The term deep inference is generally reserved for proof calculi where the structural complexity is unbounded; in this article we will use non-shallow inference to refer to calculi that have structural complexity greater than the sequent calculus, but not unboundedly so, although this is not at present established terminology.
Sequent
In mathematical logic, a sequent is a very general kind of conditional assertion. A sequent may have any number m of condition formulas Ai (called "antecedents") and any number n of asserted formulas Bj (called "succedents" or "consequents"). A sequent is understood to mean that if all of the antecedent conditions are true, then at least one of the consequent formulas is true. This style of conditional assertion is almost always associated with the conceptual framework of sequent calculus.
Logique
La logique — du grec , qui est un terme dérivé de signifiant à la fois « raison », « langage » et « raisonnement » — est, dans une première approche, l'étude de l'inférence, c'est-à-dire des règles formelles que doit respecter toute argumentation correcte. Le terme aurait été utilisé pour la première fois par Xénocrate. La logique antique se décompose d'abord en dialectique et rhétorique. Elle est depuis l'Antiquité l'une des grandes disciplines de la philosophie, avec l'éthique (philosophie morale) et la physique (science de la nature).
Structural proof theory
In mathematical logic, structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof, a kind of proof whose semantic properties are exposed. When all the theorems of a logic formalised in a structural proof theory have analytic proofs, then the proof theory can be used to demonstrate such things as consistency, provide decision procedures, and allow mathematical or computational witnesses to be extracted as counterparts to theorems, the kind of task that is more often given to model theory.
Analytic proof
In mathematics, an analytic proof is a proof of a theorem in analysis that only makes use of methods from analysis, and which does not predominantly make use of algebraic or geometrical methods. The term was first used by Bernard Bolzano, who first provided a non-analytic proof of his intermediate value theorem and then, several years later provided a proof of the theorem that was free from intuitions concerning lines crossing each other at a point, and so he felt happy calling it analytic (Bolzano 1817).
Méthode des tableaux
vignette|200px|Représentation graphique d'un tableau propositionnel partiellement construit En théorie de la démonstration, les tableaux sémantiques sont une méthode de résolution du problème de la décision pour le calcul des propositions et les logiques apparentées, ainsi qu'une méthode de preuve pour la logique du premier ordre. La méthode des tableaux peut également déterminer la satisfiabilité des ensembles finis de formules de diverses logiques. C'est la méthode de preuve la plus populaire pour les logiques modales (Girle 2000).
Calcul des séquents
En logique mathématique et plus précisément en théorie de la démonstration, le calcul des séquents est un système de déduction créé par Gerhard Gentzen. Le nom de ce formalisme fait référence à un style particulier de déduction ; le système original a été adapté à diverses logiques, telles que la logique classique, la logique intuitionniste et la logique linéaire. Un séquent est une suite d'hypothèses suivie d'une suite de conclusions, les deux suites étant usuellement séparées par le symbole (taquet droit), « : » (deux-points) ou encore (flèche droite) dans l'œuvre originale de Gentzen.
Déduction naturelle
En logique mathématique, la déduction naturelle est un système formel où les règles de déduction des démonstrations sont proches des façons naturelles de raisonner. C'est une étape importante de l'histoire de la théorie de la démonstration pour plusieurs raisons : contrairement aux systèmes à la Hilbert fondés sur des listes d'axiomes logiques plus ou moins ad hoc, la déduction naturelle repose sur un principe systématique de symétrie : pour chaque connecteur, on donne une paire de règles duales (introduction/élimination) ; elle a conduit Gentzen à inventer un autre formalisme très important en théorie de la démonstration, encore plus « symétrique » : le calcul des séquents ; elle a permis dans les années 1960 d'identifier la première instance de l'isomorphisme de Curry-Howard.
Système à la Hilbert
En logique, les systèmes à la Hilbert servent à définir les déductions formelles en suivant un modèle proposé par David Hilbert au début du : un grand nombre daxiomes logiques exprimant les principales propriétés de la logique que l'on combine au moyen de quelques règles, notamment la règle de modus ponens, pour dériver de nouveaux théorèmes. Les systèmes à la Hilbert héritent du système défini par Gottlob Frege et constituent les premiers systèmes déductifs, avant l'apparition de la déduction naturelle ou du calcul des séquents, appelés parfois par opposition systèmes à la Gentzen.
Démonstration formelle
Une démonstration formelle est une séquence finie de propositions (appelées formules bien formées dans le cas d'un langage formel) dont chacun est un axiome, une hypothèse, ou résulte des propositions précédentes dans la séquence par une règle d'inférence. La dernière proposition de la séquence est un théorème d'un système formel. La notion de théorème n'est en général pas effective, donc n'existe pas de méthode par laquelle nous pouvons à chaque fois trouver une démonstration d'une proposition donnée ou de déterminer s'il y en a une.