Accueil

Quelques preuves de logique du premier ordre

Le programme ci-dessous, basé sur un code dû à Kevin Klement, permet de s'exercer à l'application du système déductif du premier ordre. Pour tous les exemples donnés ci-dessous, il s'agit de fournir une preuve étape par étape, en donnant à chaque fois la règle déductive appliquée dans la case à droite (elles sont rappelées ci-contre). Ceci est une version minimaliste: admirez la puissance de ce programme dans toute sa splendeur dans son habitat naturel.

Instructions


Propositions:
(lettres majuscules)
A, B, X, etc.
Négation: ¬ ~ ∼ - −
Cononction ("et"): ∧ ^ & . · *
Disjonction ("ou"): ∨ v
Equivalence: ↔ ≡ <-> <>=
Condition ("implique"): → ⇒ ⊃ -> >
Contradiction: ⊥ XX #

Propriétés des différents boutons:

×= supprime la ligne
|+= ajjoute une ligne sous celle-ci
||+= ajoute une sous-preuve sous cette ligne
<+= ajoute une ligne sous la sous-preuve en cours
<|+= ajoute une nouvelle sous-preuve sous celle-ci

Chaque ligne a également une case où entrer la justification, sous la forme "nom de la règle"+numéro des lignes sur lesquelles elle est appliquée; par ex “&I 1,2”.

Quelques preuves à tester: