Automatic Generation of Human Readable Proofs

Abstract

Declarative sentences are statements constructed from propositions that can be either true or false. To be easily manipulated by a program, we present a formal system for handling such declarative sentences called propositional logic. Currently, widely used methods for automatically generating proofs have readability limitations: the deduction process does not conform to human reasoning processes, or the proof tree generated is too complicated. The primary objective of this thesis is to design a program that automatically gen- erates human-readable propositional logic proofs using Natural Deduction. Natural Deduction is a calculus for deriving conclusions from a finite set of premises using proof rules. The deduction process is a tree structure with assumptions as leaves, natural deduction rules as nodes, and the conclusion as the root. This calculus mod- els human reasoning very well because it builds proofs incrementally using logical deductions from known facts and assumptions. Our approach will be capable of proving any valid sentence of Propositional Logic automatically and producing a proof tree in the Natural Deduction calculus.