Automated first order natural deduction
Alexander Bolotov, Vyacheslav Bocharov, A. Yu. Gorchakov, Vasilyi Shangin · WestminsterResearch (University of Westminster) · 2005
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.