Automated Deduction in Arithmetic with the Omega Rule

Contents

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.