Sciweavers

Share
ACL2
2006
ACM

Unique factorization in ACL2: Euclidean domains

9 years 7 months ago
Unique factorization in ACL2: Euclidean domains
ACL2 is used to systematically study domains whose elements can be “uniquely” factored into products of “irreducible” elements. The best known examples of such domains are the positive integers, which can be factored into products of primes, and univariate polynomials with rational coefficients, which can be factored into products of irreducible polynomials. There are many other such domains. n domains are an algebraic abstraction, of both the positive integers and the rational polynomials, in which the usual proofs of unique factorization, for both the integers and the polynomials, can be generalized. Categories and Subject Descriptors F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic—Mechanical theorem proving, Computational logic General Terms Verification Keywords Boyer-Moore logic,unique factorization, Euclidean domains, ACL2
John R. Cowles, Ruben Gamboa
Added 13 Jun 2010
Updated 13 Jun 2010
Type Conference
Year 2006
Where ACL2
Authors John R. Cowles, Ruben Gamboa
Comments (0)
books