Journal of Logic and Computation, Volume 10, Issue 4, pp. 527-572: Abstract.
Presentation of proofs in modal natural deduction
EF de Lima1 and C Lingenfelder2
1IMS - Institute for Natural Language Processing, University of Stuttgart, Azenbergstrasse 12, 70174 Stuttgart, Germany, E-mail: firstname.lastname@example.org, 2IBM Germany, PO Box 13 80, 71003 Boeblingen, Germany, E-mail: email@example.com
We introduce a calculus for transforming first-order proofs of theorems originally formulated in modal logic, into modal natural deduction proofs. With a transformation procedure based on this calculus, we are able to present a proof in the language in which the problem was originally formulated, and in a formalism giving better insight into the contents of the proof. As a target language of the proof transformation we use a linearized modal natural deduction calculus which makes the reasoning involving modal contexts explicit.
Keywords: modal logic, modal natural deduction, theorem proving, proof transformation