Automated Deduction in Ring Theory

DOI10.1007/978-3-319-42432-3_9zbMath1434.68642MaRDI QIDQ2819201

Yang Zhang, R. Padmanabhan

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

commutativity; associative rings; Otter; Prover9

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

16Z05: Computational aspects of associative rings (general theory)

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Uses Software

• OTTER
• Prover9
• Mace4