Oracle Integration of Floating-Point Solvers with Isabelle

EasyChair Preprint no. 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: floating-points, Sledgehammer, SMT solvers

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

  year = {EasyChair, 2022}}