Quantification in tail-recursive function definitions

We investigate the logical issues behind axiomatizing equations that contain both recursive calls and quantifiers in ACL2. We identify a class of such equations, named extended tail-recursive equations, that can be uniformly introduced in the logic. We point out some potential benefits of this axiomatization, and discuss the logical impediments behind introducing more general quantified formulas. Categories and Subject Descriptors F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs--Assertions, Invariants, Mechanical Verification; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic-Computational Logic, Mechanical Theorem Proving General Terms Theory, Verification Keywords Formal methods, Logic, ACL2, Skolemization, Conservativity

• Type: Conference
• Year: 2006
• Where: ACL2
• Authors: Sandip Ray
• Keywords: ACL2 2006, Computational Linguistics, General Quantified Formulas, Keywords Formal Methods, Mathematical Logic-Computational Logic