Document Type
Report
Date
10-1991
Keywords
Resolution
Language
English
Disciplines
Computer Sciences
Description/Abstract
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.
Recommended Citation
Purdy, William C., "Resolution without Unification" (1991). Electrical Engineering and Computer Science - Technical Reports. 102.
https://surface.syr.edu/eecs_techreports/102
Source
local
Additional Information
School of Computer and Information Science, Syracuse University, SU-CIS-91-31