Skip to main content
SpringerLink
Log in

FDPLL — A First-Order Davis-Putnam-Logeman-Loveland Procedure

  • Conference paper
Automated Deduction - CADE-17 (CADE 2000)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1831))

Included in the following conference series:

Abstract

FDPLL is a directly lifted version of the well-known Davis-Putnam-Logeman-Loveland (DPLL) procedure. While DPLL is based on a splitting rule for case analysis wrt. ground and complementary literals, FDPLL uses a lifted splitting rule, i.e. the case analysis is made wrt. non-ground and complementary literals now.

The motivation for this lifting is to bring together successful first-order techniques like unification and subsumption to the propositionally successful DPLL procedure.

At the heart of the method is a new technique to represent first-order interpretations, where a literal specifies truth values for all its ground instances, unless there is a more specific literal specifying opposite truth values. Based on this idea, the FDPLL calculus is developed and proven as strongly complete.

For a long version of the paper see http://www.uni-koblenz.de/fb4/publikationen/gelbereihe .

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Baumgartner, P.: Hyper Tableaux — The Next Generation. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, p. 60. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  2. Beckert, B.: Integration und Uniformierung von Methoden des tableaubasierten Theorembeweisens. Dissertation, University of Karlsruhe (1998)

    Google Scholar 

  3. Bibel, W., Brüning, S., Otten, J., Schaub, T.: Compressions and Extensions. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction. A Basis for Applications, vol. 1, ch. 5, pp. 133–179. Kluwer Academic Publishers, Dordrecht (1998)

    Google Scholar 

  4. Baumgartner, P., Eisinger, N., Furbach, U.: A confluent connection calculus. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 329–343. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  5. Baumgartner, P., Furbach, U., Niemelä, I.: Hyper Tableaux. In: Orłowska, E., Alferes, J.J., Moniz Pereira, L. (eds.) JELIA 1996. LNCS (LNAI), vol. 1126, Springer, Heidelberg (1996)

    Google Scholar 

  6. Billon, J.-P.: The Disconnection Method. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS (LNAI), vol. 1071, pp. 110–126. Springer, Heidelberg (1996)

    Google Scholar 

  7. Crawford, J.M., Auton, L.D.: Experimental results on the crossover point in random 3sat. Artificial Intelligence 81 (1996)

    Google Scholar 

  8. Chang, C., Lee, R.: Symbolic logic and Mechanical Theorem Proving. Academic Press, London (1973)

    MATH  Google Scholar 

  9. Caferra, R., Peltier, N.: Decision Procedures using Model Building techniques. In: Computer Science logic (CSL 1995) (1995)

    Google Scholar 

  10. Davis, M.: Eliminating the irrelevant from mechanical proofs. In: Proceedings of Symposia in Applied Mathematics - Experimental Arithmetic, High Speed Computing and Mathematics, American Mathematical Society, vol. XV, pp. 15–30 (1963)

    Google Scholar 

  11. Davis, M., Logeman, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM 5(7) (1962)

    Google Scholar 

  12. Davis, M., Putnam, H.: A Computing Procedure for Quantification Theory. Journal of the ACM 7, 201–215 (1960)

    Article  MATH  MathSciNet  Google Scholar 

  13. Eder, E.: Properties of Substitutions and Unifications. Journal of Symbolic Computation 1(1) (March 1985)

    Google Scholar 

  14. Fermüller, C., Leitsch, A.: Model building by resolution. In: Martini, S., Börger, E., Kleine Büning, H., Jäger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol. 702, pp. 134–148. Springer, Heidelberg (1993)

    Google Scholar 

  15. Fermüller, C., Leitsch, A.: Hyperresolution and automated model building. Journal of Logic and Computation 6(2), 173–230 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  16. Gottlob, G., Pichler, R.: Working with Arms: Complexity Results on Atomic Representations of Herbrand Models. In: Proceedings of the 14th Symposium on Logic in Computer Science, IEEE, Los Alamitos (1998)

    Google Scholar 

  17. Lee, S.-J., Plaisted, D.: Eliminating Duplicates with the Hyper-Linking Strategy. Journal of Automated Reasoning 9, 25–42 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  18. Manthey, R., Bry, F.: SATCHMO: a theorem prover implemented in Prolog. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 415–434. Springer, Heidelberg (1988)

    Google Scholar 

  19. Peltier, N.: Pruning the search space and extracting more models in tableaux. Logic Journal of the IGPL 7(2), 217–251 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  20. Plaisted, D.A., Zhu, Y.: Ordered Semantic Hyper Linking. In: Proceedings AAAI 1997 (1997)

    Google Scholar 

  21. Sutcliffe, G., Suttner, C., Yemenis, T.: The TPTP problem library. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol. 814, pp. 192–206. Springer, Heidelberg (1994)

    Google Scholar 

  22. Zhang, H.: SATO: An Efficient Propositional Theorem Prover. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol. 1249, pp. 272–275. Springer, Heidelberg (1997)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Universität Koblenz-Landau, D-56073, Koblenz, Germany

    Peter Baumgartner

Authors
  1. Peter Baumgartner
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Toyota Technological Institute at Chicago, 1427 E. 60th Street, 60637, Chicago, Illinois

    David McAllester

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Baumgartner, P. (2000). FDPLL — A First-Order Davis-Putnam-Logeman-Loveland Procedure. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_16

Download citation

  • DOI: https://doi.org/10.1007/10721959_16

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67664-5

  • Online ISBN: 978-3-540-45101-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation