Conversion of Resolution Proofs into Natural Deduction Proofs

摘要

The presentation of automatically generated proofs in a format comprehensible fora user is studied. The conversion of resolution proofs into natural deduction proofs is considered worth investigating because of its natural and human oriented proof methods. The relationship between a system I used by Uiterwijk and Gentzen's original more extensive natural deduction system NK and LK is described. The conversion of I-profs into LK-proofs and NK-proofs is shown. As a result, the conversion of resolution proofs into comprehensible natural deduction proofs become feasible. A high level overview of a computer program that effectuates this conversion is given. Criteria for judging the comprehensibility of proofs are discussed.