[isabelle] New AFP entry: Homogeneous Linear Diophantine Equations



Homogeneous Linear Diophantine Equations
Florian Messner, Julian Parsert, Jonas SchÃpf and Christian Sternagel

We formalize the theory of homogeneous linear diophantine equations, focusing on two main results: (1) an abstract characterization of minimal complete sets of solutions, and (2) an algorithm computing them. Both, the characterization and the algorithm are based on previous work by Huet. Our starting point is a simple but inefficient variant of Huet's lexicographic algorithm incorporating improved bounds due to Clausen and Fortenbacher. We proceed by proving its soundness and completeness. Finally, we employ code equations to obtain a reasonably efficient implementation. Thus, we provide a formally verified solver for homogeneous linear diophantine equations.

https://www.isa-afp.org/entries/Diophantine_Eqns_Lin_Hom.html

Enjoy!

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.