A Formally Verified Solver for Homogeneous Linear Diophantine Equations
Florian Meßner, Julian Parsert, Jonas Schöpf, Christian Sternagel9th International Conference on Interactive Theorem Proving, Lecture Notes in Computer Science 10895, pp. 441 – 458, 2018.
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 for example 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.
BibTeX
@inproceedings{FMJPJSCS-ITP18,
author = "Florian Me\ss{}ner, Julian Parsert, Jonas Sch\"opf, Christian Sternagel",
title = "A Formally Verified Solver for Homogeneous Linear Diophantine Equations",
booktitle = "Proceedings of the 9th International Conference on Interactive Theorem Proving",
editor = "Jeremy Avigad and Assia Mahboubi",
series = "Lecture Notes in Computer Science",
volume = 10895,
pages = "441--458",
year = 2018,
doi = "10.1007/978-3-319-94821-8_26"
}