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

Towards efficient "knowledge-based" automated theorem proving for non-standard logics

  • Conference paper
  • First Online:
9th International Conference on Automated Deduction (CADE 1988)

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

Included in the following conference series:

Abstract

In this paper we give an introduction to a technique for greatly increasing the efficiency of automated theorem provers for non-standard logics. This technique takes advantage of the fact that while most important non-standard logics do not have finite characteristic models (in the sense that truth tables are a finite characteristic model for classical propositional logic), they do have finite models. These models validate all the theorems of a given logic, though some non-theorems as well. They invalidate the rest of the non-theorems. Hence this technique involves using the models to direct a search by an automated theorem prover for a proof by filtering out or pruning the items of the search space which the models invalidate.

UUCP: {uunet,hplabs,ubc-vision,ukc,mcvax,nttlab}!munnari!arp.anu.oz!xxx [where xxx = mam (McRobbie), rkm (Meyer) or pbt (Thistlewaite)]

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.

8. References

  1. Anderson, A.R. and Belnap, N.D. Jr. Entailment: The Logic of Relevance and Necessity, Vol. 1, Princeton U.P., Princeton, New Jersey, 1975.

    Google Scholar 

  2. Beth, E.W. Formal Methods: An Introduction to Symbolic Logic and to the Study of Effective Operations in Arithmetic and Logic, Reidel, Dordrecht, 1962.

    Google Scholar 

  3. Bibel, W. "Mating in Matrices", Communications of the ACM, 26 (1983), 844–852.

    Article  Google Scholar 

  4. Bledsoe, W.W. "Non-Resolution Theorem Proving", Artificial Intelligence, 9 (1977), 1–35.

    Article  Google Scholar 

  5. Bundy, A. The Computer Modelling of Mathematical Reasoning, Academic Press, London, 1983.

    Google Scholar 

  6. Curry, H.B. Foundations of Mathematical Logic, McGraw-Hill, New York, 1963. (Corrected reprint, Dover, 1977.)

    Google Scholar 

  7. Dummett, M. Elements of Intuitionism, Oxford U.P., Oxford, 1977.

    Google Scholar 

  8. Eisinger, N. "What You Always Wanted to Know About Clause Graph Resolution", 316–336, in Proceedings of the 8th International Conference on Automated Deduction, ed. J. Siekmann, LNCS, Vol. 230, Springer, Berlin, 1986.

    Google Scholar 

  9. Farinas del Cerro, L. and Orlowska, M. (eds.) Automated Reasoning in Non-Classical Logic, Special double issue of Logique et Analyse, 28 (1985), 115–294.

    Google Scholar 

  10. Gabbay, D.M. and Guenthner, F. (eds.) Handbook of Philosophical Logic, Vol. 1, Reidel, Dordrecht, 1983. (Vol.2 was published in 1984 and Vol. 3 in 1985.)

    Google Scholar 

  11. Gallier, J.H. Logic for Computer Science: Foundations of Automatic Theorem Proving, Harper and Row, New York, 1986.

    Google Scholar 

  12. Gelernter, H. Hanson, J.R. and Loveland, D.W. "Empirical Explorations of the Geometry Theorem-Proving Machine", 153–163, Computers and Thought, eds. E. Feigenbaum and J. Feldman, McGraw-Hill, New York, 1963.

    Google Scholar 

  13. Gödel, K. "Zum intuitionistischen Aussagenkalkül", Anzeiger der Akademie der Wissenschaften Wien, mathematisch naturwissenschaftliche Klasse, 69 (1932), 65–66.

    Google Scholar 

  14. Halpern, J.Y. (ed.) Theoretical Aspects of Reasoning About Knowledge: Proceedings of the 1986 Conference, Morgan Kaufmann, Los Altos, California, 1986.

    Google Scholar 

  15. Harrop, R. "Some Structure Results for Propositional Calculus", Journal of Symbolic Logic, 30 (1965), 271–292.

    Google Scholar 

  16. Kleene, S. C. Introduction to Metamathematics, North-Holland, Amsterdam, 1952.

    Google Scholar 

  17. Kowalski, R.E. Logic for Problem Solving, North-Holland, Amsterdam, 1979.

    Google Scholar 

  18. Loveland, D.W. Automated Theorem Proving: A Logical Basis, North-Holland, Amsterdam 1978.

    Google Scholar 

  19. McDermott, J. (ed.) IJCAI 87: Proceedings of the Tenth International Joint Conference on Artificial Intelligence, Vols. 1 and 2, Morgan Kaufmann, Los Altos, 1987.

    Google Scholar 

  20. McGovern, G. and McRobbie, M.A. "On an Efficient Computer Implementation of A Decision Procedure for Intuitionistic Logic Using Matrix Models", Manuscript, 1987.

    Google Scholar 

  21. McRobbie, M.A. "What is Relevant Resolution? A Simple Tutorial", Manuscript, 1985. (Presented at the 1985 Conference of the Australasian Association for Logic.)

    Google Scholar 

  22. McRobbie, M.A. and Belnap, N.D. Jr. "Relevant Analytic Tableaux", Studia Logica, 38 (1979), 187–200.

    Article  Google Scholar 

  23. McRobbie, M.A., Meyer, R.K. and Thistlewaite, P.B. "Computer-Aided Investigations into the Decision Problem for Relevant Logics: The Search for a Free Associative Operation", Australian Computer Science Communications, 5 (1982), 236–267. (Proceedings of the 6th Australian Computer Science Conference, ed. L.M. Goldschlager, Basser Department of Computer Science, University of Sydney.)

    Google Scholar 

  24. McRobbie, M.A., Meyer, R.K. and Thistlewaite, P.B. "A Challange", Manuscript, 1987.

    Google Scholar 

  25. McRobbie, M.A., Thistlewaite, P.B. and Meyer, R.K. "A Mechanized Decision Procedure for Non-Classical Logic: The Program Kripke", Bulletin of the Section of Logic, Polish Academy of Sciences, 9 (1980), 189–192.

    Google Scholar 

  26. McRobbie, M.A., Thistlewaite, P.B. and Meyer, R.K. "A Mechanized Decision Procedure for Non-Classical Logic-the Program Kripke", (Abstract), Journal of Symbolic Logic, 47 (1982), 717.

    Google Scholar 

  27. Malkin, P.K. and Martin, E.P. "Logical Matrix Generation and Testing", see these Proceedings.

    Google Scholar 

  28. Nilsson, N.J. Principles of Artificial Intelligence, Springer, Berlin, 1980.

    Google Scholar 

  29. Prawitz, D. Natural Deduction: A Proof Theoretic Study, Almqvist and Wiksell, Stockholm 1985.

    Google Scholar 

  30. Rasiowa, H. and Sikorski, R. The Mathematics of Metamathematics, Polish Scientific Publishers (PWN), Warsaw, 1963. (3rd Edition, 1970.)

    Google Scholar 

  31. Reiter, R. "A Semantically Guided Deductive System for Automated Theorem Proving", IEEE Transactions on Computers, C-25 (1976), 328–334.

    Google Scholar 

  32. Rescher, N. Many-Valued Logic, McGraw-Hill, New York, 1969.

    Google Scholar 

  33. Routley, R. and Wolf, R.G. "No Rational Logic Has a Finite Characteristic Matrix", Logique et Analyse, 17 (1974), 317–321.

    Google Scholar 

  34. Sandford, M.M. Using Sophisticated Models in Resolution Theorem Proving, LNCS, Vol. 90, Springer, Berlin, 1980.

    Google Scholar 

  35. Schütte, K. Proof Theory, trans. J. Crossley, Springer, Berlin, 1977.

    Google Scholar 

  36. Siekmann, J. "Geschichte und Anwendungen", in Deduktionssysteme: Automatisierung des logischen Denken, eds. K.H. Bläsius and H.-J. Bürckert, Oldenbourg, Munich and Vienna, 1987.

    Google Scholar 

  37. Slaney, J.K. Computers and Relevant Logics: A Project in Computing Matrix Model Structures for Propositional Logics, Ph.D. Thesis, Australian National University, 1980.

    Google Scholar 

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

    Google Scholar 

  39. Thistlewaite, P.B., McRobbie, M.A. and Meyer, R.K. "The Kripke Automated Theorem Proving System", 705–706 in Proceedings of the 8th International Conference on Automated Deduction, ed J. Siekmann, LNCS, Vol. 230, Springer, Berlin, 1987.

    Google Scholar 

  40. Thistlewaite, P.B, McRobbie, M.A. and Meyer, R.K. Automated Theorem Proving in Non-Classical Logic, Research Notes in Theoretical Computer Science, Pitman, London and Wiley, New York, 1987.

    Google Scholar 

  41. Thistlewaite, P.B., Meyer, R.K. and McRobbie, M.A. "Advanced Theorem Proving for Relevant Logics", Logique et Analyse, 28 (1985), 233–258.

    Google Scholar 

  42. Turner, R. Logics for Artificial Intelligence, Ellis Horwood, Chichester 1984.

    Google Scholar 

  43. Wolf, R.G. "A Survey of Many-Valued Logic", 167–323 in Modern Uses of Multiple-Valued Logic, ed. J.M. Dunn and G. Epstein, Reidel, Dordrecht, 1977.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Automated Reasoning Project, Australian National University, G.P.O. Box 4, 2601, Canberra, A.C.T., Australia

    Michael A. McRobbie, Robert K. Meyer & Paul B. Thistlewaite

Authors
  1. Michael A. McRobbie
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Robert K. Meyer
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Paul B. Thistlewaite
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Ewing Lusk Ross Overbeek

Rights and permissions

Reprints and permissions

Copyright information

© 1988 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

McRobbie, M.A., Meyer, R.K., Thistlewaite, P.B. (1988). Towards efficient "knowledge-based" automated theorem proving for non-standard logics. In: Lusk, E., Overbeek, R. (eds) 9th International Conference on Automated Deduction. CADE 1988. Lecture Notes in Computer Science, vol 310. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0012833

Download citation

  • DOI: https://doi.org/10.1007/BFb0012833

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-19343-2

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation