# STRIP Version 1.0

## Description

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.

## Installation

• create a directory, eg STRIP and cd to it.
• make

## Usage

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

# Basic syntactic units

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 and sequents

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

# Prover commands

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
use [method]
• firstleaf: set first-encountered-leaf as the current search-method
• ruleprec : set rule-precedence as the current search-method (default)
[print]