Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
STRIP Version 1.0

STRIP Version 1.0

Equipe TYPES, LORIA

Authors: Dominique Larchey, Daniel Mery and Didier Galmiche.

License: GPL.

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.

If you have any question, please contact Dominique Larchey by email: larchey@loria.fr.

Installation

STRIP is distributed under the GNU GPL. See the file COPYING.

create a directory, eg STRIP and cd to it.
Download the .tar.gz archive and untar.
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.

Help

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]

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

Examples:

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