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öße | Format | |
---|---|---|---|---|
SEKI-Report-SR-89-08_Ohlbach_Context-Logic.pdf | 6,28 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.