cl-banner

A Formally Verified Solver for Homogeneous Linear Diophantine Equations

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.

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.

 

  PDF |    doi:10.1007/978-3-319-94821-8_26  

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"
}
Nach oben scrollen