A macro for reusing abstract functions and theorems

DOI10.4204/EPTCS.114.3MaRDI QIDQ6587251zbMATH OpenFDO

Authors Sebastiaan J. C. Joosten, Bernard van Gastel, Julien Schmaltz

Publication date 13 August 2024

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

Mathematics Subject Classification ID

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

Recommendations

• Limited second-order functionality in a first-order setting
• Second-order functions and theorems in ACL2
• Partial functions in ACL2
• scientific article; zbMATH DE number 88983
• Generating mutually inductive theorems from concise descriptions

Cites work

• Formalization of a normalization theorem in simplicial topology
• How can I do that with ACL2? Recent enhancements to ACL2
• scientific article; zbMATH DE number 88983 (Why is no real title available?)

Cited in

(2)

• Second-order functions and theorems in ACL2
• Generating mutually inductive theorems from concise descriptions

This page was built for publication: A macro for reusing abstract functions and theorems

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