Paper Info
Title
Paramodulation with built-in AC-theories and symbolic constraints
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 Nieuwenhuis1140593.78
Albert Rubio222819.44