Meta Reasoning in ACL2

DOI10.1007/11541868_11MaRDI QIDQ5477654zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Describes a project that uses

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)