Automated Deduction in Ring Theory
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 rin
- PDF / 157,278 Bytes
- 8 Pages / 439.37 x 666.142 pts Page_size
- 4 Downloads / 219 Views
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.
Keywords: Prover9
1
· Otter · Commutativity · Associative rings
Introduction
It is well-known that automated reasoning tools have been widely used in many areas such as lattice theory, loop algebra, group theory, which provide powerful methods to check or simplify the proofs, prove or construct counter-examples for conjectures, and discover the new theorems, see, for example, McCune and Padmanabhan [11] and Phillips and Stanovsky [13]. Pover9/Mace4 [10] or its predecessor Otter [9] is one of the powerful automated theorem provers for first-order and equational logic. To our best knowledge, only few papers considered how to use Prover9 in ring theory. In non-commutative rings, one of significant difficult points is to construct some conter-examples, which is almost impossible to do that by hand. Now using Mace4, many examples can be constructed quickly. The purpose of this paper is to explore various possibilities of using Prover9 in ring theory, in particular, associative rings, rings with involutions, rings with derivations and near-rings. We code the corresponding axioms in Prover9, check some well-known theorems, give some new proofs, and also discuss some conjectures. This paper is self-contained in that we do not assume that the reader is familiar with ring theory or Prover9. We provide some Prover9 commands in ring theory, and expect that other researchers can use Prover9 in their research works easily. c Springer International Publishing Switzerland 2016 G.-M. Greuel et al. (Eds.): ICMS 2016, LNCS 9725, pp. 67–74, 2016. DOI: 10.1007/978-3-319-42432-3 9
68
R. Padmanabhan and Y. Zhang
In Sect. 2, we first code the axioms of associative rings in Prover9, and then prove Jacobson’s commutativity theorem, as well as other commutativity theorems. The similar theorems in rings with involutions and derivations as well as near-rings are discussed in Sect. 3. Finally some new results in semirings are presented in Sect. 4. All results in this paper are tested in iMac 3.06 GHz. Prover9’s default termordering is LPO but KBO (Knuth-Bendix) is sometimes preferable. For associative rings, KBO usually finds direct proofs (instead of indirect proofs via contradictions).
2
Commutativity in Associative Rings
When we study polynomial identities in non-commutative rings, one interesting question is that a ring will be commutative if its elements satisfy a polynomial identity. The summary of early work can be found in Herstein’s books [2,3]. Since then, many people have worked in this area and various identitie
Data Loading...
