Skip to main content


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

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


Served by Apache on Linux on seL4.