7 citations · 11 across the 7 of their papers we have counts for
8 papers · 1 filter
A Free Group of Rotations of Rank 2
Jagadish Bapanapally, Ruben Gamboa
One of the key steps in the proof of the Banach-Tarski Theorem is the introduction of a free group of rotations. First, a free group of reduced words is generated where each elemen…
Using ACL2 To Teach Students About Software Testing
Ruben Gamboa, Alicia Thoney
We report on our experience using ACL2 in the classroom to teach students about software testing. The course COSC2300 at the University of Wyoming is a mostly traditional Discrete…
All Prime Numbers Have Primitive Roots
Ruben Gamboa, Woodrow Gamboa
If p is a prime, then the numbers 1, 2, ..., p-1 form a group under multiplication modulo p. A number g that generates this group is called a primitive root of p; i.e., g is such t…
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…
Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications
Grant Passmore, Ruben Gamboa
This volume contains a selection of papers presented at the 16th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2-2020). The workshops are the premier t…
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…