[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Controlling deduction with proof condensation and heuristics

  • Special Deduction Systems
  • Conference paper
  • First Online:
8th International Conference on Automated Deduction (CADE 1986)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 230))

Included in the following conference series:

Abstract

This paper presents a proof condensation (or redundancy elimination) procedure and heuristic rules that are used to enhance the tableau-based theorem prover HARP. The proof condensation procedure makes proofs easier to construct and more readable by excising redundancies from proof trees. Since the entire language of first-order logic is used without preprocessing, heuristics can be formulated to capture efficient and human-like deduction strategies. We also present evidence that the combination of these two techniques enable HARP to solve challenging problems such as Schubert's Steamroller.

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.

Similar content being viewed by others

References

  1. E.W.Beth. The Foundations of Mathematics. North-Holland, 1965.

    Google Scholar 

  2. W. Bibel. "A Comparative Study of Several Proof Procedures". Artificial Intelligence (18, 1982), pp 269–293.

    Article  Google Scholar 

  3. W.W.Bledsoe. The UT Interactive Prover. University of Texas at Austin, ATP-17B, 1983.

    Google Scholar 

  4. D.N. Cohen. Knowledge Based Theorem Proving and Learning. UMI Research Press, Ann Arbor, Michigan, 1981.

    Google Scholar 

  5. A.G.Cohn. "On the solution of Schubert's Steamroller in Many Sorted Logic". IJCAI85, pp 1169–1173.

    Google Scholar 

  6. M.C. Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel, Dordrecht, Holland, 1983.

    Google Scholar 

  7. J.Hintikka. Form and Content in Quantification Theory. Acta Philosophica Fennica 8, 1955.

    Google Scholar 

  8. R.C. Jeffrey. Formal Logic: Its Scope and Limits. McGraw-Hill, New York, 1967.

    Google Scholar 

  9. D. Loveland. Automated Theorem Proving: A Logical Basis. North Holland, New York, 1978.

    Google Scholar 

  10. N.V. Murray. "Completely Non-Clausal Theorem Proving". Artificial Intelligence (18, 1982), pp 67–85.

    Article  Google Scholar 

  11. N.Nilsson. Principles of Artificial Intelligence. Tioga, Palo Alto, 1980.

    Google Scholar 

  12. J.A. Robinson. Logic: Form and Function. North Holland, New York, 1981.

    Google Scholar 

  13. W. Schonfeld. "Prolog extensions based on Tableau Calculus". IJCAI 85, pp 730–732.

    Google Scholar 

  14. R.M. Smullyan. First-Order Logic. Springer Verlag, Berlin, 1968.

    Google Scholar 

  15. W. Stegmuller, M.V. v.Kibed, Strukturtypen der Logik. Springer-Verlag, New York, 1984.

    Google Scholar 

  16. C.Walther. "A many-sorted calculus based on resolution and paramodulation". IJCAI 83, Vol. 2, pp 882–891.

    Google Scholar 

  17. C.Walther. "A mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution". Artificial Intelligence, (May 1985), pp 217–224.

    Google Scholar 

  18. G. Wrightson. Semantic Tableaux, Unification and Links. Technical Report CSD-ANZARP-84-001, 1984, Victoria University, Wellington, New Zealand.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, Carleton University, K1S 5B6, Ottawa, Ontario, Canada

    F. Oppacher & E. Suen

Authors
  1. F. Oppacher
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. E. Suen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jörg H. Siekmann

Rights and permissions

Reprints and permissions

Copyright information

© 1986 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Oppacher, F., Suen, E. (1986). Controlling deduction with proof condensation and heuristics. In: Siekmann, J.H. (eds) 8th International Conference on Automated Deduction. CADE 1986. Lecture Notes in Computer Science, vol 230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16780-3_105

Download citation

  • DOI: https://doi.org/10.1007/3-540-16780-3_105

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-16780-8

  • Online ISBN: 978-3-540-39861-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation