A Computational Logic with Quantifiers.
Abstract
A logical theory consists of a language, some axioms schemas, and some rules of inference. However, in developing the proofs of interesting theorems it is often necessary to introduce axioms defining new concepts and operations. Logically speaking, the main results and all of the lemmas along the way are proved in the final theory. To accomodate the practical view of the situation we provide several 'extension principles' by which the user of the theory can add new axioms of a particularly constructive sort. Among these principles is the 'shell principle,' which permits the axiomatization of a 'new' type of inductively constructed object, and the 'definitional principle,' which permits the introduction of an equation defining a recursive function. These extension principles can be considered as rules of inference since they permit one to deduce that certain formulas are theorems. We present the formal syntax of our logic. This syntax is extremely simple and is not the syntax implemented in the theorem-prover. We then develop a large number of syntactic conventions used to describe the axioms and rules of inference. Once we have completed the formal development of the logic we turn, in Section IMPLEMENTEDSYNTAX, to a description of the implemented syntax.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 01, 1984
- Accession Number
- ADA144335
Entities
People
- J. S. Moore
- R. S. Boyer
Organizations
- University of Texas at Austin