A proof environment for arithmetic with the omega rule

Siani Baker, Alan Smaill

Research output: Book/ReportBook

Abstract

An important technique for investigating derivability in formal systems of arithmetic has been to embed such systems into semiformal systems with the Ω-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 Ω-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 may be generated by an explanation-based learning algorithm. This is an alternative approach to reasoning about inductively defined domains from traditional structural induction, which may sometimes be more intuitive.
Original languageEnglish
PublisherSpringer-Verlag
Number of pages15
Publication statusPublished - 1994

Fingerprint Dive into the research topics of 'A proof environment for arithmetic with the omega rule'. Together they form a unique fingerprint.

Cite this