Document Type

Report

Date

10-1991

Embargo Period

5-2-2012

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.

Additional Information

School of Computer and Information Science, Syracuse University, SU-CIS-91-31

Source

local

Share

COinS
 
 

To view the content in your browser, please download Adobe Reader or, alternately,
you may Download the file to your hard drive.

NOTE: The latest versions of Adobe Reader do not support viewing PDF files within Firefox on Mac OS and if you are using a modern (Intel) Mac, there is no official plugin for viewing PDF files within the browser window.