|
|
|
|
ncDP is a non-clausal theorem prover for classical propositional logic.
It is a generalization of the well-known
Davis - Putnam - Logemann - Loveland
decision procedure for propositional formulas in clausal form.
By working entirely on the original (non-clausal) formula,
any translation steps to clausal form are avoided. This yields
a compact code and a strong performance.
Features of ncDP
-
Theorem prover for classical propositional logic.
-
Based on a generalized non-clausal Davis-Putnam calculus.
-
Sound and complete.
-
Decision procedure for propositional logic.
-
Source code available for popular
Prolog systems, including ECLiPSe Prolog, SWI-Prolog and
SICStus Prolog.
-
Strong performance.
-
Simple input format.
ncDP is described within a chapter of a book and in a technical report.
-
The book chapter contains a description of the
non-clausal Davis-Putnam calculus and the source code.
Some performance results are presented as well.
W. Bibel, S. Brüning, J. Otten, T. Rath,
T. Schaub.
Compressions and Extensions.
In W. Bibel, P. Schmitt, editors, Automated Deduction -
A Basis for Applications.
Chapter 1.5, Volume 1, Kluwer, 1998.
·
compext_dedu.pdf
(307 kbytes)
-
The technical report also provides some
details about the standard clausal form Davis-Putnam procedure.
Jens Otten
On the Advantage of a Non-Clausal Davis-Putnam Procedure.
Technical Report, AIDA-97-1, TH Darmstadt, Intellektik, 1997.
·
ncdp_aida97.pdf
(202 kbytes)
·
ncdp_aida97.dvi
(52 kbytes)
The source code of ncDP 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 ncDP on your system.
-
The ncDP Prolog program code:
·
ncdp.pl
(ECLiPSe, SWI-Prolog, 3 kbytes)
·
ncdp_sicstus.pl
(SICStus, 3 kbytes)
The ncDP prover is invoked with
prove(F). where F
is a propositional formula. For example
prove( (((~a; ~b),c)=>(c,(a=> ~b))) ).
will prove the validity of the given formula.
The logical connectives are expressed by "~" (negation),
"," (conjunction), ";" (disjunction), "=>"
(implication) and "<=>" (equivalence). See the
documentation for more details about
the syntax of propositional formulas.
-
The minimal version of ncDP is further optimised for
the size of the source code:
·
ncdp_small.pl
(ECLiPSe,SWI-Prolog,SICStus, 449 bytes)
The minimal ncDP version is invoked with dp(M).
where M is a non-clausal (i.e. nested) matrix.
For example dp([[a,b],[-c],[c,[[-a],[-b]]]]).
will prove the validity of the given matrix. See the
documentation for details about
the syntax of a (non-clausal) matrix. This version of ncDP does
not apply the PURE reduction before the actual proof search starts.
Here is a selection of interesting links related to ncDP.
-
leanCoP
- a compact Prolog theorem prover for classical-first order
logic.
-
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é.
-
ileanTAP
- a compact Prolog theorem prover for intuitionistic
first-order logic based on analytic tableaux and
prefix unification.
-
linTAP
- a compact Prolog theorem prover for the multiplicative and
exponential fragment of Girard's linear logic.
Please feel free to contact us if you have any
questions about ncDP. If you have any suggestions for improvements
or if you have done something interesting with ncDP, please
let us know about it.
|
