The addition of bounded quantification and partial functions to a computational logic and its theorem prover (Q1107510)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | The addition of bounded quantification and partial functions to a computational logic and its theorem prover |
scientific article |
Statements
The addition of bounded quantification and partial functions to a computational logic and its theorem prover (English)
0 references
1988
0 references
The paper describes an extension of a computational logic, developed earlier by the authors, by bounded quantifiers and partial functions. Bounded quantifiers are variable-binding constructs with the bound variable ranging over some finite sequence. The formalization employed also includes partial recursive functions. The computational logic which the work is based on is a quantifier-free first-order logic resembling pure Lisp. An extensive automated theorem prover has been written by the authors and shown to be able to check proofs of rather complicated theorems. The formalization of the quantifiers extends the existing logic and the theorem prover with additional constructs providing mechanisms for controlling the elementary operators of the underlying theories. Basic properties of the formalism are studied, and the use of the extended logic and its theorem prover are illustrated on construction of several proofs, including a proof of the Binomial Theorem.
0 references
recursion
0 references
interpreter
0 references
evaluation
0 references
semantics
0 references
continuity
0 references
computational logic
0 references
bounded quantifiers
0 references
partial functions
0 references
quantifier-free first- order logic
0 references
pure Lisp
0 references
automated theorem prover
0 references