Olle Torstensson and Tjark Weber. In Uli Sattler and Martin Suda, editors, Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20-22, 2023, Proceedings, volume 14279 of Lecture Notes in Computer Science, pages 217-235. Springer, 2023.
Sledgehammer, a component of the interactive proof assistant Isabelle/HOL, aims to increase proof automation by automatically discharging proof goals with the help of external provers. Among these provers are a group of satisfiability modulo theories (SMT) solvers with support for the SMT-LIB input language. Despite existing formalizations of IEEE floating-point arithmetic in both Isabelle/HOL and SMT-LIB, Sledgehammer employs an abstract translation of floating-point types and constants, depriving the SMT solvers of the opportunity to make use of their dedicated decision procedures for floating-point arithmetic.
We show that, by extending Sledgehammer's translation from the language of Isabelle/HOL into SMT-LIB with an interpretation of floating- point types and constants, floating-point reasoning in SMT solvers can be made available to Isabelle/HOL. Our main contribution is a description and implementation of such an extension. An evaluation of the extended translation shows a significant increase of Sledgehammer's success rate on proof goals involving floating-point arithmetic.
@inproceedings{torstensson23hammering,
author = {Olle Torstensson and Tjark Weber},
title = {Hammering Floating-Point Arithmetic},
editor = {Uli Sattler and Martin Suda},
booktitle = {Frontiers of Combining Systems~- 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September~20-22, 2023, Proceedings},
volume = {14279},
series = {Lecture Notes in Computer Science},
pages = {217--235},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-43369-6\_12},
doi = {10.1007/978-3-031-43369-6\_12}
}