Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-40240
Titel: Context Logic
VerfasserIn: Ohlbach, Hans Jürgen
Sprache: Englisch
Erscheinungsjahr: 1989
Erscheinungsort: Kaiserslautern
Freie Schlagwörter: Automated Theorem Proving by Translation and Refutation
Resolution
Nonclassical Logics
Modal Logic
Temporal Logic
Process Logic
Epistemic Logic
Action Logic
CTL
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: Context Logic (CL) is a logic in the original sense, but more than that, it is a methodology for designing a certain class of logics in such a way that automatically a first-order many-sorted resolution and paramodulation calculus is obtained. This calculus can be executed on a clause based predicate logic theorem prover. The class of logics which can be handled with the CL-methodology is mainly characterized by the existence of “hidden parameters”, parameters like worlds in modal logics defining the context in which the terms and formulae are to be interpreted. The hidden parameters are usually determined implicitly by additional logical operators like for example □ (necessarily) and ◊ (possibly) in modal logic. These operators refer to an underlying semantical structure - Kripke’s possible worlds structure in the case of modal logic, time points and time intervals in the case of temporal logic are examples. CL provides a means for axiomatizing these structures and for expressing the semantics of the desired operators in a formal language. This information about the desired logic is sufficient to translate formulae written in the operator syntax automatically into predicate logic syntax where the operators are replaced by quantifiers and the hidden parameters are made an explicit part of the formula. After the translation, information about a whole bunch of nested operators is shifted into one “context term” that can be handled by an appropriate unification algorithm. Hence, a resolution step may exploit information about many nested operators at once and is therefore much more goal directed than a corresponding step in a tableaux system for example. The main limits of CL are: • Since predicate logic is the “target logic” into which the designed logic is mapped, in order to obtain a complete calculus, its semantical structure must be first-order axiomatizable. This excludes certain properties like discreteness and finiteness. • Due to the current limits of predicate logic resolution (no partial functions allowed for example) two further assumptions are still necessary. For Kripke structures these are the constant-domain assumption and the seriality assumption. For other structures the assumptions are analogous. In order to demonstrate the method, a quite complex first-order many-sorted multi modal logic with operators indexed with arbitrary (possibly non-ground) terms is constructed using the CL tools. The logic is actually an extension of Clarke and Emerson’s CTL temporal logic. Therefore, as a side effect, we get a proof theory for CTL.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-402407
hdl:20.500.11880/36252
http://dx.doi.org/10.22028/D291-40240
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 89,8
Datum des Eintrags: 14-Aug-2023
Fakultät: SE - Sonstige Einrichtungen
Fachrichtung: SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
Professur: SE - Sonstige
Sammlung:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Dateien zu diesem Datensatz:
Datei Beschreibung GrößeFormat 
SEKI-Report-SR-89-08_Ohlbach_Context-Logic.pdf6,28 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.