Delivery-Date: 
Message-Id: <9405191339.AA26404@csdec1.tuwien.ac.at>
To: aal@anu.edu.au, deduktion@intellektik.informatik.th-darmstadt.de, 
    fg121@inferenzsysteme.informatik.th-darmstadt.de, info-hol@cs.uidaho.edu, 
    kgs@csdec1.tuwien.ac.at, nqthm-users@cli.com, qed@mcs.anl.gov, 
    rewriting-list@lorraine.loria.fr, theorem-provers@mc.lcs.mit.edu
Subject: CADE tutorial on resolution as decision method
Date: Thu, 19 May 94 15:39:34 +0200
From: chrisf@csdec1.tuwien.ac.at

CALL FOR PARTICIPATION:  

                         TUTORIAL

                 RESOLUTION DECISION METHODS

Speakers: C. Fermueller, A. Leitsch, T. Tammet, N. Zamov.
Time: June 26, 1994

CONTENT:

   It is a central problem of logic and computer science to determine
whether a formula in predicate logic is decidable. A thorough 
investigation of decidable classes can be found in the book of Dreben 
and Goldfarb; this approach, however, is model theoretic and does not 
provide feasible algorithms. We present a proof theoretic method, based 
on resolution refinements, to decide a wide range of clause classes. The 
central idea is to use complete resolution refinements and guarantee 
termination on decidable clause classes. Besides the applications to the 
decision problem resolution decision methods provide a tool for designing 
efficient general theorem provers for first order clause logic and 
methods for automated model building. Based on approaches of Joyner 
and of the Maslov school our approach is method oriented; that means we 
investigate several types of resolution refinements w.r.t. their 
potential of deciding clause classes. Recent work of this type has been 
summarized by the speakers mentioned above in [FLTZ93].
The presentation will (roughly) consists of three parts:

1. Hyperresolution as decision procedure.
2. Ordering resolution as decision procedure.
3. Finite model building based on resolution decision procedures.

AD 1.)
  We define the classes PVD, OCC1N (PVD is a strong generalization 
of DATALOG to non-Horn functional classes) and characterize termination 
of hyperresolution by abstract atom complexity measures. Moreover we 
indicate how termination sets of hyperresolution can be turned into 
representations of Herbrand models. In case of PVD and OCC1N these 
Herbrand models can be transformed into finite models by filtration.
The decision classes suggest a selection strategy for refinements 
resulting in a prover generator. Finally it is pointed out that 
significant speed-ups of ATP-programs may be achieved by selecting 
decision refinements as theorem provers.

AD 2.) 
  We present A-ordering, Pi-ordering and ordering methods without 
ground lifting. We introduce the concept of covering and weakly 
covering terms and show, how to obtain decidable classes properly 
containing the one-variable class; e.g. we show that the method of 
A-ordering combined with saturation yields a method to decide 
extensions of the initially-extended Skolem class. The saturation 
principle is shown to be of importance to decide the Bernays- 
Schoenfinkel class. It is demonstrated how Maslov's K-class (this 
class contains many of the well-known decidable classes) can be 
decided by a non-liftable ordering refinement.

AD 3.)
  We present a post-processing of termination sets (under ordering 
refinements) defined by decision procedures on the Ackermann- and 
monadic class resulting in representations of finite models. The 
method essentially consists in pruning term trees via ground rewrite 
rules and in applying narrowing. The method is purely syntactic and 
yields full interpretations of the function symbols over the domain 
of the finite model. This method has already been shown powerful in 
experiments with implementations.

[FLTZ93] C.Fermueller, A.Leitsch, T.Tammet, N.Zamov: Resolution 
  Methods for the Decision Problem, Lecture Notes in AI 679 (1993).