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