Campus Event Calendar

Event Entry

What and Who

Backward translations for modal logics

Stephane Demri
L.I.F.I.A. Grenoble
AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, RG1, SWS  
AG Audience

Date, Time and Location

Tuesday, 24 October 95
60 Minutes
44 - MPII


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.


Uwe Waldmann
(0681) 302-5431
--email hidden
passcode not visible
logged in users only

Tags, Category, Keywords and additional notes

modal logics