ileanSeP: An Intuitionistic Sequent Prover

Universität Potsdam

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.


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 source code of ileanSeP is available for ECLiPSe Prolog, SWI-Prolog and SICStus Prolog; it should run on most other Prolog systems as well. Please contact us if you encounter any problems when downloading or running ileanSeP on your system.

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.

Related Links

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.

Contact Us

Please feel free to contact us if you have any questions about ileanSeP. If you have any suggestions for improvements or if you have done something interesting with ileanSeP, please let us know about it.

Jens Otten · Institut für Informatik · University of Potsdam · 03.03.2008