Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
Meta Reasoning in ACL2
verfasst von : Warren A. Hunt Jr, Matt Kaufmann, Robert Bellarmine Krug, J Strother Moore, Eric Whitman Smith
Erschienen in: Theorem Proving in Higher Order Logics
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The ACL2 system is based upon a first-order logic and implements traditional first-order reasoning techniques, notably (conditional) rewriting, as well as extensions including mathematical induction and a “functional instantiation” capability for mimicking second-order reasoning. Additionally, one can engage in meta-reasoning — using ACL2 to reason, and prove theorems, about ACL2’s logic from within ACL2. One can then use these theorems to augment ACL2’s proof engine with custom extensions. ACL2 also supports forms of meta-level control of its rewriter. Relatively recent additions of these forms of control, as well as extensions to ACL2’s long-standing meta-reasoning capability, allow a greater range of rules to be written than was possible before, allowing one to specify more comprehensive proof strategies.