Home  Online Resources  Table of Contents

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: delima@ims.uni-stuttgart.de, 2IBM Germany, PO Box 13 80, 71003 Boeblingen, Germany, E-mail: lin@de.ibm.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

  Full-Text PDF  (423 KB)

[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 2000.