Technical reports

A proof environment for arithmetic with the Omega rule

Siani L. Baker

August 1994, 17 pages

DOI: 10.48456/tr-345

Abstract

An important technique for investigating the derivability in formal systems of arithmetic has been to embed such systems into semi-formal 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 of the 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 traditionas structural induction, which may sometimes be more intuitive.

Full text

PDF (1.4 MB)

BibTeX record

@TechReport{UCAM-CL-TR-345,
  author =	 {Baker, Siani L.},
  title = 	 {{A proof environment for arithmetic with the Omega rule}},
  year = 	 1994,
  month = 	 aug,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-345.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-345},
  number = 	 {UCAM-CL-TR-345}
}