|
Abstract : |
During the last years, several saturation-based theorem proving techniques for full first-order (ordering and/or equality constrained) clauses with equality have emerged. Bachmair and Ganzinger ([BG91]) apply a model construction technique for proving the refutational completeness of strict superposition (paramodulation restricted to maximal terms of maximal equations of clauses). Their powerful abstract redundancy notions allow redundant inferences to be ignored and redundant clauses to be deleted without loosing completeness. This makes it also possible to compute finite saturated sets of axioms. Using saturated sets, more efficient proof strategies become (refutationally) complete, like the set-of-support strategy, which is normally incomplete for ordered inference systems and also for equality clauses. Saturated sets fulfilling some syntactic properties even provide decision procedures, like rewrite proofs do in the equational case. Moreover, if a finite saturated set (not containing the empty clause) is obtained for a given theory, then its consistency has been proved (normally one can only prove inconsistencies)., |
