Theorems from compiler verification: a problem set for automated theorem provers

Abstract

The paper describes a large experiment in using automated theorem provers on first-order goals that showed up in a KIV case study on the verification of a Prolog compiler. Based on an algebraic specification with 456 axioms, 580 theorems were proven in KIV. For the theorems using induction, additional goals were generated for induction bases and steps, resulting in 733 noninductive goals. These were given to Otter, Setheo and Spass in several versions: with and without an axiom reduction preprocessing step, and with and without a precedence order generated from the specification structure. Test files are available in Otter syntax, as Setheo clauses and in the common syntax of the DFG-Schwerpunkt "Deduktion", which is used by Spass.