MPI-INF Logo
MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments

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.pdfMPI-I-92-224.pdfMPI-I-92-224.ps
  • 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

Hide details for BibTeXBibTeX
@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},
}