Second-order functions and theorems in ACL2

DOI10.4204/EPTCS.192.3MaRDI QIDQ6591103zbMATH OpenFDO

Authors Alessandro Coglio

Publication date 21 August 2024

Mathematics Subject Classification ID

Higher-order logic (03B16) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Limited second-order functionality in a first-order setting
• A macro for reusing abstract functions and theorems
• Partial functions in ACL2
• scientific article; zbMATH DE number 88983
• Theory and practice of second-order rewriting: foundation, evolution, and SOL

Cited in

(1)

• A macro for reusing abstract functions and theorems

This page was built for publication: Second-order functions and theorems in ACL2

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