3 papers
cs.LO2020
Quadratic Extensions in ACL2
Ruben Gamboa, John Cowles, Woodrow Gamboa
Given a field K, a quadratic extension field L is an extension of K that can be generated from K by adding a root of a quadratic polynomial with coefficients in K. This paper shows…
cs.LO2018
The Fundamental Theorem of Algebra in ACL2
Ruben Gamboa, John Cowles
We report on a verification of the Fundamental Theorem of Algebra in ACL2(r). The proof consists of four parts. First, continuity for both complex-valued and real-valued functions…
cs.LO2017
The Cayley-Dickson Construction in ACL2
John Cowles, Ruben Gamboa
The Cayley-Dickson Construction is a generalization of the familiar construction of the complex numbers from pairs of real numbers. The complex numbers can be viewed as two-dimensi…