Name
Abstract | ||
|---|---|---|
We consider a restricted version of ordered paramodulation, called strict superposition. We show that strict superposition (together with equality resolution) is refutationally complete for Horn clauses, but not for general first-order clauses. Two moderate enrichments of the strict superposition calculus are, however, sufficient to establish refutation completeness. This strictly improves previous results. We also propose a simple semantic notion of redundancy for clauses which covers most simplification and elimination techniques used in practice yet preserves completeness of the proposed calculi. The paper introduces a new and comparatively simple technique for completeness proofs based on the use of canonical rewrite systems to represent equality interpretations. |
Year | DOI | Venue |
|---|---|---|
1990 | 10.1007/3-540-52885-7_105 | CADE |
Keywords | Field | DocType |
ordered paramodulation,first order | Superposition principle,Horn clause,Computer science,Algorithm,Superposition calculus,Redundancy (engineering),Mathematical proof,Completeness (statistics),Rule of inference | Conference |
Volume | ISBN | Citations |
449 | 3-540-52885-7 | 63 |
PageRank | References | Authors |
6.73 | 6 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Leo Bachmair | 1 | 1006 | 90.72 |
| Harald Ganzinger | 2 | 1513 | 155.21 |