Name
Title | ||
|---|---|---|
The Hyper Tableaux Calculus with Equality and an Application to Finite Model Computation |
Abstract | ||
|---|---|---|
In most theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this article 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 superposition are drawn (only) from a set of positive unit clauses, and superposition inferences into positive literals is restricted into (positive) unit clauses only. 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 of the calculus, but we also show how to apply the calculus for finite model computation, and we briefly describe the implementation. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1093/logcom/exn061 | J. Log. Comput. |
Keywords | Field | DocType |
finite model computation,proper treatment,hyper tableau calculus,semantically justified simplification rule,modern treatment,positive literal,hyper tableaux calculus,superposition theorem,superposition inference,superposition inference rule,positive unit clause,positive clause,theorem proving,inference rule | Superposition theorem,Discrete mathematics,Multivariable calculus,Automated theorem proving,Time-scale calculus,Algorithm,Soundness,Unit propagation,Rule of inference,Completeness (statistics),Calculus,Mathematics | Journal |
Volume | Issue | ISSN |
20 | 1 | 0955-792X |
Citations | PageRank | References |
3 | 0.46 | 23 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Peter Baumgartner | 1 | 364 | 26.97 |
| Ulrich Furbach | 2 | 639 | 88.23 |
| Björn Pelzer | 3 | 114 | 10.64 |