Top

Published in:

2016 | OriginalPaper | Chapter

Automated Deduction in Ring Theory

Authors : Ranganathan Padmanabhan, Yang Zhang

Published in: Mathematical Software – ICMS 2016

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Pover9/Mace4 or its predecessor Otter is one of the powerful automated theorem provers for first-order and equational logic. In this paper we explore various possibilities of using Prover9 in ring theory and semiring theory, in particular, associative rings, rings with involutions, semirings with cancellation laws and near-rings. We code the corresponding axioms in Prover9, check some well-known theorems, for example, Jacobson’s commutativity theorem, give some new proofs, and also present some new results.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0

next chapter Agent-Based HOL Reasoning

Fitelson, B.: Using Wolfram’s mathematica to understand the computer proof of Robbin’s conjecture. Math. Educ. Res. 7(1), 17–26 (1998)

Herstein, I.K.: Noncommutative rings, No. 15. In: Carus Mathematical Monographs. American Mathematical Society (1968)

Herstein, I.K.: Topics in Algebra, 2nd edn. Wiley, Toronto (1975). Copyright: Xerox Corporation (1975)MATH

Herstein, I.K.: A condition for the commutativity of rings. Canad. J. Math. 9, 583–586 (1957)MathSciNetCrossRefMATH

Herstein, I.K.: Rings with Involution. University of Chicago, Chicago (1976)MATH

Jacobson, N.: Structure theory for algebraic algebras of bounded degree. Ann. Math. 46(2), 695–707 (1945)MathSciNetCrossRefMATH

MacHale, D.: An anticommutativity consequence of a ring commutativity theorem of Herstein. Amer. Math. Monthly 94(2), 162–165 (1987)MathSciNetCrossRefMATH

McCune, W.: Solution of Robbin’s problem. J. Automat. Reason 19, 263–276 (1997)MathSciNetCrossRefMATH

McCune, W.: Otter 3.3 Reference Manual and Guide, Argonne National Laboratory Technical Memorandum ANL/MCS-TM-263 (2003)

10.

McCune, W.: Prover9, automated reasoning software, and Mace4, finite model builder, Argonne National Laboratory (2005). https://www.cs.unm.edu/~mccune/mace4/

11.

McCune, W., Padmanabhan, R. (eds.): Automated Deduction in Equational Logic and Cubic Curves. LNCS (LNAI), vol. 1095. Springer, Heidelberg (1996)MATH

12.

Neumann, B.H.: On the commutativity of addition. J. London Math. Soc. 15, 203–208 (1940)MathSciNetCrossRefMATH

13.

Phillips, J.D., Stanovsky, D.: Automated theorem proving in loop theory. In: Proceedings of ESARM 2008, pp. 42–54 (2008)

14.

Posner, E.C.: Derivations in prime rings. Proc. Amer. Soc. 8(6), 1093–1100 (1957)MathSciNetCrossRefMATH

15.

Wavrik, J.J.: Commutativity theorems: examples in search of algorithms. In: Proceedings of 1999 International Symposium on Symbolic and Algebraic Computations, pp. 31–36. ACM (1999)

16.

Zhang, H.: Automated proof of ring commutativity problems by algebraic methods. J. Symbolic Comput. 9, 423–427 (1990)MathSciNetCrossRefMATH

17.

Zemmer, J.L.: The addition group of an infinite near-field is abelian. J. London Math. Soc. 44, 65–67 (1969)MathSciNetCrossRefMATH

Title: Automated Deduction in Ring Theory
Authors: Ranganathan Padmanabhan
Yang Zhang
Publisher: Springer International Publishing
Book: Mathematical Software – ICMS 2016
Print ISBN: 978-3-319-42431-6

Electronic ISBN: 978-3-319-42432-3

Copyright Year: 2016
DOI: https://doi.org/10.1007/978-3-319-42432-3_9

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner