Record Details


Field	Value

Title	Proving associative-commutative termination using RPO-compatible orderings

Creator	KAPUR, D SIVAKUMAR, G

Subject	rewriting-systems

Description	Developing path orderings for associative-commutative (AC) rewrite systems has been quite a challenge at least for a decade. Compatibility with the recursive path ordering (RPO) schemes is desirable, and this property helps in orienting the commonly encountered distributivity axiom as desired. For applications in theorem proving and constraint solving, a total ordering on ground terms involving AC operators is often required. It is shown how the main solutions proposed so far ([7],[13]) with the desired properties can be viewed as arising from a common framework. A general scheme that works for non-ground (general) terms also is proposed. The proposed definition allows flexibility (using different abstractions) in the way the candidates of a term with respect to an associative-commutative function symbol are compared, thus leading to at least two distinct orderings on terms (from the same precedence relation on function symbols).

Publisher	SPRINGER-VERLAG BERLIN

Date	2011-08-30T12:06:33Z 2011-12-26T12:58:56Z 2011-12-27T05:49:39Z 2011-08-30T12:06:33Z 2011-12-26T12:58:56Z 2011-12-27T05:49:39Z 2000

Type	Article

Identifier	AUTOMATED DEDUCTION IN CLASSICAL AND NON-CLASSICAL LOGICS, 1761(), 39-61 0302-9743 http://dspace.library.iitb.ac.in/xmlui/handle/10054/12308 http://hdl.handle.net/10054/12308

Language	en

ICAR Research Data Repository for Knowledge Management