Olle Torstensson and Tjark Weber. EasyChair Preprint no. 8640, 2022. Presented at the Isabelle Workshop 2022 (associated with ITP 2022/FLoC 2022).
Sledgehammer, a component of the interactive proof assistant Isabelle, 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 the 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. 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-points. In particular, this enhancement enables Sledgehammer to prove more non-trivial goals -- thereby increasing proof automation for floating-point arithmetic in Isabelle.
@booklet{torstensson22oracle,
author = {Olle Torstensson and Tjark Weber},
title = {Oracle Integration of Floating-Point Solvers with {Isabelle}},
howpublished = {EasyChair Preprint no. 8640},
year = {2022},
note = {Presented at the Isabelle Workshop 2022 (associated with ITP 2022/FLoC 2022)},
url = {https://easychair.org/publications/preprint/VtNH}
}