Documentation
Principe
Dedunat construit une preuve en déduction naturelle de bas
en haut. On part du séquent à prouver, par exemple ⊢ (A ∧ B) → (B ∧ A),
puis on applique des règles. Chaque règle remplace le but courant
(encadré dans l'arbre, en tête de la liste des buts) par zéro, un ou
plusieurs sous-buts. Quand il ne reste plus aucun but, la preuve est
complète : Qed la valide. Elle reste alors affichée et
exportable jusqu'à ce qu'on tape une nouvelle formule.
- Tapez une formule (ou
Prove formule) dans la console, ou choisissez un exemple.
- Appliquez des règles avec les boutons ou en tapant les commandes ci-dessous.
Undo annule la dernière étape ; Auto applique l'introduction évidente.Qed valide, puis Print, LaTeX ou Français exportent la preuve.
Écrire des formules
| Connecteur | Unicode | ASCII | LaTeX |
|---|
| Implication | → | -> | \to |
| Conjonction | ∧ | /\ | \land |
| Disjonction | ∨ | \/ | \lor |
| Négation | ¬ | ~ | \neg |
| Absurde | ⟂ | _|_ | \bot |
| Pour tout | ∀x. … | \-/x. … | \forall x. … |
| Il existe | ∃x. … | -]x. … | \exists x. … |
| Thèse (séquent) | ⊢ | |- | \vdash |
- Variables propositionnelles :
A, B… ;
prédicats et termes : P(x), R(x, f(y)).
- ¬ est prioritaire, puis ∧ et ∨ (même niveau, associatifs à droite :
A ∧ B ∨ C se lit A ∧ (B ∨ C)), puis → (associatif à droite).
En cas de doute, mettez des parenthèses.
- Un quantificateur porte sur tout ce qui suit :
∀x. P(x) → Q(x)
se lit ∀x. (P(x) → Q(x)).
- Un séquent avec hypothèses s'écrit
A, A → B ⊢ B.
- Les mots-clés ne sont pas sensibles à la casse.
Règles
Γ désigne les hypothèses. Chaque schéma se lit de bas en haut : la
commande transforme le but du bas en les sous-buts du haut. Les
arguments en italique sont à fournir.
Autres commandes
axiom | Ferme le but Γ ⊢ A lorsque A est une hypothèse de Γ (à α-équivalence près). |
auto | Applique l'introduction du connecteur principal du but quand elle ne demande pas d'argument (→, ∧, ¬, ∀). |
classical | Tiers exclu : ferme un but de la forme A ∨ ¬A ou ¬A ∨ A. |
peirce | Loi de Peirce : ferme un but de la forme ((A → B) → A) → A. |
assume | Admet le but courant (noté ! dans l'arbre). |
undo | Annule la dernière commande (y compris Qed). |
qed | Valide la preuve quand il ne reste plus de but. |
print, latex, french | Affichent la preuve (en cours ou dernière validée) en texte, en LaTeX
(paquet bussproofs) ou rédigée en français. |
define R n formule | Définit le prédicat R d'arité n ; ses arguments sont notés
V1, …, Vn dans la formule. Ex. : define Sym 1 ∀y. (R(V1, y) → R(y, V1)). |
unroll | Remplace dans le but courant les prédicats définis par leur définition. |
help, help intro, help elim, help ∧… | Aide en ligne dans la console. |
Exemple
Preuve de (A ∧ B) → (B ∧ A) :
(A ∧ B) → (B ∧ A) ⊢ (A ∧ B) → (B ∧ A)
intro → A ∧ B ⊢ B ∧ A
intro ∧ deux buts : A ∧ B ⊢ B et A ∧ B ⊢ A
elim ∧ right A A ∧ B ⊢ A ∧ B
axiom reste A ∧ B ⊢ A
elim ∧ left B A ∧ B ⊢ A ∧ B
axiom plus de but
qed
Clavier
- Entrée exécute la commande ; ↑ / ↓ parcourent l'historique.
- Tab insère → puis, à chaque nouvel appui, le remplace par ∧, ∨, ¬, ⟂, ∀, ∃.
- Les boutons de règles qui attendent un argument pré-remplissent la console ; complétez puis Entrée.
Limites
Les conditions sur les variables libres des règles ∀i et ∃e ne sont pas
vérifiées : c'est à vous de choisir des variables fraîches.