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)
68Q42: Grammars and rewriting systems
Related Items
Automated deduction with associative-commutative operators, A rewriting approach to satisfiability procedures., Unification modulo ACUI plus distributivity axioms