Journal of Formalized Reasoning
https://jfr.unibo.it/
Journal of Formalized Reasoning (JFR) – ISSN 1972-5787 encourages submission of papers describing significant, automated or semi-automated formalization efforts in any area, including classical mathematics, constructive mathematics, formal algorithms, and program verification. The emphasis of the journal is on proof techniques and methodologies and their impact on the formalization process. In particular, the journal provides a forum for comparing alternative approaches, enhancing reusability of solutions and offering a clear view of the current state of the field.en-US Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions. This journal is licensed under a Creative Commons Attribution 3.0 Unported License ( full legal code ). See also our Open Access policy asperti@cs.unibo.it (Prof. Andrea Asperti)ojs@unibo.it (OJS Support)Tue, 19 Feb 2019 10:26:25 +0100OJS 2.4.8.2http://blogs.law.harvard.edu/tech/rss60Commutativity Theorems in Groups with Power-like Maps
https://jfr.unibo.it/article/view/8751
There are several commutativity theorems in groups and rings which involve power maps f(x) = x<sup>n</sup>. The most famous example of this kind is Jacobson's theorem which asserts that any ring satisfying the identity x<sup>n</sup> = x is commutative. Such statements belong to first order logic with equality and hence provable, in principle, by any first-order theorem-prover. However, because of the presence of an arbitrary integer parameter n in the exponent, they are outside the scope of any first-order theorem-prover. In particular, one cannot use such an automated reasoning system to prove theorems involving power maps. Here we focus just on the needed properties of power maps f(x) = x<sup>n</sup> and show how one can avoid having to reason explicitly with integer exponents. Implementing these new equational properties of power maps, we show how a theorem-prover can be a handy tool for quickly proving or confirming the truth of such theorems.Ranganathan Padmanabhan, Yang Zhang
Copyright (c) 2019 R Padmanabhan, Yang Zhang
http://creativecommons.org/licenses/by/3.0
https://jfr.unibo.it/article/view/8751Tue, 19 Feb 2019 10:26:24 +0100