Éditeur d’arbres de preuves

Cet outil permet de réaliser un arbre de preuve de manière interactive. Il supporte actuellement la logique intuitionniste, et la logique classique. Je travaille actuellement sur l’ajout de la logique du 1^er ordre.

Pour utiliser cet outil, il suffit d’entrer un séquent avec le format décrit ci-après. Un séquent s’écrit de la forme « H₁ ; ... ; H_n ⊢ G », où les H_i et G sont des formules. Le caractère ‘⊢’ est un caractère Unicode, mais il peut également être réalisé avec ‘|-.’ Le format d’une formule est donné par ci-dessous.

• Si F = ⊥, on note la formule F comme ‘false,’ ‘_|_’ ou encore ‘⊥.’
• Si F = ⊤, on note la formule F comme ‘true,’ ‘T’ ou encore ‘⊤.’
• Si F = P(x₁,...,x_n) on note la formule F comme ‘P(x₁,..., x_n)’ ou encore ‘P’ si P n’a aucun terme.
• Si F = ¬G, on note la formule F comme ‘not G,’ ‘~G’ ou encore ‘¬G.’
• Si F = G ∧ H, on note la formule F comme ‘G and H,’ ‘G /\ H’ ou encore ‘G ∧ H.’
• Si F = G ∨ H, on note la formule F comme ‘G or H,’ ‘G \/ H’ ou encore ‘G ∨ H.’
• Si F = G → H, on note la formule F comme ‘G => H,’ ‘G -> H’ ou encore ‘G → H.’
• Si F = (∀x, G), on note la formule F comme ‘forall x, G,’ ‘\-/ x, G’ ou encore ‘∀x, G.’
• Si F = (∃x, G), on note la formule F comme ‘exists x, G,’ ‘-] x, G’ ou encore ‘∃x, G.’

Lors de la création de l’arbre de preuve, appliquer certaines règles demande “des arguments.” Ceci est vrai pour la règle →e notamment : on transforme l’objectif H en deux objectifs G → H, et G, il est donc important de préciser quelle formule G choisir.

Ce projet a été réalisé dans le cadre du soutien en informatique en prépa MPI^(⋆|𝜀) par Hugo SALOU. En cas de bug, merci de me contacter via Discord (username : hugos29).