Department of Mathematics
Server

Mathematical induction is most commonly used to establish a given statement for all natural numbers. In spite of many recent developments in both hardware and software, a formal proof using mathematical induction, is still not that easy with first-order theorem-provers like Otter and Prover9. In this presentation, we reformulate a group-theoretical statement (proved by Hossein last month, [1]), involving n, an integer variable and make Prover9 give a formal proof for all n. Thus while it may take infinitely long time to prove the validity of the statement for say, n = 100, it takes a very short time to prove the same theorem for all n using the same Theorem-Prover. We show several examples from the literature in the areas of groups (with commutators) and rings (with additive commutators) which are ideal candidates for such experiments. This is part of an ongoing research done in collaboration with Dr. G. Moghaddam and Dr. Yang Zhang.

1. G. Moghaddam, On commutativity of cancellative semigroups, Rings and Modules Seminar, 29 March 2016
2. Yang Zhang, Automated Deduction in Ring Theory, ICMS Conference, Berlin, 2016.