A proof environment for arithmetic with the omega rule

Siani Baker, Alan Smaill

Research output: Book/ReportBook


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
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