Abstract
In this chapter we present ACL2 as a mathematical logic. Traditionally, one begins by specifying the syntax of formulas, identifying some formulas as axioms, and precisely specifying some rules of inference. The rules of inference are formula transformers; they permit one to produce new formulas from old formulas. A theorem is either an axiom or the formula produced by applying some rule of inference to other theorems. A proof is a finite tree showing the derivation of a theorem from the axioms. The traditional presentation of a mathematical logic proceeds by assigning a meaning to formulas as follows. A structure is a pair consisting of a domain and a map assigning functions and predicates on the domain to the function and predicate symbols of the logic. An interpretation is a pair consisting of a structure and an assignment of elements in the domain to the variable symbols. The semantics of a formula under an interpretation is the truth-value of the formula under the interpretation. An interpretation is a model of a set of formulas if every formula in the set is true in the interpretation. If the rules of inference are truth preserving then every theorem is true in every model of the axioms.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Notes
A stronger condition holds, namely that each axiom gives a conservative extension of the existing set of axioms. This means that no new theorems can be proved about the existing set of function symbols when the new axiom is added.
However, the user of the mechanized ACL2 writes this as ((v1 TN) … (vn Tn)).
In the definition of e0-ord->, atoms are coerced to rationals so that the guards of the function can be verified. The Common Lisp Language does not define > on non-numeric arguments.
It is not crucial that you remember this definition when using the theorem prover. The reason is that when you define a recursive function, the theorem prover will print out the measure conjectures that it must prove, so for any given definition you will see what is required.
The reason has to do with the induction scheme we prefer to generate from such definitions.
The ACL2 universe is not closed. There are no axioms that say an object must have one of the five types listed.
An informal proof is fine here. Those familiar with set theory will notice that they are using some form of the axiom of choice in their proof.
f can be a function symbol or a lambda expression and must be of the same arity as f.
Often in mechanical proofs, (mv-nth 0 v) is simplified to (car v), while (mv-nth 1 v) is not expanded. This is due to the heuristics for expanding the recursive function mv-nth, where 0 is the base case. This obscure note may help you formulate rewrite rules about the various components of the output vector of such a function.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media New York
About this chapter
Cite this chapter
Kaufmann, M., Manolios, P., Moore, J.S. (2000). The Logic. In: Computer-Aided Reasoning. Advances in Formal Methods, vol 3. Springer, Boston, MA. https://doi.org/10.1007/978-1-4615-4449-4_6
Download citation
DOI: https://doi.org/10.1007/978-1-4615-4449-4_6
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4613-7003-1
Online ISBN: 978-1-4615-4449-4
eBook Packages: Springer Book Archive