Any ground associative-commutative theory has a finite canonical system
From MaRDI portal
Publication:1357668
DOI10.1007/BF00247671zbMath0878.68076MaRDI QIDQ1357668
Paliath Narendran, Michaël Rusinowitch
Publication date: 14 December 1997
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Related Items (9)
Automated deduction with associative-commutative operators ⋮ A rewriting approach to satisfiability procedures. ⋮ Extensions of unification modulo ACUI ⋮ An Assertional Language for the Verification of Systems Parametric in Several Dimensions ⋮ Unification modulo ACUI plus distributivity axioms ⋮ Associative-commutative deduction with constraints ⋮ AC-superposition with constraints: No AC-unifiers needed ⋮ Order-Sorted Rewriting and Congruence Closure ⋮ Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols
This page was built for publication: Any ground associative-commutative theory has a finite canonical system
