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.

- create a directory, eg STRIP and cd to it.
- Download the .tar.gz archive and untar.
- make

- cd to the STRIP directory
- ./strip

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:

- (A->B) | (B->A)
- ###P->Q
- (Foo & Foobar)<->(#SeRIOus)

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:

- (p->q) ; (#q->#p)
- ; (a|#a)
- (a->b)->c, d->(a->b), d ; c

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**.

- define sequent: define the sequent to work with (current sequent)
- check [sequent]: decide deducibility of the current sequent
- trace [sequent]: output tracing information when checking deducibility
- prove [sequent]: try to build a proof of the current sequent
- refute [sequent]: try to build a counter-model to the current sequent
- solve [sequent]: try to build either a proof or a counter-model
- quit : leave the prover

- firstleaf: set first-encountered-leaf as the current search-method
- ruleprec : set rule-precedence as the current search-method (default)

- help : display this page
- sequent: output the current sequent
- method : output the current search-method
- stat : output statistics about the last search
- proof : output the proof built with command "prove" (if provable)
- kripke : output the counter-model built with "refute" (if unprovable)

- verbose stat : output detailed statistics about the last search
- verbose method: output detailed information about current method
- verbose kripke: output detailed counter-model

- define (p->q) ; (#q->#p) . refute. kripke.
- use ruleprec. check ###a->#a. stat. trace.