Name
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. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/978-3-540-73595-3_36 | CADE |
Keywords | Field | DocType |
proper treatment,hyper tableau calculus,semantically justified simplification rule,modern treatment,Hyper Tableaux,superposition theorem,superposition inference rule,equational theory,candidate model,positive unit clause,positive clause | Superposition theorem,Discrete mathematics,Superposition principle,Computer science,Automated theorem proving,Algorithm,Redundancy (engineering),Unit propagation,Soundness,Completeness (statistics),Rule of inference | Conference |
Volume | ISSN | Citations |
4603 | 0302-9743 | 5 |
PageRank | References | Authors |
0.50 | 13 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Peter Baumgartner | 1 | 364 | 26.97 |
| Ulrich Furbach | 2 | 639 | 88.23 |
| Björn Pelzer | 3 | 114 | 10.64 |