Oracle Integration of Floating-Point Solvers with Isabelle

EasyChair Preprint 8640

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.

Keyphrases: SMT solvers, Sledgehammer, floating-points

@booklet{EasyChair:8640,
  author    = {Olle Torstensson and Tjark Weber},
  title     = {Oracle Integration of Floating-Point Solvers with Isabelle},
  howpublished = {EasyChair Preprint 8640},
  year      = {EasyChair, 2022}}