Automated deduction in ring theory

DOI10.1007/978-3-319-42432-3_9MaRDI QIDQ2819201zbMATH OpenOpenAlexFDO

Authors R. Padmanabhan, Yang Zhang

Publication date 28 September 2016

Published in Mathematical Software – ICMS 2016 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-42432-3_9

zbMATH Keywords

commutativityassociative ringsOtterProver9

Mathematics Subject Classification ID

Computational aspects of associative rings (general theory) (16Z05) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Automated proof of ring commutativity problems by algebraic methods
• Some experiments in nonassociative ring theory with an automated theorem prover
• Case studies of Z-module reasoning: Proving benchmark theorems from ring theory
• scientific article; zbMATH DE number 3870641
• Automated reasoning in reduction rings using the Theorema system

Cites work

• scientific article; zbMATH DE number 3534657 (Why is no real title available?)
• scientific article; zbMATH DE number 3282724 (Why is no real title available?)
• A Condition for the Commutativity of Rings
• An Anticommutativity Consequence of a Ring Commutativity Theorem of Herstein
• Automated deduction in equational logic and cubic curves
• Automated proof of ring commutativity problems by algebraic methods
• Derivations in Prime Rings
• On the Commutativity of Addition
• Solution of the Robbins problem
• Structure theory for algebraic algebras of bounded degree
• The Additive Group of an Infinite Near-Field is Abelian

Cited in

(14)

• scientific article; zbMATH DE number 3870641 (Why is no real title available?)
• Automated Reasoning in Higher-Order Regular Algebra
• Superposition theorem proving for commutative rings
• Automated proofs of the Moufang identities in alternative rings
• Automated proof of ring commutativity problems by algebraic methods
• Automated reasoning with power maps
• scientific article; zbMATH DE number 4068331 (Why is no real title available?)
• Automatic Abstraction for Congruences
• Case studies of Z-module reasoning: Proving benchmark theorems from ring theory
• Some experiments in nonassociative ring theory with an automated theorem prover
• Automated reasoning in reduction rings using the Theorema system
• Z-module reasoning
• Formalizing ring theory in PVS
• Automated deduction with associative-commutative operators

Describes a project that uses

Uses Software

• OTTER
• Prover9
• Mace4

This page was built for publication: Automated deduction in ring theory

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