Sciweavers

IPL
2006

Knuth-Bendix completion of theories of commuting group endomorphisms

13 years 4 months ago
Knuth-Bendix completion of theories of commuting group endomorphisms
Knuth-Bendix completions of the equational theories of k 2 commuting group endomorphisms are obtained, using automated theorem proving and modern termination checking. This improves on modern implementations of completion, where the orderings implemented cannot orient the commutation rules. The result has applications in decision procedures for automated verification. Key words: Knuth-Bendix completion, group theory, decision procedures
Aaron Stump, Bernd Löchner
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2006
Where IPL
Authors Aaron Stump, Bernd Löchner
Comments (0)