Name
Abstract | ||
|---|---|---|
Up to now, all existing completeness results for ordered paramodulation and Knuth–Bendix completion have required term ordering ≻ to be well founded, monotonic, and total(izable) on ground terms. For several applications, these requirements are too strong, and hence weakening them has been a well-known research challenge.Here we introduce a new completeness proof technique for ordered paramodulation where the only properties required on ≻ are well-foundedness and the subterm property. The technique is a relatively simple and elegant application of some fundamental results on the termination and confluence of ground term rewrite systems (TRS).By a careful further analysis of our technique, we obtain the first Knuth–Bendix completion procedure that finds a convergent TRS for a given set of equations E and a (possibly non-totalizable) reduction ordering ≻ whenever it exists. Note that being a reduction ordering is the minimal possible requirement on ≻, since a TRS terminates if, and only if, it is contained in a reduction ordering. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1023/A:1022515030222 | Journal of Automated Reasoning |
Keywords | Field | DocType |
term rewriting,automated deduction | Discrete mathematics,Monotonic function,Automated theorem proving,Algorithm,Confluence,If and only if,Completeness (statistics),Mathematics | Journal |
Volume | Issue | ISSN |
30 | 1 | 1573-0670 |
Citations | PageRank | References |
5 | 0.48 | 20 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Miquel Bofill | 1 | 148 | 19.04 |
| Guillem Godoy | 2 | 220 | 21.72 |
| Robert Nieuwenhuis | 3 | 1405 | 93.78 |
| Albert Rubio | 4 | 228 | 19.44 |