Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor

Author(s):

Hustadt, Ullrich

dblp



Editor(s):

Bürckert, Hans-Jürgen
Nutt, Werner

dblp
dblp



BibTeX cite key*:

Hustadt93b

Title, Booktitle

Title*:

Automated Support for the Development of Non-classical Logics

Booktitle*:

Workshop: Modellierung epistemischer Propositionen, KI '93

Event, URLs

URL of the conference:


URL for downloading the paper:


Event Address*:


Language:

English

Event Date*
(no longer used):


Organization:


Event Start Date:

19 November 2019

Event End Date:

19 November 2019

Publisher

Name*:



URL:


Address*:

Berlin

Type:


Vol, No, Year, pp.

Series:


Volume:


Number:


Month:


Pages:


Year*:

1993

VG Wort Pages:


ISBN/ISSN:


Sequence Number:


DOI:




Note, Abstract, ©

Note:

To appear as Research Report of DFKI

(LaTeX) Abstract:

The most natural means for specifying a non-classical logic is by means of a Hilbert calculus. Usually, the semantics of a non-classical logic is given in terms of possible worlds. Given an axiomatization of a non-classical logics, the {\em correspondence problem} in these logics is to find for every given Hilbert axiom an equivalent property of the accessibility relation (van Benthem (1984)). For mechanizing deduction in non-classical logics it is very important to find these correspondences (Ohlbach (1991)). So far the method for finding the correspondences was mostly by intuition and the verification required complex proofs (van Benthem (1984)). SCAN is an algorithm which offers a method for computing the correspondences fully automatically. Moreover, since SCAN preserves equivalences, the computed correspondence axioms are {\em guaranteed to be complete} in the sense that a formula is derivable in the Hilbert calculus if and only if it is valid in the frames which are models
of the computed correspondence axiom. In this paper we present the SCAN algorithm and an application of it to the problem of collapsing modalities in multi-modal logics: Given a Hilbert calculus for modalities $\Box_{m_1}$ and $\Box_{m_2}$ we have to ensure that $$\Box_{m_1} P \Leftrightarrow \Box_{m_2} P$$ doesn't hold for all formulae $P$, because this is in general an unwanted consequence of the given axiomatization.



Download
Access Level:


Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

Audience:

experts only

Appearance:



BibTeX Entry:

@INPROCEEDINGS{Hustadt93b,
AUTHOR = {Hustadt, Ullrich},
EDITOR = {B{\"u}rckert, Hans-J{\"u}rgen and Nutt, Werner},
TITLE = {Automated Support for the Development of Non-classical Logics},
BOOKTITLE = {Workshop: Modellierung epistemischer Propositionen, KI '93},
YEAR = {1993},
ADDRESS = {Berlin},
NOTE = {To appear as Research Report of DFKI},
}


Entry last modified by Uwe Brahm/MPII/DE, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Uwe Brahm
Created
01/14/1995 06:52:04 PM
Revisions
2.
1.
0.

Editor(s)
Uwe Brahm/MPII/DE
Uwe Brahm/MPII/DE
Uwe Brahm/MPII/DE

Edit Dates
21/01/95 20:52:29
17/01/95 20:44:32
14/01/95 19:00:53