Toward a Sound Integration of Isabelle with a Combined Decision Procedure

I present work on a project to integrate Isabelle, an extremely versatile interactive proof assistant, with a combined decision procedure, the Cooperating Validity Checker (CVC). Isabelle is sound and flexible, however it is often tedious to use. CVC is fully automatic, but only handles decision problems expressible over a relatively weak set of theories including linear arithmetic, uninterpreted functions, data types, and firstorder quantifier-free logic. My goal is to increase the amount of automation in Isabelle, by making it use CVC as an oracle for such problems, but without compromising Isabelle’s soundness. In this paper I report on the progress made toward this goal. The key to retaining soundness is in CVC’s ability to produce proofs. I have implemented a basic infrastructure to translate these proofs into Isabelle tactics. This effort has revealed a number of issues that complicate the translation. One complication is an unwanted conversion from a logic of partial functions to classical logic. Another is the unsoundness off the CVC proof system, which makes part of a CVC proof unusable. Fortunately, we can regenerate the unusable part by mimicking CVC’s conversion. The current state of the project includes a detailed plan to work around the complications, and a partial implementation that handles part of first-order quantifier-free logic