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...
On the lines of the binary gcd algorithm for rational integers, algorithms for computing the gcd are presented for the ring of integers in Q( √ d) where d ∈ {−2, −7, −11,...