Accession Number : AD0711049
Title : THEORY OF ADAPTIVE MECHANISMS. PART III. EFFICIENT MAXIMAL SEMANTIC RESOLUTION PROOFS BASED UPON BINARY SEMANTIC TREES.
Descriptive Note : Final technical rept. 8 Aug 66-31 Oct 69,
Corporate Author : SYRACUSE UNIV RESEARCH INST N Y
Personal Author(s) : Cantarella,R. G.
Report Date : JUL 1970
Pagination or Media Count : 172
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)
Descriptors : (*ARTIFICIAL INTELLIGENCE, AUTOMATA), (*LEARNING MACHINES, THEORY), SEMANTICS, BINARY ARITHMETIC, FLOW CHARTING, CONTROL SEQUENCES, OPTIMIZATION, PROBLEM SOLVING, ADAPTIVE SYSTEMS, RECURSIVE FUNCTIONS, STOCHASTIC PROCESSES, REPORTS
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE