Resolution methods for the decision problem (Q1310269)

For first-order logic with function symbols the authors treat the decision problem by proof-theoretical, essentially resolution-based methods. In this monograph they collect and extend earlier results of their own. After two introductory chapters, chapter 3 (by Leitsch) discusses semantic clash resolution. Chapter 4 (by Tammet) is devoted to a detailed treatment of ordering refinements and their completeness properties. Chapter 5 (by Fermüller) describes various decision procedures based on \(A\)-ordering refinements and saturation. Also based on ordering refinements is a decision procedure for Maslov's \(K\)-classes, which is given in chapter 6 (by Zamov). And in chapter 7 (by Tammet), methods of resolution and narrowing are applied to automatical finite model building. The final chapter 8 presents some additional applications, e.g. to the consistency problem in knowledge representation languages, and discusses results of experiments with implementations of the decision methods of the monograph.