Meta Reasoning in ACL2

DOI10.1007/11541868_11zbMATH Open1152.68522OpenAlexW1490999085MaRDI QIDQ5477654FDOQ5477654

Authors: Warren A. jun. Hunt, Matt Kaufmann, Robert Bellarmine Krug, J Strother Moore, Eric Whitman Smith 

Publication date: 6 July 2006

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11541868_11

Recommendations

• scientific article; zbMATH DE number 2079835
• scientific article; zbMATH DE number 2101985
• Formal proofs about rewriting using ACL2
• scientific article; zbMATH DE number 1926640
• Milestones from the Pure Lisp Theorem Prover to ACL2

Mathematics Subject Classification ID

Cited In (10)

• Directly reflective meta-programming
• Verified AIG algorithms in ACL2
• Meta-extract: using existing facts in meta-reasoning
• Incorporating quotation and evaluation into Church's type theory
• A graph library for Isabelle
• Integrating external deduction tools with ACL2
• Metainferential reasoning on strong Kleene models
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• Second-order programs with preconditions
• An ACL2 Tutorial

Uses Software

• ACL2

This page was built for publication: Meta Reasoning in ACL2

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5477654)