THEORY OF ADAPTIVE MECHANISMS. PART III. EFFICIENT MAXIMAL SEMANTIC RESOLUTION PROOFS BASED UPON BINARY SEMANTIC TREES.
Final technical rept. 8 Aug 66-31 Oct 69,
SYRACUSE UNIV RESEARCH INST N Y
Pagination or Media Count:
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
- Computer Programming and Software
- Computer Hardware