|
Homogeneous
Linear
Diophantine
Equations
Title: |
Homogeneous Linear Diophantine Equations |
Authors:
|
Florian Messner (florian /dot/ g /dot/ messner /at/ uibk /dot/ ac /dot/ at),
Julian Parsert (julian /dot/ parsert /at/ gmail /dot/ com),
Jonas Schöpf (jonas /dot/ schoepf /at/ uibk /dot/ ac /dot/ at) and
Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com)
|
Submission date: |
2017-10-14 |
Abstract: |
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. |
BibTeX: |
@article{Diophantine_Eqns_Lin_Hom-AFP,
author = {Florian Messner and Julian Parsert and Jonas Schöpf and Christian Sternagel},
title = {Homogeneous Linear Diophantine Equations},
journal = {Archive of Formal Proofs},
month = oct,
year = 2017,
note = {\url{http://isa-afp.org/entries/Diophantine_Eqns_Lin_Hom.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
GNU Lesser General Public License (LGPL) |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|