Tactic-Based Theorem Proving and Knowledge-Based Forward Chaining: An Experiment with Nuprl and Ontic

http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR92-1276
unofficial copies [PDF], [PS]


by Wilfred Z. Chen

Proceedings of 11th International Conference on Automated Deduction, D. Kapur (ed.), LNCS 607, pp. 552-566, Springer-Verlag, (also Cornell TR 92-1276), 1992.

Abstract

We explore a new approach to interactive theorem proving which combines a knowledge-based notion of obvious reasoning with a tactic-based notion of obvious reasoning. We study the interplay of two particular systems and apply our approach to a proof of the Fundamental Theorem of Arithmetic. We achieve both shorter and more robust proofs. It is our opinion that the kind of control information contained in interactive proofs is a more important issue than their mere size. We analyze our proof scripts in terms of the control information they contain and suggest that stronger knowledge-based notions of obviousness and declarative representations of tactics are needed to further reduce low-level control information.