## ileanSeP: An Intuitionistic Sequent Prover What is ileanSeP? · Documentation · Source Code · Related Links · Contact Us Potsdam University Computer Science Theoretical CS
 What is ileanSeP?

ileanSeP is a Prolog program that implements a very compact theorem prover for first-order intuitionistic logic. It is based on a single-succedent intuitionistic sequent calculus very similar to Gentzen's LJ. Using an analytic proof search, free variables and skolemization ensures good performance. Inference rules are defined in a modular way which makes modifications to the calculus easily possible.

Features of ileanSeP

• Theorem prover for intuitionistic first-order logic.
• Based on an intuitionistic sequent calculus using free term-variables and skolemization.
• Sound and complete.
• Decision procedure for the fragment where negation occurs only positively and which contains only existential quantified variables.
• Source code available for popular Prolog systems, including ECLiPSe Prolog, SWI-Prolog and SICStus Prolog.
• Simple first-order form input format.

 Documentation

The following paper provides details about the implemented sequent calculus and the source code of ileanSeP.

• Jens Otten.
ileanSeP: An Intuitionistic Sequent Theorem Prover.
Technical Report. To appear.

 Source Code

The ileanSeP prover is invoked with  prove(F).  where  F  is a first-order formula. For example  prove( all X: ex Y:(~q,p(Y) => p(X)) ).  will prove the validity of the given formula. The logical connectives are expressed by "~" (negation), "," (conjunction), ";" (disjunction), "=>" (implication), "<=>" (equivalence); quantifiers are expressed by "all X:" (universal) and "ex X:" (existential). See the documentation for more details about the syntax of first-order formulae.

Here is a selection of links related to ileanSeP.

• ileanTAP - a compact Prolog theorem prover for intuitionistic first-order logic based on analytic tableaux and prefix unification.
• leanTAP - a compact Prolog theorem prover for first-order logic based on analytic tableaux by Bernhard Beckert and Joachim Posegga.
• ModLeanTAP - a compact Prolog theorem prover for modal logics based on analytic tableaux by Bernhard Beckert and Rajeev Goré.
• linTAP - a compact Prolog theorem prover for the multiplicative and exponential fragment of Girard's linear logic.
• leanCoP - a compact Prolog theorem prover for classical-first order logic.
• ncDP - a compact Prolog non-clausal "Davis-Putnam" prover.