Originaltitel:
Deductive Systems and the Decidability Problem for Hybrid Logics
Inhalt des Buches:
Dieses Buch steht an der Schnittstelle zweier Themen: der Entscheidbarkeit und der rechnerischen Komplexität hybrider Logiken und der für sie entworfenen deduktiven Systeme. Hybride Logiken werden hier in zwei Gruppen unterteilt: Standard-Hybridlogiken, die Nominale als Ausdrücke einer eigenen Art enthalten, und Nicht-Standard-Hybridlogiken, die keine Nominale enthalten, deren Ausdruckskraft aber der Ausdruckskraft von bindungsfreien Standard-Hybridlogiken entspricht. Die ursprünglichen Ergebnisse dieses Buches sind in zwei Teile aufgeteilt. Diese Aufteilung spiegelt die Aufteilung des Buches selbst wider. Die erste Art von Ergebnissen betrifft modelltheoretische und Komplexitätseigenschaften von hybriden Logiken. Da hybride Logiken, die wir als Standard bezeichnen, recht gut untersucht sind, konzentrierten sich die Bemühungen auf hybride Logiken, die in diesem Buch als Nicht-Standard bezeichnet werden. Nicht-Standard-Hybridlogiken werden als Modallogiken mit globalen Zähloperatoren (M(En)) verstanden, deren Ausdruckskraft der Ausdruckskraft von bindungsfreien Standard-Hybridlogiken entspricht. Die relevanten Ergebnisse umfassen: 1. die Etablierung einer soliden und vollständigen Axiomatisierung für die Modallogik K mit globalen Zähloperatoren (MK(En)), die leicht auf andere Rahmenklassen erweitert werden kann, 2.
Festlegung enger Komplexitätsgrenzen, nämlich NExpTime-Vollständigkeit für die modale Logik mit globalen Zähloperatoren, die über die Klassen beliebiger, reflexiver, symmetrischer, serieller und transitiver Rahmen (MK(En)), MT(En)), MD(En)), MB(En)), MK4(En)) mit binär kodierten numerischen Indizes definiert ist. Feststellung der Eigenschaft des Exponentialmodells für diese Logik, definiert über die Klassen der euklidischen und äquivalenten Rahmen (MK5(En)), MS5(En)). Die Ergebnisse des zweiten Typs bestehen im Entwurf konkreter deduktiver Systeme (Tableaus und Sequenzen) für Standard- und Nicht-Standard-Hybridlogiken. Genauer gesagt, umfassen sie: 1. Die Entwicklung eines vorangestellten und eines internalisierten Tableau-Kalküls, die für eine reiche Klasse von bindemittelfreien Standard-Hybrid-Logiken solide, vollständig und terminierend sind. Ein interessantes Merkmal der angegebenen Kalküle ist der nicht-verzweigende Charakter der Regel (D), 2. die Entwicklung eines vorangestellten und eines internalisierten Tableau-Kalküls, die solide, vollständig und terminierend für nicht-standardisierte hybride Logiken sind. Die Internalisierungstechnik, die auf ein Tableaukalkül für die Modallogik mit globalen Zähloperatoren angewendet wird, ist neu in der Literatur, 3. die Entwicklung des ersten hybriden Algorithmus, der einen Ungleichungslöser für Modallogiken mit globalen Zähloperatoren beinhaltet. Die Übertragung des arithmetischen Teils der Argumentation auf einen Ungleichungslöser hat sich als ausreichend erwiesen, um die Terminierung sicherzustellen.
Das Buch richtet sich an Philosophen und Logiker, die sich mit modalen und hybriden Logiken beschäftigen, sowie an Informatiker, die sich für deduktive Systeme und Entscheidungsverfahren für Logiken interessieren. Ausführliche Fragmente des ersten Teils des Buches können auch als Einführung in hybride Logiken für ein breiteres, an Logik interessiertes Publikum dienen. Der Inhalt des Buches ist in den Bereichen der formalen Logik und der theoretischen Informatik angesiedelt, mit einigen Elementen der Theorie der rechnerischen Komplexität.
Weitere Daten des Buches:
| ISBN: | 9788323336952 |
| Autor: | |
| Verlag: | |
| Einband: | Taschenbuch |
| Erscheinungsjahr: | 2015 |
| Seitenzahl: | 232 |
Kauf:
Derzeit verfügbar, auf Lager.
