The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #645

Title:A Proof Environment for Arithmetic with the Omega Rule
Authors:Baker,S; Smaill,AD
Date:Sep 1993
Presented:To be published in Computer Science Logic'93, Swansea
Abstract:An important technique for investigating derivability in formal systems of arithmetic has been to embed such systems into semi-formal systems with the w-rule. This paper exploits this notion within the domain of automated theorem-proving and discusses the implementation of such a proof environment, namely the CORE system which implements a version of the primitive recursive w-rule. This involves providing an appropriate representation for infinite proofs, and a means of verifying properties of such objects. By means of the CORE system, from a finite number of instances a conjecture for a proof of the universally quantified formula is automatically derived by an inductive inference algorithm, and checked for correctness. In addition, candidates for cut formulae are generated by an explanation-based learning algorithm.

[Search These Pages] [DAI Home Page] [Comment]