### 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.

### License

GNU Lesser General Public License (LGPL)

### Topics

- Computer science/Algorithms/Mathematical
- Mathematics/Number theory
- Tools

### Session Diophantine_Eqns_Lin_Hom

- List_Vector
- Linear_Diophantine_Equations
- Sorted_Wrt
- Minimize_Wrt
- Simple_Algorithm
- Algorithm
- Solver_Code

## Cite

×

Diophantine_Eqns_Lin_Hom-AFP

    @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   = {October},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Diophantine_Eqns_Lin_Hom.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 15, 2017 : Isabelle2017