Skip Navigation

Journal of Logic and Computation 2000 10(4):527-572; doi:10.1093/logcom/10.4.527
© 2000 by Oxford University Press
This Article
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Similar articles in ISI Web of Science
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by de Lima, E.
Right arrow Articles by Lingenfelder, C
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

Presentation of proofs in modal natural deduction

EF de LimaA1 and C LingenfelderA

A1 IMS - Institute for Natural Language Processing, University of Stuttgart, Azenbergstrasse 12, 70174 Stuttgart, Germany E-mail: delima@ims.uni-stuttgart.de, A IBM 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


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer:
Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.