Skip to main content
SpringerLink
Log in

An example of FOL using metatheory

Formalizing reasoning systems and introducing derived inference rules

  • Conference paper
  • First Online:
6th Conference on Automated Deduction (CADE 1982)

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

Included in the following conference series:

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.

References

  1. Aiello, L, and Weyhrauch, R., Using meta-theoretic reasoning to do algebra, Proceedings of the 5-th Workshop on Automated Deduction, Springer-Verlag, Lecture Notes in Computer Science, 1980.

    Google Scholar 

  2. Bowen, K.A., and Kowalski, R., Amalgamating Language and Metalanguage in Logic Programming, School of Computer and Information Science, Syracuse University, June 1981.

    Google Scholar 

  3. Boyer, R.S. and Moore, J.S., Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures, SRI International Technical Report CSL-108, December 1979.

    Google Scholar 

  4. Church, A., Introduction to mathematical logic, vol 1, Princeton University Press, Princeton, 1956.

    Google Scholar 

  5. Gordon, M.J., Milner, A.J., and Wadsworth, C.P., Edinburgh LCF: A Mechanized Logic of Computation, Springer-Verlag, Lecture Notes in Computer Science 78.

    Google Scholar 

  6. Kleene, S. C., Introduction to metamathematics, Van Nostrand, New York and Toronto, 1952.

    Google Scholar 

  7. Konolige, K., A metalanguage representation of relational databases for deductive question-answering systems, in Proceedings of the 7-th IJCAI, 1981.

    Google Scholar 

  8. McCarthy, J. and Hayes, P.J., Some Philosophical Problems from the Viewpoint of Artificial Intelligence, in (D.Michie, ed.) Machine Intelligence, 7, Edinburgh U.P., Edinburgh, 1969.

    Google Scholar 

  9. see Weyhrauch [1980]: Prolegomena to a theory of mechanized formal reasoning, Artificial Intelligence, 13, 1980, pp.133–170.

    Article  Google Scholar 

  10. Talcott, C, and Weyhrauch, R., Reasoning about actions, in preparation.

    Google Scholar 

  11. Weyhrauch, R., FOL: A Proof Checker for First-order Logic, Stanford Artificial Intelligence Laboratory Memo AIM-235.1, Stanford University, Stanford, 1977.

    Google Scholar 

  12. Weyhrauch, R., Prolegomena to a theory of mechanized formal reasoning, Artificial Intelligence, 13, 1980, pp.133–170.

    Article  Google Scholar 

  13. Weyhrauch, R., A Mechanizable Formulation of Logic, in preparation.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Stanford University, 94305, Stanford, CA

    Richard W. Weyhrauch

Authors
  1. Richard W. Weyhrauch
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

D. W. Loveland

Rights and permissions

Reprints and permissions

Copyright information

© 1982 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Weyhrauch, R.W. (1982). An example of FOL using metatheory. In: Loveland, D.W. (eds) 6th Conference on Automated Deduction. CADE 1982. Lecture Notes in Computer Science, vol 138. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0000057

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-39240-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation