## Resolution Methods for the Decision ProblemThis volume contains work on the decision problem done in Kazan (Russia), Tallinn (Estonia), and Vienna (Austria). The authors met several times to discuss and exchange their results and finally decided to write this monograph together. Besides a unified treatment of previously published results there are many new results first presented in this volume. The monograph opens with an introduction and a chapter on terminology, followed by chapters on: - Semantic clash resolution as decision procedure, - Completeness of ordering refinements, - Semantic tree based resolution variants, - Deciding the class K by an ordering refinement, - A resolution based method for building finite models. A final chapter on applications completes the volume. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Other editions - View all

Resolution Methods for the Decision Problem C. Fermüller,A. Leitsch,Tanel Tammet,Nail Zamov No preview available - 1993 |

Resolution Methods for the Decision Problem C. Fermuller,A. Leitsch,Tanel Tammet No preview available - 2014 |

### Common terms and phrases

A-ordering Ackermann argument arity atoms Automated Theorem Proving binary called chapter clash resolvent clause form clause logic clause set Cneg completeness compute condensed constant symbol contains corresponding Cpos DATALOG decision problem decision procedure defined DEFINITION denote disunification dominating term electron equation essentially monadic example finite model formula function symbols functional term ground clauses ground instance ground term HD(C Herbrand base Herbrand universe holds Horn clause HOSC HRS(C implication problem implies induction KL-ONE lemma literal of type method OCC(x OCC1N occur ordering refinement positive hyperresolution predicate logic predicate symbols prefix proof prove regular term resolution refinement restricted factoring RSCm RSCmD satisfiable semantic clash resolution semantic tree set of clauses Skolem strategy substitution subsumed subsumption subterms syntactically term depth termination theorem tj/xj unifiable unsat unsatisfiable v-refinement V(C_ V(C+ V(Cneg variable weakly covering

### Popular passages

Page 198 - Gilbert, and HJ Levesque. An essential hybrid reasoning system: Knowledge and symbol level accounts in KRYPTON.