[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

PTTP+GLiDeS: Guiding Linear Deductions with Semantics

  • Conference paper
Advanced Topics in Artificial Intelligence (AI 1999)

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

Included in the following conference series:

  • 1289 Accesses

Abstract

Using semantics to guide automated theorem proving systems is an under-utilised technique. In linear deduction, semantic guidance has received only limited attention. This research is developing semantic guidance for linear deduction in the Model Elimination paradigm. Search pruning, at the possible loss of some refutation completeness, and search guidance, are being considered. This paper describes PTTP+GLiDeS, a PTTP style prover augmented with a semantic pruning mechanism, GLiDeS. PTTP+GLiDeS combines a modified version of Stickel’s PTTP prover with the model generator MACE.

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. A. Bundy. The Computer Modelling of Mathematical Reasoning. Academic Press, 1983.

    Google Scholar 

  2. H. Chu. CLIN-S User’s Manual. Chapel Hill, USA, 1994.

    Google Scholar 

  3. D.A. de Waal and J.P. Gallagher. The Applicability of Logic Programming Analysis and Transformation to Theorem Proving. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, number 814 in Lecture Notes in Artificial Intelligence, pages 207–221. Springer-Verlag, 1994.

    Google Scholar 

  4. D.W. Loveland. Mechanical Theorem Proving by Model Elimination. Journal of the ACM, 15(2):236–251, 1968.

    Article  Google Scholar 

  5. D.W. Loveland. A Linear Format for Resolution. In Laudet M. et al., editor, Proceedings of the IRIA Symposium on Automatic Demonstration, pages 147–162. Springer-Verlag, 1970.

    Google Scholar 

  6. D. Luckham. Some Tree-paring Strategies for Theorem Proving. Machine Intelligence, 3:95–112, 1968.

    Google Scholar 

  7. D. Luckham. Refinement Theorems in Resolution Theory. In Laudet M. et al., editor, Proceedings of the Symposium on Automatic Demonstration, pages 163–190. Springer-Verlag, 1970.

    Google Scholar 

  8. W.W. McCune. A Davis-Putnam Program and its Application to Finite First-Order Model Search: Quasigroup Existence Problems. Technical Report Technical Report ANL/MCS-TM-194, Argonne National Laboratory, Argonne, USA, 1994.

    Google Scholar 

  9. J.A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM, 12(1):23–41, January 1965.

    Article  MathSciNet  Google Scholar 

  10. J.R. Slagle. Automatic Theorem Proving with Renamable and Sematic Resolution. Journal of the ACM, 14:687–697, October 1967.

    Article  Google Scholar 

  11. J.K. Slaney. SCOTT: A Model-Guided Theorem Prover. In R. Bajcsy, editor, Proceedings of the 13th International Conference on Artificial Intelligence, pages 109–114. Morgan-Kaufman, 1993.

    Google Scholar 

  12. M.E. Stickel. A Prolog Technology Theorem Prover. In Proceedings of the 1st International Symposium on Logic Programming, pages 211–217. IEEE Computer Society Press, 1984.

    Google Scholar 

  13. M.E. Stickel. A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog. Technical Report Technical Note 464, SRI International, Menlo Park, USA, 1989.

    Google Scholar 

  14. G. Sutcliffe. Linear-Input Subset Analysis. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction, number 607 in Lecture Notes in Artifical Intelligence, pages 268–280, Saratoga Springs, NY, USA, June 1992. Springer-Verlag.

    Google Scholar 

  15. G. Sutcliffe and C.B. Suttner. The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning, 21(2):177–203, 1998.

    Article  MathSciNet  Google Scholar 

  16. L. Wos. Automated Reasoning-33 Basic Research Problems. Prentice-Hall, 1988.

    Google Scholar 

  17. L. Wos, D. Carson, and G.A. Robinson. The Unit Preference Strategy in Theorem Proving. In Proceedings of the AFIPS 1964 Fall Joint Computer Conference, pages 615–621. Spartan Books, 1964.

    Google Scholar 

  18. L. Wos, R. Overbeek, E. Lusk, and J. Boyle. Automated Reasoning Introduction and Applications. Prentice-Hall, Englewood Cliffs, New Jersey, 1984.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science, James Cook University, Australia

    Marianne Brown & Geoff Sutcliffe

Authors
  1. Marianne Brown
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Geoff Sutcliffe
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computer Science and Engineering, University of New South Wales, Sydney, NSW, 2052, Australia

    Norman Foo

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Brown, M., Sutcliffe, G. (1999). PTTP+GLiDeS: Guiding Linear Deductions with Semantics. In: Foo, N. (eds) Advanced Topics in Artificial Intelligence. AI 1999. Lecture Notes in Computer Science(), vol 1747. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46695-9_21

Download citation

  • DOI: https://doi.org/10.1007/3-540-46695-9_21

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66822-0

  • Online ISBN: 978-3-540-46695-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation