ncDP: A Non-Clausal Davis-Putnam Prover

Universität Potsdam

What is ncDP?
 · Documentation
 · Source Code
 · Related Links
 · Contact Us
 
 
 
Potsdam University
Computer Science
Theoretical CS
What is ncDP?

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.

Documentation

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)

Source Code

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.


Related Links

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.

Contact Us

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.


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