Document Type

Technical Report

Publication Date

5-5-2004

Subjects

Debugging in computer science, Computer logic, Automatic theorem proving, Formal methods (Computer science)

Abstract

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.

Description

Portland State University Computer Science Department Technical Report #08-01, May 2004..

Persistent Identifier

https://archives.pdx.edu/ds/psu/30740

Download

Share

COinS