Resolution-Based Methods

  • Ricardo Caferra
  • Alexander Leitsch
  • Nicholas Peltier
Part of the Applied Logic Series book series (APLS, volume 31)


The model building methods presented in this chapter are based on deductive saturation procedures. Instead of constructing refutation trees we consider resolution as an operator on sets of clauses. If a finite number of iterations of the operator leads to a fixed point set C then there are two possibilities: either C contains □ and we have shown that the original set of clauses is unsatisfiable, or □ is not in C; in the latter case we may conclude that C is satisfiable. This is the general principle of resolution decision procedures (for a thorough treatment of this topic see [Fermüller et al., 1993]) . As unrefined resolution shows a quite bad termination behavior, resolution decision procedures are mostly based on refinements. Here not only the correctness but also the completeness of refinements are required in order to ensure the correctness of the decision procedure. Once we have found out that the original set of clauses D is satisfiable we may use the computed fixed point set C for constructing a model of D this is basically the approach to model building we are following in this chapter.


Horn Clause Ground Atom Unit Clause Atomic Representation Ground Substitution 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media Dordrecht 2004

Authors and Affiliations

  • Ricardo Caferra
    • 1
  • Alexander Leitsch
    • 2
  • Nicholas Peltier
    • 3
  1. 1.Laboratory Leibniz — IMAG, INPGGrenobleFrance
  2. 2.Vienna University of TechnologyAustria
  3. 3.Laboratory Leibniz — IMAG, CNRSGrenobleFrance

Personalised recommendations