Tactic-Based Theorem Proving and Knowledge-Based Forward Chaining: An Experiment with Nuprl and Ontic
by Wilfred Z. Chen
Proceedings of 11th International Conference on Automated Deduction
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.
bibTex ref: Chen92