IsaAbduct: A Multi-Strategy Abduction Pipeline for Isabelle/HOL

Abstract

Isabelle/HOL is a widely used proof assistant for higher-order logic. However, constructing an Isabelle/HOL proof is not always straightforward. In particular, the user may not know which intermediate lemmas or assumptions are required. A common situation is that a user attempts a proof, the automated reasoning tools fail to find one, and the system returns only “No proof found.” This can be frustrating. A more helpful outcome would provide insight into (1) what is missing or (2) which reasoning steps the automated tools attempted. The first aspect corresponds to abduction: finding additional premises that would make the goal provable. The second aspect can be supported by reporting the facts that were relevant during the (ultimately unsuccessful) proof search. In this work, we present IsaAbduct, a new command for Isabelle/HOL that integrates an abductive reasoning engine to suggest plausible missing assumptions and to provide additional feedback about the proof search process. The command is based on the syntax-guided synthesis (SyGuS) solver cvc5 and the saturation-based prover E, and operates by exchanging grammar-based hypotheses from cvc5’s enumeration and relevant facts extracted from E’s saturation search, so that cvc5 and E synergistically guide each other’s progress. Our evaluation shows that IsaAbduct produces a variety of useful hypotheses for the user and indicates that the different backend configurations are complementary: the integrated approach leads to higher-quality suggestions in comparison with using either the cvc5 or the E pipeline in isolation. Index Terms—abduction; proof assistants; Isabelle/HOL; SMT; saturation.