MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments


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.

  • Attachement: (832 KBytes); MPI-I-92-224.pdf (75 KBytes)

URL to this document:

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