Automated Deduction in Arithmetic with the Omega Rule

Siani Baker

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.