A typed resolution principle for deduction with conditional typing theory

摘要

The formal reasoning involved in solving a real world problem usually consists of two parts: type reasoning associated with the type structure of the problem domain, and general reasoning associated with the kernel formulation. This paper introduces a typed resolution principle for a typed predicate calculus. This principle permits a separation of type reasoning from general reasoning even when the background typing theory shares the same language constructs with the kernel formulation. Such a typing theory is required for an accurate formulation of the type structure of a computer program which contains partial functions and predicate subtypes, and also is useful for efficiently proving certain theorems from mathematics and logic by typed (sorted) formulation and deduction. The paper presents a typed deduction procedure which employs type reasoning as a form of constraints to general reasoning for speeding up the proof discovery. The paper also discusses further refinements of the procedure by incorporating existing refinements of untyped resolution.