Advertisement

A Portable Environment for Research in Automated Reasoning

  • Ewing L. Lusk
  • Ross A. Overbeek
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)

Abstract

The Interactive Theorem Prover (ITP), an environment that supports research into the theory and application of automated reasoning, is described. ITP is an interactive system providing convenient access to and control of the many inference mechanisms of Logic Machine Architecture (LMA), described elsewhere, LMA itself has been substantially enhanced since the last report on its status, and we describe here some of the enhancements, particularly the addition of a tightly-coupled logic programming component, which provides an integration of the theorem-proving and logic programming approaches to problems represented in the predicate calculus.

Keywords

Inference Rule Logic Programming Automate Reasoning Reasoning System Inference Mechanism 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    W. F. Clocksin and C. S. Mellish, Programming in Prolog, Springer-Verlag, New York (1981).zbMATHGoogle Scholar
  2. 2.
    E. Lusk, William McCune, and R. Overbeek, “Logic Machine Architecture: inference mechanisms,” pp. 85–108 in Proceedings of the Sixth Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, Vol. 138, ed. D. W. Loveland,Springer-Verlag, New York ().Google Scholar
  3. 3.
    E. Lusk and R. Overbeek, “Data structures and control architecture for the implementation of theorem-proving programs,” in Proceedings of the Fifth Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, Vol. 87, ed. Robert Kowalski and Wolfgang Bibel, ().Google Scholar
  4. 4.
    E. Lusk, William McCune, and R. Overbeek, “Logic machine architecture: kernel functions,” pp. 70–84 in Proceedings of the Sixth Conference on Automated Deduction, Springer-verlag Lecture. Notes in Computer Science, vol. 138, ed. D. W. Loveland,Springer-Vertag, New York (1982).Google Scholar
  5. 5.
    Ewing L. Lusk and Ross A. Overbeek, “An LMA-based theorem prover,” ANL-82-75, Argonne National Laboratory (December, 1982).Google Scholar
  6. 6.
    Ewing L. Lusk and Ross A. Overbeek, “Logic Machine Architecture inference mechanisms — layer 2 user reference manual,” ANL-82-84, Argonne National Laboratory (December, 1982).Google Scholar
  7. 7.
    J. McCharen, R. Overbeek, and L. Wos, “Complexity and related enhancements for automated theorem-proving programs,” Camputers and Mathematics with Applications 2 pp, 1–16 (1976).zbMATHGoogle Scholar
  8. 8.
    S. Winker and L. Wos, “Procedure implementation through demodulation and related tricks,” pp. 109–131 in Proceedings of the Sixth Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, Vol. 138, ed. D. W. Loveland,Springer-Verlag, New York (1982).Google Scholar
  9. 9.
    L. Wos, G. Robinson, D. Carson, and L. Shalla, “The concept of demodulation in theorem proving,” Journal of the ACM 14 pp, 698–704 (1967).CrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Ewing L. Lusk
    • 1
  • Ross A. Overbeek
    • 1
  1. 1.Mathematics and Computer Science DivisionArgonne National LaboratoryArgonne

Personalised recommendations