登入
選單
返回
Google圖書搜尋
A Proof Environment for Arithmetic with the Omega Rule
Siani L. Baker
Alan Smaill
University of Edinburgh. Department of Artificial Intelligence
出版
University of Cambridge Computer Laboratory
, 1993
URL
http://books.google.com.hk/books?id=8E0kAQAAIAAJ&hl=&source=gbs_api
註釋
Abstract: "An important technique for investigating derivability in formal systems of arithmetic has been to embed such systems into semi- formal systems with the [omega]-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 [omega]-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."