Abstract | ||
---|---|---|
Complete paramodulation strategies are developed for clauses with symbolic constraints and built-in associativity and commutativity (AC) properties for a subset of the function symbols. Apart from the reduced search space due to the inherited ordering and unification restrictions of the inferences (cf. Nieuwenhuis and Rubio, 1995), symbolic constraints turn out to be especially useful in the context of built-in equational theories E . In every inference, instead of producing as many conclusions as minimal E -unifiers of two terms s and t , one single conclusion is generated with an additional E -unification problem s = t kept in its constraint. In the AC-case developed here (the most extensively studied built-in theory), the computation of the (doubly exponentially many) AC-unifiers can thus be completely avoided. These results are also applied here to more efficient strategies (sometimes decision procedures) in theories expressed by finite saturated sets of clauses and, in particular, to rewriting and Knuth–Bendix completion modulo AC. |
Year | DOI | Venue |
---|---|---|
1997 | 10.1006/jsco.1996.0074 | J. Symb. Comput. |
Keywords | DocType | Volume |
symbolic constraint,built-in AC-theories | Journal | 23 |
Issue | ISSN | Citations |
1 | Journal of Symbolic Computation | 10 |
PageRank | References | Authors |
0.61 | 20 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Robert Nieuwenhuis | 1 | 1405 | 93.78 |
Albert Rubio | 2 | 228 | 19.44 |