Trustworthy Systems

Hierarchic superposition: Completeness without compactness


Peter Baumgartner and Uwe Waldmann


Max-Planck-Institute for Computer Science


Hierarchic superposition calculi aim at proving the inconsistency of a set of first-order clauses with respect to conservative extensions of a background specification. The calculi are refutationally complete if the set of clauses is sufficiently complete and if the background specification is compact. We demonstrate that, in the case of linear integer or rational arithmetic, the compactness requirement can be waived if all background-sorted terms in the clauses are ground or variables, and that, under certain conditions, also variables with offsets can be permitted.

BibTeX Entry

    month            = nov,
    keywords         = {first-order logic, automated theorem proving},
    paperurl         = {},
    booktitle        = {Fifth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS
    editor           = {{Marek Kosta and Thomas Sturm}},
    author           = {Baumgartner, Peter and Waldmann, Uwe},
    year             = {2013},
    pages            = {8--12},
    title            = {Hierarchic Superposition: Completeness without Compactness},
    address          = {Nanning, China}