A simple experimental proof assistant, made for academic purposes. It is based on sequent calculus LK system. And is supposed to work on boolean propositions, as well as natural numbers.
proof <name> <formula>
<rule 1>
.
.
.
<rule n>
name can contain a-z letters, numbers as well as - and _
The syntax of formulas is as follow:
-Variable names : A-Z
-And : ^
-Or : v
-Imp : ->
-Not : -| or ¬
Parenthesis are usable in formula names
There are a few rules available. In order to make things more readable, the permutation is not implemented, you can instead act on the i-th element of the left or right side of a sequent as you wish:
-Axiom : axiom
-Left/Right Weakening i : wl i / wr i
-Left/Right Contraction i : cl i /cr i
-Left/Right Not i : notl i or ¬l i / notr i or ¬r i
-Left/Right Ant i : ^l i / ^r i
-Left/Right Or i : vl i / vr i
-Left/Right Imply i : ->l i / ->r i
-Reduction i j : reduc i j (if A is present on both sides, it makes all the weakenings/contractions in one go)
-Extern : ext <name> with <name> being the name of a previously saved, already proved proposition
If you want to simply verify if a proposition is correct, you can simply write proof <name> <formula> in a file, and check it using pr_assistant <dir> in your shell, with <dir> being the directory in which the formula is written.
Otherwise, if you want to also check if your own sequence of rules work, you can add -m true in the command
Let's try to verify if the following property is true : ((A -> B) ^ ¬B) -> ¬A
This property is refered to as the Modus Tollens, let's write in a certain file called modus_tollens the following:
proof modus_tollens ((A -> B) ^ ¬B) -> ¬A
by running pr_assistant modus_ponens, we get the following result:
tentative de résolution automatique de la propriété:
(((A)->(B))^(¬(B)))->(¬(A))
----------<- reduc 0 0
B,A ├ B
---------- ----------<- reduc 0 1
B,A ├ B A ├ B,A
-----------------<- ->gauche 0
(A)->(B),A ├ B
----------------------<- ┐gauche 1
(A)->(B),¬(B),A ├
--------------------------<- ^gauche 0
((A)->(B))^(¬(B)),A ├
-----------------------------<- ┐droite 0
((A)->(B))^(¬(B)) ├ ¬(A)
-----------------------------------<- ->droite 0
├ (((A)->(B))^(¬(B)))->(¬(A))
Propriété "modus_tollens" ajoutée au répertoire avec succès !
formule modus_tollens correcte et ajouté au registre
The text is currently in french, sorry about that.
The command will also display the tactics used to reduce the first expression.
The proposition being right, it was saved and can now be used again for further proofs using ext modus_tollens