Meta-extract: using existing facts in meta-reasoning

DOI10.4204/EPTCS.249.4MaRDI QIDQ6591109zbMATH OpenFDO

Authors Matt Kaufmann, Sol Swords

Publication date 21 August 2024

Full work available at URL https://doi.org/10.4204/EPTCS.249.4

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Meta Reasoning in ACL2
• How can I do that with ACL2? Recent enhancements to ACL2
• Enhancements to ACL2 in versions 5.0, 6.0, and 6.1
• Milestones from the Pure Lisp Theorem Prover to ACL2
• A versatile, sound tool for simplifying definitions

Cited in

(3)

• How can I do that with ACL2? Recent enhancements to ACL2
• Enhancements to ACL2 in versions 5.0, 6.0, and 6.1
• A versatile, sound tool for simplifying definitions

This page was built for publication: Meta-extract: using existing facts in meta-reasoning

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