Skip to main content
SpringerLink
Log in

Using meta-theoretic reasoning to do algebra

  • Tuesday Morning
  • Conference paper
  • First Online:
Book cover 5th Conference on Automated Deduction Les Arcs, France, July 8–11, 1980 (CADE 1980)

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

Included in the following conference series:

Abstract

We report on an experiment in interactive reasoning with FOL. The subject of the reasoning is elementary algebra. The main point of the paper is to show how the use of meta-theoretic knowledge results in improving the quality of the resulting proofs in that, in this environment, they are both easier to find and easier to understand.

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. Evaluating Functions Defined in First Order Logic or In Defense of Semantic Attachment in FOL, Stanford Artificial Intelligence Laboratory Memo, in preparation (1980).

    Google Scholar 

  2. Boyer, R.S. and Moore, J.S. Metafunctions: Proving them correct and using them efflciently as new proof procedures, Computer Science Laboratory, SRI International (1979).

    Google Scholar 

  3. Birkoff, G. and McLane, S. Brief Survey of Modern Algebra, The McMillan Company (1965).

    Google Scholar 

  4. Filman, R.E. The Interaction of Observation and Inference, Ph.D. Thesis, Stanford University, Stanford (1978).

    Google Scholar 

  5. Filman, R.E. Observation and Inference applied in a Formal Representation System, Proc. of the 4-th Workskop on Automated Deduction, Austin, Texas (1979)

    Google Scholar 

  6. Prawitz, D. Natural Deduction — a Proof-Theoretical Study, Almqvist & Wiksell, Stockholm (1965).

    Google Scholar 

  7. Talcott, C. FOLISP: a System for Reasoning about LISP Programs, Stanford Artificial Intelligence Laboratory Memo, in preparation (1980).

    Google Scholar 

  8. Weyhrauch, Richard W. FOL: A Proof Checker for First-order Logic, Stanford Artificial Intelligence Laboratory Memo AIM-235.1 (1977).

    Google Scholar 

  9. Weyhrauch, Richard W. The Uses of Logic in Artiflcial Intelligence, Lecture Notes prepared for the Summer School on the Foundations of Artificial Intelligence and Computer Science (FAICS '78), Pisa (1978).

    Google Scholar 

  10. Weyhrauch, Richard W. Prolegomena to a Mechanized Theory of Formal Reasoning, Stanford Artificial Intelligence Laboratory Memo AIM-315 (1979); to appear in Artificial Intelligence Journal (1980)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Istituto di Elaborazione della Informazione, CNR, Pisa, Italy

    Luigia Aiello

  2. Artificial Intelligence Laboratory, Stanford University, Stanford, USA

    Luigia Aiello & Richard W. Weyhrauch

Authors
  1. Luigia Aiello
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Richard W. Weyhrauch
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Wolfgang Bibel Robert Kowalski

Rights and permissions

Reprints and permissions

Copyright information

© 1980 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Aiello, L., Weyhrauch, R.W. (1980). Using meta-theoretic reasoning to do algebra. In: Bibel, W., Kowalski, R. (eds) 5th Conference on Automated Deduction Les Arcs, France, July 8–11, 1980. CADE 1980. Lecture Notes in Computer Science, vol 87. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-10009-1_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-10009-1_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-10009-6

  • Online ISBN: 978-3-540-38140-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation