Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Deduction

CADE 1988: 9th International Conference on Automated Deduction pp 685–693Cite as

Logical matrix generation and testing

  • Conference paper
  • First Online:

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

Abstract

Logical matrices are generalisations of truth-tables. They provide powerful computational tools for dealing with inference systems. A matrix in which all of the axioms and rules of a theory are true (or designated) but in which some query statement is false (or undesignated) shows that the query statement cannot be derived from the given theory. In this paper we discuss the use of matrices in logical research and in automated theorem-proving, and we conjecture further uses in the area of general constraint satisfaction. The computational ease of use of matrices is partly overshadowed by the computational difficulty of selecting the best or even a suitable matrix for a given task. Little is known about the relative efficiency of various matrices. We discuss our implementation of a general matrix generate and test algorithm which is designed to assist with research into these questions.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Anderson A.R. and Belnap N.D. Jr. (1975), Entailment: The Logic of Relevance and Necessity, Princeton, Princeton University Press.

    Google Scholar 

  2. Gelernter, H. (1959), Realization of a geometry-theorem proving machine, Proceedings of the International Conference on Information Processing, UNESCO House, pp. 273–282. Reprinted in Siekmann and Wrightson (1983), pp. 99–117.

    Google Scholar 

  3. Jaffar, J. and Lassez, J-L. (1987), Constraint Logic Programming, Proceedings of the Fourteenth ACM Symposium on Principles of Programming Languages, pp.111–119.

    Google Scholar 

  4. Morishita, S., Numao, M. and Hirose, S. (1987), Symbolical construction of truth value domain for logic program, Proceedings of the 4th International Conference on Logic Programming (ed. J-L. Lassez), Cambridge, Mass., MIT Press.

    Google Scholar 

  5. Pritchard, P.A. (1978), And now for Something Completely Different, ms., Australian National University.

    Google Scholar 

  6. Pritchard, P.A. (1979), Son of Something Completely Different, ms., University of Queensland.

    Google Scholar 

  7. Pritchard, P.A. and Meyer, R.K., (1977), On computing matrix models of propositional calculi, ms. ANU.

    Google Scholar 

  8. Siekmann, J. and Wrightson, G. (1983), Automation of Reasoning: Classical Papers on Computational Logic, 2 vols. Springer-Verlag.

    Google Scholar 

  9. Slaney, J.K. (1980), Computers and Relevant Logic: A project in computing matrix model structures for propositional logics, Ph.D. thesis, Australian National University.

    Google Scholar 

  10. Thistlewaite, P.B., McRobbie, M.A., and Meyer, R.K. (1988). Automated Theorem-Proving in Non-Classical Logics, London, Pitman.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Automated Reasoning Project, RSSS, Australian National University, GPO Box 4, 2600, Canberra, ACT, Australia

    Peter K. Malkin & Errol P. Martin

Authors
  1. Peter K. Malkin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Errol P. Martin
    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

Malkin, P.K., Martin, E.P. (1988). Logical matrix generation and testing. 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/BFb0012866

Download citation

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

  • 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