Skip to main content

TS

Hyper tableaux with equality

Authors

Peter Baumgartner, Ulrich Furbach and Bjoern Pelzer

NICTA

Universitaet Koblenz-Landau
Germany

Abstract

In most theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this paper we show how to integrate a modern treatment of equality in the hyper tableau calculus. It is based on splitting of positive clauses and an adapted version of the superposition inference rule, where equations used for paramodulation are drawn (only) from a set of positive unit clauses, the candidate model. The calculus also features a generic, semantically justified simplification rule which covers many redundancy elimination techniques known from superposition-style theorem proving. Our main theoretical result is the soundness and completeness of the calculus. The calculus is implemented, and we also report on practical experiments.

BibTeX Entry

  @inproceedings{Baumgartner_FP_07,
    publisher        = {Springer},
    isbn             = {3-540-73594-1},
    author           = {Baumgartner, Peter and Furbach, Ulrich and Pelzer, Bjoern},
    month            = jul,
    editor           = {{Frank Pfenning}},
    year             = {2007},
    title            = {Hyper Tableaux with Equality},
    booktitle        = {CADE-21 -- The 21st International Conference on Automated Deduction},
    pages            = {492-507},
    address          = {Bremen, Germany}
  }

Download

Served by Apache on Linux on seL4.