Automated proofs of the Moufang identities in alternative rings

DOI10.1007/BF00302643zbMath0698.68079MaRDI QIDQ912653

Siva Anantharaman, Jieh Hsiang

Publication date: 1990

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

equational logicalternative ringsterm rewritingMoufang identitiesKnuth-Bendix completion

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Software, source code, etc. for problems pertaining to nonassociative rings and algebras (17-04)

Related Items (10)

An application of automated equational reasoning to many-valued logic ⋮ Completion procedures as semidecision procedures ⋮ On subsumption in distributed derivations ⋮ A case study of completion modulo distributivity and Abelian groups ⋮ Towards a foundation of completion procedures as semidecision procedures ⋮ Solving the word problem for two classes of non-associative rings by rewriting ⋮ Any ground associative-commutative theory has a finite canonical system ⋮ On the modelling of search in theorem proving -- towards a theory of strategy analysis ⋮ A Wos Challenge Met ⋮ Automated proofs of equality problems in Overbeek's competition

Uses Software

• SbReve2

Cites Work

• Termination of rewriting
• Case studies of Z-module reasoning: Proving benchmark theorems from ring theory
• Some experiments in nonassociative ring theory with an automated theorem prover
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Critical pair criteria for completion
• Complete Sets of Reductions for Some Equational Theories
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Automated proofs of the Moufang identities in alternative rings