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

## by Wilfred Z. Chen

1992

Proceedings of 11th International Conference on Automated Deduction

- Tech Report TR92-1276: http://hdl.handle.net/1813/7116
- unofficial copies PDF, PS

**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.

**bibTex ref: Chen92**

cite link