Campus Event Calendar
Event Entry
What and Who
Backward translations for modal logics
Stephane Demri
L.I.F.I.A. Grenoble
Logik-Seminar
AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, RG1, SWS
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 24 October 95
16:15
60 Minutes
44 - MPII
117
Saarbrücken
Abstract
Methods for automated deduction for non classical logics can be
broadly divided in two categories: the direct approach (construction
of specific proof systems for the non classical logics) and the
translation approach (translation between a source logic and a
target logic). One of the advantages of the approach by translation
lies on the use of a theorem prover dedicated to the target logic
(for instance the classical first-order logic) in order to solve
problems initially expressed in the source logic (for instance the
modal logic S4). However the presentation of (partial) proofs in
calculi of the source logic remains an aspect of the translation
approach that has been generally neglected. A hierarchy of backward
translations is given in the talk in order to present different
types of information that can be recovered in the source logics.
The backward translations are then classified with respect to the
information retrieved from the target logics. Partial backward
translations for some usual propositional modal logics are discussed,
involving resolution and tableaux calculi. Different examples
illustrate the construction of (partial) proofs in the source logics.
broadly divided in two categories: the direct approach (construction
of specific proof systems for the non classical logics) and the
translation approach (translation between a source logic and a
target logic). One of the advantages of the approach by translation
lies on the use of a theorem prover dedicated to the target logic
(for instance the classical first-order logic) in order to solve
problems initially expressed in the source logic (for instance the
modal logic S4). However the presentation of (partial) proofs in
calculi of the source logic remains an aspect of the translation
approach that has been generally neglected. A hierarchy of backward
translations is given in the talk in order to present different
types of information that can be recovered in the source logics.
The backward translations are then classified with respect to the
information retrieved from the target logics. Partial backward
translations for some usual propositional modal logics are discussed,
involving resolution and tableaux calculi. Different examples
illustrate the construction of (partial) proofs in the source logics.
Contact
Uwe Waldmann
(0681) 302-5431
--email hidden
passcode not visible
logged in users only
Tags, Category, Keywords and additional notes
modal logics