Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic.

Wilfred Z. Chen

Browse the full CADE paper archive.