Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Homogeneous Linear Diophantine ...


view this post on Zulip Email Gateway (Aug 22 2022 at 16:16):

From: Tobias Nipkow <nipkow@in.tum.de>
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!
smime.p7s


Last updated: Mar 28 2024 at 08:18 UTC