Please use this identifier to cite or link to this item: doi:10.22028/D291-40240
Title: Context Logic
Author(s): Ohlbach, Hans Jürgen
Language: English
Year of Publication: 1989
Place of publication: Kaiserslautern
Free key words: Automated Theorem Proving by Translation and Refutation
Nonclassical Logics
Modal Logic
Temporal Logic
Process Logic
Epistemic Logic
Action Logic
DDC notations: 004 Computer science, internet
Publikation type: Report
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 to this record: urn:nbn:de:bsz:291--ds-402407
Series name: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Series volume: 89,8
Date of registration: 14-Aug-2023
Faculty: SE - Sonstige Einrichtungen
Department: SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
Professorship: SE - Sonstige
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
SEKI-Report-SR-89-08_Ohlbach_Context-Logic.pdf6,28 MBAdobe PDFView/Open

Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.