MPI-I-92-224
Completeness of resolution and superposition calculi
Socher-Ambrosius, Rolf
June 1992, 9 pages.
.
Status: available - back from printing
We modify Bezem's (Bezem, M. Completeness of
Resolution Revisited. Theoretical Computer
Science 74 (1990) 227-237) completeness proof
for ground resolution in order to
deal with ordered resolution, redundancy,
and equational reasoning in form
of superposition. The resulting proof is
completely independent of the
cardinality of the set of clauses.
-
MPI-I-92-224.pdf
- Attachement: MPI-I-92-224.ps (832 KBytes); MPI-I-92-224.pdf (75 KBytes)
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1992-224
BibTeX
@TECHREPORT{Socher-Ambrosius92c,
AUTHOR = {Socher-Ambrosius, Rolf},
TITLE = {Completeness of resolution and superposition calculi},
TYPE = {Research Report},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
NUMBER = {MPI-I-92-224},
MONTH = {June},
YEAR = {1992},
ISSN = {0946-011X},
}