Generic Automatic Proof Tools

TL;DR

This chapter explores the integration of Isabelle's classical reasoner with traditional tableau and resolution methods, demonstrating its effectiveness through a case study on the Church-Rosser theorem for combinators.

Contribution

It introduces a high-automation classical reasoner within Isabelle, bridging interactive proof tools with classical theorem proving techniques.

Findings

Isabelle's classical reasoner achieves high automation.

Successful demonstration with the Church-Rosser theorem.

Establishes connections between Isabelle and classical proof methods.

Abstract

This book chapter establishes connections between the interactive proof tool Isabelle and classical tableau and resolution technology. Isabelle's classical reasoner is described and demonstrated by an extended case study: the Church-Rosser theorem for combinators. Compared with other interactive theorem provers, Isabelle's classical reasoner achieves a high degree of automation.