Resolution Methods for the Decision Problem
Springer Science & Business Media, Jul 29, 1993 - Computers - 205 pages
This 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
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