Hyper tableaux with equality

Peter Baumgartner; Ulrich Furbach; Björn Pelzer

doi:10.1007/978-3-540-73595-3_36

Hyper tableaux with equality

Peter Baumgartner^*, Ulrich Furbach, Björn Pelzer

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

22 Citations (Scopus)

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 theorem proving. Our main results are soundness and completeness, but we briefly describe the implementation, too.

Original language	English
Title of host publication	Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings
Publisher	Springer Verlag
Pages	492-507
Number of pages	16
ISBN (Print)	3540735941, 9783540735946
DOIs	https://doi.org/10.1007/978-3-540-73595-3_36
Publication status	Published - 2007
Externally published	Yes
Event	21st International Conference on Automated Deduction, CADE-21 2007 - Bremen, Germany Duration: 17 Jul 2007 → 20 Jul 2007

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	4603 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	21st International Conference on Automated Deduction, CADE-21 2007
Country/Territory	Germany
City	Bremen
Period	17/07/07 → 20/07/07

Access to Document

10.1007/978-3-540-73595-3_36

Cite this

Baumgartner, P., Furbach, U., & Pelzer, B. (2007). Hyper tableaux with equality. In Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings (pp. 492-507). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4603 LNAI). Springer Verlag. https://doi.org/10.1007/978-3-540-73595-3_36

@inproceedings{037f9b730f604340b2e13488187a21aa,

title = "Hyper tableaux with equality",

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 theorem proving. Our main results are soundness and completeness, but we briefly describe the implementation, too.",

author = "Peter Baumgartner and Ulrich Furbach and Bj{\"o}rn Pelzer",

year = "2007",

doi = "10.1007/978-3-540-73595-3_36",

language = "English",

isbn = "3540735941",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "492--507",

booktitle = "Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings",

address = "Germany",

note = "21st International Conference on Automated Deduction, CADE-21 2007 ; Conference date: 17-07-2007 Through 20-07-2007",

}

Baumgartner, P, Furbach, U & Pelzer, B 2007, Hyper tableaux with equality. in Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4603 LNAI, Springer Verlag, pp. 492-507, 21st International Conference on Automated Deduction, CADE-21 2007, Bremen, Germany, 17/07/07. https://doi.org/10.1007/978-3-540-73595-3_36

Hyper tableaux with equality. / Baumgartner, Peter; Furbach, Ulrich; Pelzer, Björn.
Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings. Springer Verlag, 2007. p. 492-507 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4603 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Hyper tableaux with equality

AU - Baumgartner, Peter

AU - Furbach, Ulrich

AU - Pelzer, Björn

PY - 2007

Y1 - 2007

N2 - 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 theorem proving. Our main results are soundness and completeness, but we briefly describe the implementation, too.

AB - 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 theorem proving. Our main results are soundness and completeness, but we briefly describe the implementation, too.

UR - http://www.scopus.com/inward/record.url?scp=35148890322&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-73595-3_36

DO - 10.1007/978-3-540-73595-3_36

M3 - Conference contribution

SN - 3540735941

SN - 9783540735946

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 492

EP - 507

BT - Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings

PB - Springer Verlag

T2 - 21st International Conference on Automated Deduction, CADE-21 2007

Y2 - 17 July 2007 through 20 July 2007

ER -

Baumgartner P, Furbach U, Pelzer B. Hyper tableaux with equality. In Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings. Springer Verlag. 2007. p. 492-507. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-73595-3_36

Hyper tableaux with equality

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this