Metafunctions in nqthm and acl

Abstract

Meta-level reasoning was added to the Boyer-Moore theorem prover by 1979. We have recently re-implemented and, we think, slightly improved our approach to meta-theoretic reasoning in the Acl2 theorem prover. However, there is lots of room for much more substantial improvement. Our talk will consist of 3 parts: review, recent results, and general remarks.

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,174

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

  • Only published works are available at libraries.

Similar books and articles

Metamathematics, machines, and Gödel's proof.N. Shankar - 1994 - New York: Cambridge University Press.
Automated Reasoning for Conditional Logics: the Theorem Prover Condlean 3.1.Nicola Olivetti & Gian Luca Pozzato - 2007 - In Jean-Yves Béziau & Alexandre Costa-Leite (eds.), Perspectives on Universal Logic. Milan, Italy: Polimetrica.

Analytics

Added to PP
2009-01-28

Downloads
14 (#1,280,710)

6 months
3 (#1,475,474)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references