Computational Natural Deduction

Abstract

The formalization of the notion of a logically sound argument as a natural deduction proof offers the prospect of a computer program capable of constructing such arguments for conclusions of interest. We present a constructive definition for a new subclass of natural deduction proofs, called atomic normal form (ANF) proofs. A natural deduction proof is readily understood as an argument leading from a set of premisses, by way of simple principles of reasoning, to the conclusion of interest. ANF extends this explanative power of natural deduction. The very detailed steps of the argument are replaced by derived rules of inference, each of which is justified by a particular input formula. ANF constitutes a proof theoretically well motivated normal form for natural deduction. Computational techniques developed for resolution refutation based systems are directly applicable to the task of constructing ANF proofs. We analyse a range of languages in this framework, extending from the simple Horn language to the full classical calculus. This analysis is applied to provide a natural deduction based account for existing logic programming languages, and to extend current logic programming implementation techniques towards more expressive languages. We consider the visualization of proofs, failure demonstrations, search spaces and the proof search process. Such visualization can be used for the purposes of explanation and to gain an understanding of the proof search process. We propose introspection based architecture for problem solvers based on natural deduction. The architecture offers a logic based meta language to overcome the combinatorial and other practical problems faced by the problem solver.