Name
Abstract | ||
|---|---|---|
Recently, ordered paramodulation and Knuth-Bendix: completion were shown to remain complete when using non-monotonic orderings. However, these results only implied the compatibility with too weak redundancy notions and, in particular, demodulation could not be applied at all. In this paper, we present a complete ordered paramodulation calculus compatible with powerful redundancy notions including demodulation, which strictly improves previous results. Our results can be applied as well to obtain a Knuth-Bendix completion procedure compatible with simplification techniques, which can be used for finding, whenever it exists, a convergent TRS for a given set of equations and a (possibly non-totalizable) reduction ordering. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1007/978-3-540-25984-8_6 | Lecture Notes in Artificial Intelligence |
Field | DocType | Volume |
Monotonic function,Discrete mathematics,Automated reasoning,Demodulation,Compatibility (mechanics),Computer science,Automated theorem proving,Algorithm,Circumscription,Redundancy (engineering),Completeness (statistics) | Conference | 3097 |
ISSN | Citations | PageRank |
0302-9743 | 3 | 0.45 |
References | Authors | |
10 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Miquel Bofill | 1 | 148 | 19.04 |
| Albert Rubio | 2 | 228 | 19.44 |