A formally verified solver for homogeneous linear Diophantine equations

DOI10.1007/978-3-319-94821-8_26MaRDI QIDQ1791187

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

Publication date: 4 October 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-94821-8_26

zbMATH Keywords

mechanized mathematics; code generation; Isabelle/HOL; homogeneous linear Diophantine equations; verified code

Mathematics Subject Classification ID

11Y50: Computer solution of Diophantine equations

68V20: Formalization of mathematics in connection with theorem provers

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Related Items

Diophantine

Uses Software

• Isabelle/HOL
• Isabelle/Isar
• CoLL