Automated first order natural deduction

Abstract

We present a proof-searching algorithm for the classical first order natural deduction calculus and prove its correctness. For any given task (if this task is indeed solvable), a searching algorithm terminates, either finding a corresponding natural deduction proof or giving a set of constraints, from which a counter-example can be extracted. Proofs of the properties which characterize correctness of the searching algorithm are given. Based on a fully automatic goal-directed searching procedure, our technique can be efficiently applied as an automatic reasoning tool in a deliberative decision making framework across various AI applications.