MPI-I-91-208. September 1991, 24 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry
Abstract in LaTeX format:
We present various refutationally complete calculi for first-order clauses with equality that
allow for arbitrary selection of negative atoms in clauses. Refutation completeness is established via the use of well-founded orderings on clauses for defining a Herbrand model for a consistent set of clauses.
We also formulate an abstract notion of redundancy and show that the deletion of redundant clauses
during the theorem proving process preserves refutation completeness.
It is often possible to compute the closure of nontrivial sets of clauses under application of non-redundant inferences.
The refutation of goals for such complete sets of clauses is simpler than for arbitrary sets of clauses, in particular one can restrict attention to proofs that have support from the goals without compromising refutation completeness. Additional syntactic properties allow to restrict the search space even further, as we demonstrate for so-called quasi-Horn clauses.
The results in this paper contain as special cases or generalize many known results about Knuth-Bendix-like completion procedures (for equations, Horn clauses, and Horn clauses over built-in Booleans), completion of first-order clauses by clausal rewriting, and inductive theorem proving for Horn clauses.
Revised version in the Journal of Logic and Computation 4, 3 (1994), pp.~217--247
References to related material:
|To download this research report, please select the type of document that fits best your needs.||Attachement Size(s):|
|MPI-I-91-208.pdf||109 KBytes; 177 KBytes|
|Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView|