Name
Abstract | ||
|---|---|---|
. We present an associative-commutative paramodulation calculusthat generalizes the associative-commutative completion procedure to firstorderclauses. The calculus is parametrized by a selection function (on negativeliterals) and a well-founded ordering on terms. It is compatible with an abstractnotion of redundancy that covers such simplification techniques as tautologydeletion, subsumption, and simplification by (associative-commutative) rewriting.The proof of refutational completeness... |
Year | DOI | Venue |
|---|---|---|
1994 | 10.1007/3-540-60381-6_1 | CTRS |
Keywords | Field | DocType |
associative-commutative superposition | Tautology (logic),Associative property,Algebra,Commutative property,Redundancy (engineering),Rewriting,Completeness (statistics),Congruence relation,Rule of inference,Mathematics | Conference |
ISBN | Citations | PageRank |
3-540-60381-6 | 16 | 1.04 |
References | Authors | |
20 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Leo Bachmair | 1 | 1006 | 90.72 |
| Harald Ganzinger | 2 | 1513 | 155.21 |