4 citations · 7 across the 8 of their papers we have counts for
8 papers
Towards Automated Verification of Logarithmic Arithmetic
Mark G. Arnold, Thomas A. Bailey, John R. Cowles
Correctness proofs for floating point programs are difficult to verify. To simplify the task, a similar, but less complex system, known as logarithmic arithmetic can be used. The B…
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…
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…
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…
Perfect Numbers in ACL2
John Cowles, Ruben Gamboa
A perfect number is a positive integer n such that n equals the sum of all positive integer divisors of n that are less than n. That is, although n is a divisor of n, n is excluded…
Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent
Ruben Gamboa, John Cowles
The verification of many algorithms for calculating transcendental functions is based on polynomial approximations to these functions, often Taylor series approximations. However,…
Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis
John Cowles, Ruben Gamboa
ACL2(r) is a variant of ACL2 that supports the irrational real and complex numbers. Its logical foundation is based on internal set theory (IST), an axiomatic formalization of non-…
Verifying Sierpiński and Riesel Numbers in ACL2
John R. Cowles, Ruben Gamboa
A Sierpinski number is an odd positive integer, k, such that no positive integer of the form k * 2^n + 1 is prime. Similar to a Sierpinski number, a Riesel number is an odd positiv…