The addition of bounded quantification and partial functions to a computational logic and its theorem prover (Q1107510)

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.