THEORY OF ADAPTIVE MECHANISMS. PART III. EFFICIENT MAXIMAL SEMANTIC RESOLUTION PROOFS BASED UPON BINARY SEMANTIC TREES.
Abstract
A new proof procedure is presented which generates an efficient maximal semantic resolution proof of the inconsistency of any wff (well formed formula) of first order logic without equality. This is done by constructing one path at a time down a binary semantic tree. The new proof procedure has the parameters: any model for the wff and any total ordering of the Herbrand base of the wff. This technique is more efficient than the method of inference nodes because more powerful inferences are made and the path need not be constructed to the bottom of the binary semantic tree for a resolution to be performed. It is also more efficient than the British Museum Algorithm for maximal semantic resolution. For a propositional wff, it is shown that the prime implicants can be generated by repeated applications of binary resolution and the subsumption rule. Furthermore, the prime implicants which cover a particular model (i.e., a zero-cube on the Karnaugh map) can be efficiently generated by repeated applications of maximal semantic resolution and the subsumption rule. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 01, 1970
- Accession Number
- AD0711049
Entities
People
- R. G. Cantarella
Organizations
- Syracuse University