Division of Informatics

Forrest Hill & 80 South Bridge

## Research Paper #645 | |
---|---|

Title: | A Proof Environment for Arithmetic with the Omega Rule |

Authors: | Baker,S; Smaill,AD |

Date: | Sep 1993 |

Presented: | To be published in Computer Science Logic'93, Swansea |

Keywords: | |

Abstract: | An important technique for investigating derivability in formal systems of arithmetic has been to embed such systems into semi-formal 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, namely the CORE system which implements a version of the primitive recursive w-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 are generated by an explanation-based learning algorithm. |

Download: | NO ONLINE COPY |