Skip to main content
SpringerLink
Log in

Model elimination without contrapositives

  • Conference paper
  • First Online:
Book cover Automated Deduction — CADE-12 (CADE 1994)

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

Included in the following conference series:

Abstract

We present modifications of model elimination which do not necessitate the use of contrapositives. These restart model elimination calculi are proven sound and complete. The corresponding proof procedures are evaluated by a number of runtime experiments and they are compared to other well known provers. Finally we relate our results to other calculi, namely the connection method, modified problem reduction format and Near-Horn Prolog.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Anderson and W. Bledsoe. A linear format for resolution with merging and a new technique for establishing completeness. J. of the ACM, 17:525–534, 1970.

    Google Scholar 

  2. Owen L. Astrachan and Mark E. Stickel. Caching and Lemmaizing in Model Elimination Theorem Provers. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction (CADE-11), pages 224–238. Springer-Verlag, June 1992. LNAI 607.

    Google Scholar 

  3. P. Baumgartner. A Model Elimination Calculus with Built-in Theories. In H.-J. Ohlbach, editor, Proceedings of the 16-th German AI-Conference (GWAI-92), pages 30–42. Springer, 1992. LNAI 671.

    Google Scholar 

  4. P. Baumgartner and U. Furbach. Consolution as a Framework for Comparing Calculi. Journal of Symbolic Computation, 16(5), 1993.

    Google Scholar 

  5. P. Baumgartner and U. Furbach. PROTEIN: A PROver with a Theory Extension Interface. In 12th International Conference on Automated Deduction. Springer, 1994. (in this volume).

    Google Scholar 

  6. W. Bibel. Automated Theorem Proving. Vieweg, 2nd edition, 1987.

    Google Scholar 

  7. E. Eder. Consolution and its Relation with Resolution. In Proc. IJCAI '91, 1991.

    Google Scholar 

  8. E. Eder. Relative Complexities of First Order Languages. Vieweg, 1992.

    Google Scholar 

  9. M. Fitting. First-Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer, 1990.

    Google Scholar 

  10. D. M. Gabbay. N-Prolog: An extension of Prolog with hypothetical implication II. logical foundations, and negation as failure. The Journal of Logic Programming, 2(4):251–284, December 1985.

    Google Scholar 

  11. J. Gallier. Logic for Computer Science: Foundations of Automatic Theorem Proving. Wiley, 1987.

    Google Scholar 

  12. R. Letz, K. Mayr, and C. Goller. Controlled Integrations of the Cut Rule into Connection Tableau Calculi. Journal of Automated Reasoning (to appear 1994), 1993.

    Google Scholar 

  13. D. Loveland. Mechanical Theorem Proving by Model Elimination. JACM, 15(2), 1968.

    Google Scholar 

  14. D. Loveland. Near-Horn Prolog and Beyond. Journal of Automated Reasoning, 7:1–26, 1991.

    Google Scholar 

  15. D.W. Loveland and D.W. Reed. A near-horn prolog for compilation. Technical Report CS-1989-14, Duke University, 1989.

    Google Scholar 

  16. R. Letz,J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A High-Performace Theorem Prover. Journal of Automated Reasoning, 8(2), 1992.

    Google Scholar 

  17. L. M. Pereira, L. Caires, and J. Alferes. SLWV — A Theorem Prover for Logic Programming. AI Centre, Uninova, Portugal, July 1991.

    Google Scholar 

  18. D. Plaisted. Non-Horn Clause Logic Programming Without Contrapositives. Journal of Automated Reasoning, 4:287–325, 1988.

    Google Scholar 

  19. D. Plaisted. A Sequent-Style Model Elimination Strategy and a Positive Refinement. Journal of Automated Reasoning, 4(6):389–402, 1990.

    Google Scholar 

  20. D. W. Reed and D. W. Loveland. A Comparison of Three Prolog Extensions. Journal of Logic Programming, 12:25–50, 1992.

    Google Scholar 

  21. G. Sutcliffe, C. Suttner, and T. Yemenis. The TPTP problem library. In Proc. CADE-12. Springer, 1994.

    Google Scholar 

  22. M. Stickel. A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. Journal of Automated Reasoning, 4:353–380, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Universiät Koblenz, Rheinau 1, 56075, Koblenz, Germany

    Peter Baumgartner & Ulrich Furbach

Authors
  1. Peter Baumgartner
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ulrich Furbach
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Alan Bundy

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Baumgartner, P., Furbach, U. (1994). Model elimination without contrapositives. In: Bundy, A. (eds) Automated Deduction — CADE-12. CADE 1994. Lecture Notes in Computer Science, vol 814. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58156-1_7

Download citation

  • DOI: https://doi.org/10.1007/3-540-58156-1_7

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58156-7

  • Online ISBN: 978-3-540-48467-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation