Automated proof of ring commutativity problems by algebraic methods

DOI10.1016/S0747-7171(08)80020-XMaRDI QIDQ912612zbMATH OpenFDO

Authors Hantao Zhang

Publication date 1990

Published in Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

Euclid's gcd algorithmNewton's binomial theoremring commutativity

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Center, normalizer (invariant elements) (associative rings and algebras) (16U70)

Recommendations

• scientific article; zbMATH DE number 3870641
• Automated deduction in ring theory
• scientific article; zbMATH DE number 33154
• scientific article; zbMATH DE number 66764
• scientific article; zbMATH DE number 16260

Cites work

• scientific article; zbMATH DE number 3870641 (Why is no real title available?)
• scientific article; zbMATH DE number 41806 (Why is no real title available?)
• History and basic features of the critical-pair/completion procedure
• Non-resolution theorem proving
• Problem corner: Reasoning about equality
• Structure theory for algebraic algebras of bounded degree

Cited in

(6)

• Theorem Proving in Higher Order Logics
• scientific article; zbMATH DE number 3870641 (Why is no real title available?)
• Automated deduction in ring theory
• Superposition theorem proving for commutative rings
• scientific article; zbMATH DE number 4036026 (Why is no real title available?)
• Some experiments in nonassociative ring theory with an automated theorem prover

This page was built for publication: Automated proof of ring commutativity problems by algebraic methods

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q912612)