Abstract
An important technique for investigating derivability in formal systems of arithmetic has been to embed such systems into semiformal systems with the Ω-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 Ω-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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Baker, S.: Aspects of the Constructive Omega Rule within Automated Deduction. PhD thesis, University of Edinburgh (1992)
Baker, S.: CORE manual. Technical Paper 10, Dept. of Artificial Intelligence, Edinburgh (1992)
Baker, S.: A new application for explanation-based generalisation within automated deduction. In A. Bundy, editor, 12th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Springer-Verlag (1994) 177–191. Also available from Cambridge as Computer Laboratory Technical Report 327.
Bundy, A., van Harmelen, F., Horn, C., and Smaill, A.: The Oyster-Clam system. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Springer-Verlag 449 (1990) 647–648
Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence, 62 (1993) 185–253
Dummett, M.: Elements of Intuitionism. Oxford Logic Guides. Oxford Univ. Press, Oxford (1977)
Feferman, S.: Transfinite recursive progressions of axiomatic theories. Journal of Symbolic Logic 27 (1962) 259–316
Gordon, M.: HOL: A proof generating system for higher-order logic. In G. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, Kluwer (1988)
Kreisel, G.: Mathematical logic. In T.L. Saaty, editor, Lectures on Modern Mathematics, John Wiley and Sons III (1965) 95–195
Löpez-Escobar, E.G.K.: On an extremely restricted Ω-rule. Fundamenta Mathematicae 90 (1976) 159–72
Mitchell, T.M.: Toward combining empirical and analytical methods for inferring heuristics. Technical Report LCSR-TR-27, Laboratory for Computer Science Research, Rutgers University (1982)
Nelson, G.C.: A further restricted Ω-rule. Colloquium Mathematicum 23 (1971)
Plotkin, G.: A note on inductive generalization. In D. Michie and B. Meltzer, editors, Machine Intelligence, Edinburgh University Press 5 (1969) 153–164
Prawitz, D.: Ideas and results in proof theory. In J.E. Fenstad, editor, Studies in Logic and the Foundations of Mathematics: Proceedings of the Second Scandinavian Logic Symposium, North Holland 63 (1971) 235–307
Rosser, B.: Gödel-theorems for non-constructive logics. JSL 2 (1937) 129–137
Rouveirol, C.: Saturation: Postponing choices when inverting resolution. In Proceedings of ECAI-90, Stockholm (1990) 557–562
Schütte, K.: Proof Theory. Springer-Verlag (1977)
Schwichtenberg, H.: Proof theory: Some applications of cut-elimination. In Barwise, editor, Handbook of Mathematical Logic, North-Holland (1977) 867–896
Shoenfield, J.R.: On a restricted Ω-rule. Bull. Acad. Sc. Polon. Sci., Ser. des sc. math., astr. et phys. 7 (1959) 405–7
Takeuti, G.: Proof theory. North-Holland, 2 edition (1987)
Tucker, J.V., Wainer, S.S., Zucker, J.I.: Provable computable functions on abstract-data-types. In M.S. Paterson, editor, Automata, Languages and Programming, Lecture Notes in Computer Science, Springer-Verlag 443 (1990) 660–673
Yoccoz, S.: Constructive aspects of the omega-rule: Application to proof systems in computer science and algorithmic logic. Lecture Notes in Computer Science, Springer-Verlag 379 (1989) 553–565
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baker, S., Smaill, A. (1995). A proof environment for arithmetic with the omega rule. In: Calmet, J., Campbell, J.A. (eds) Integrating Symbolic Mathematical Computation and Artificial Intelligence. AISMC 1994. Lecture Notes in Computer Science, vol 958. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60156-2_9
Download citation
DOI: https://doi.org/10.1007/3-540-60156-2_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60156-2
Online ISBN: 978-3-540-49533-8
eBook Packages: Springer Book Archive