STRIP is an automated theorem (ATP) prover designed for proof search and counter-model generation for Propositional Intuitionistic Logic. It is implemented in C language and has a basic user interface.
It was designed to show the efficiency of new algorithms for proof search based on efficient resource management.
D. Galmiche and D. Larchey-Wendling. "Structural sharing and efficient proof-search in propositional intuitionistic logic." In Asian Computing Science Conference, ASIAN'99, LNCS 1742.
It can be compared to other ATPs like ft or Porgi. It is usually much more efficient than both of these.
If you have any question, please contact Dominique Larchey by email: larchey@loria.fr.
Now you can interact with the system. First use the help command:
help.
This prints the short help text also provided in the next section.
Propositionnal constants: ff, falsum, tt (for true).
Propositionnal variables: A1, p3(x,y) ...
Logical connectives:
| # | (unary not) | right associative | highest precedence |
| & | (and) | right associative | | strictly |
| | | (or) | right associative | | decreasing |
| -> | (implication) | right associative | \|/ |
| <-> | (biimplication) | right associative | lowest precedence |
Formulae are built up using basic syntactic units described in section I plus parentheses and whitespace.
Examples:
Sequents are made of two parts separated by ";". The first part is called the antecedent and is a multiset of formulae, each of them separated by a ",". The antecedent may be empty. The second part is called the succedent (or the conclusion) and is made of a single formula.
Examples:
Commands must be separated from each other by "." or "\". In the following, square brackets [] are used to introduce an optional syntactic unit (or optional argument). Note: the prover is case sensitive.