Florian Meßner, Julian Parsert, Jonas Schöpf, Christian Sternagel
9th International Conference on Interactive Theorem Proving, Lecture Notes in Computer Science 10895, pp. 441 – 458, 2018.
pdf 
doi:10.1007/978-3-319-94821-8_26
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"}