Automated Deduction in Arithmetic with the Omega Rule
S.R. Baker · 1993
An important technique for investigating derivability in formal systems of arithmetic has been to embed such systems into semiformal 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. This involves providing an appropriate representation for infinite proofs, and a means of verifying properties of such objects.