A Formally Verified Solver for Homogeneous Linear Diophantine Equations

Title:A Formally Verified Solver for Homogeneous Linear Diophantine Equations

Authors:Florian Meßner, Julian Parsert, Jonas Schöpf and Christian Sternagel

Conference:ITP 2018

Tags:certified algorithm, certified code, check phase, code generation, computer science, dot product, elementary ac unification problem, formal proof, generate check, homogeneous linear diophantine equations, improved bound, Isabelle/HOL, linear diophantine equation, mechanized mathematics, minimal complete set, minimal solution, minimization phase, reverse lexicographic order, special solution and static bound

Abstract:

In this work we are interested in minimal complete sets of solutions for homogeneous linear diophantine equations. Such equations naturally arise during AC-unification, that is, unification in the presence of associative and commutative symbols. Minimal complete sets of solutions are required to compute AC-critical pairs. We present a verified solver for homogeneous linear diophantine equations that we formalized in Isabelle/HOL. Our work provides the basis for formalizing AC-unification and will eventually enable the certification of automated AC-confluence and AC-completion tools.