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

• Type: Conference
• Year: 2006
• Where: ACL2
• Authors: John R. Cowles, Ruben Gamboa
• Keywords: ACL2 2006, Computational Linguistics, Irreducible Polynomials, Positive Integers, Univariate Polynomials