Oracle Integration of Floating-Point Solvers with Isabelle

Olle Torstensson and Tjark Weber. EasyChair Preprint no. 8640, 2022. Presented at the Isabelle Workshop 2022 (associated with ITP 2022/FLoC 2022).

Abstract

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.

Download

BibTeX

@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}
}

Last modified: 2022-08-11