Skip to main content

TS

Hierarchic superposition: Completeness without compactness

Authors

Peter Baumgartner and Uwe Waldmann

NICTA

Max-Planck-Institute for Computer Science

Abstract

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

  @inproceedings{Baumgartner_Waldmann_13_2,
    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
                        2013)},
    pages            = {8-12},
    address          = {Nanning, China}
  }

Download

Served by Apache on Linux on seL4.