Resolution without Unification

Resolution as an inference procedure forms the basis of most automated theorem-proving and reasoning systems. The most costly constituent of the resolution procedure in its conventional form is unification. This paper describes PCS, a first-order language in which resolution-based inference can be conducted without unification. PCS resembles the language of elementary logic with the difference that singular predicates supplant individual constants and functions. The result is a uniformity in the treatment of individual constants, functions and predicates. An especially costly part of unification is the occur check. Since unification is unnecessary for resolution in PCS, the occur check is completely circumvented. The conditions that would invoke an occur check are properly represented however. In this sense, resolution in PCS can be viewed as a refinement of conventional resolution. PCS does not have an identity relation. Nonetheless, identity can be expressed in PCS and deduction with identical can be performed