Didier Galmiche, Brandon Hornbeck and Daniel Méry.
License: GPL.AutoPSI is an automated theorem (ATP) prover designed for proof search in the Intuitionistic Sentential Calculus with Identity (ISCI). It is implemented in Java 17 language and has a basic user interface.
It implements the L2 labeled calculus described in:
Didier Galmiche, Marta Gawek, and Daniel Méry.
Beth Semantics and Labelled Deduction for Intuitionistic Sentential Calculus with Identity. In 6th International Conference on Formal Structures for Computation and Deduction,
FSCD 2021, LIPIcs 195, page 13:1–13:21, Buenos Aires, Argentina, July 2021.
If you have any question, please contact Daniel Méry by email: Daniel.Mery@loria.fr.
AutoPSI is distributed under the GNU GPL.
You need a working Java 17 runtime environment, as well as a version of ANTLR4 version 4.11 or higher.
You can download the standalone Java archive here.
Once you have downloaded the Java archive:
java -jar ISCIProver.jarNow you can interact with the system.
prove followed by a formula (see the grammar section). The command prove can also prove a file if it is followed by a path to the file in question. It will then prove all formulas in the file, line by line.
You can add another parameter to prove, an integer, being the number of iterations of the proof you want the prover to execute (usefull for benchmarks).
Using the command trace turns on the trace mode. If the mode is on the prover will provide a trace of the proof (a tree of the rules used in the proof) if the formula is true.
Using the command again turns off the trace mode.
Using the command verbose turns on the verbose mode. If the mode is on the prover will provide informations on the proof, such as the depth of the proof, the numbers of nodes created or branches explored.
Using the command again turns off the verbose mode. Sometimes, as in this example, the prover does not count an axiom as a node explored, but it is counted as a node in the proof so that can explain the difference of one node in some examples, where the proof appears to be one node bigger than the exploration.
The command subsumption toggles a flag that activates or deactivates subsumption in the prover. This parameter is activated by default in the prover.
Using the command strategy allows the user to select a strategy between all those available in the prover. The default strategy uses maximility, then you can use the "New Label First" strategy that prioritize rules that create labels, and finally you can use the "First one strategy" that uses formulas in the sequent in left-to-right order (this strategy is not sound, so some valid formulas are unprovable using this basic method).
Using the command again turns off the trace mode.
