Deductive Systems and the Decidability Problem for Hybrid Logics
Niniejsza książka przecina dwa tematy: rozstrzygalność i złożoność obliczeniową logik hybrydowych oraz zaprojektowane dla nich systemy dedukcyjne. Logiki hybrydowe są tutaj podzielone na dwie grupy: standardowe logiki hybrydowe obejmujące nominały jako wyrażenia odrębnego rodzaju oraz niestandardowe logiki hybrydowe, które nie obejmują nominałów, ale których moc ekspresyjna odpowiada mocy ekspresyjnej standardowych logik hybrydowych bez spoiwa. Oryginalne wyniki tej książki są podzielone na dwie części. Podział ten odzwierciedla podział samej książki. Pierwszy rodzaj wyników dotyczy własności modelowo-teoretycznych i złożoności logik hybrydowych. Ponieważ logiki hybrydowe, które nazywamy standardowymi, są dość dobrze zbadane, wysiłki skupiły się na logikach hybrydowych określanych w tej książce jako niestandardowe. Niestandardowe logiki hybrydowe są rozumiane jako logiki modalne z globalnymi operatorami zliczającymi (M(En)), których moc wyrażeniowa odpowiada mocy wyrażeniowej standardowych logik hybrydowych. Istotne wyniki obejmują: 1. Ustanowienie solidnej i kompletnej aksjomatyzacji dla logiki modalnej K z globalnymi operatorami zliczania (MK(En)), którą można łatwo rozszerzyć na inne klasy ram, 2.
Ustalenie ścisłych granic złożoności, a mianowicie NExpTime-completeness dla logiki modalnej z globalnymi operatorami zliczającymi zdefiniowanej na klasach ram arbitralnych, refleksyjnych, symetrycznych, szeregowych i przechodnich (MK(En)), MT(En)), MD(En)), MB(En)), MK4(En)) z indeksami numerycznymi zakodowanymi binarnie. Ustalenie wykładniczo-wymiarowej własności modelu dla tej logiki zdefiniowanej na klasach ram euklidesowych i równoważnych (MK5(En)), MS5(En)). Wyniki drugiego typu polegają na zaprojektowaniu konkretnych systemów dedukcyjnych (tablicowych i sekwencyjnych) dla standardowych i niestandardowych logik hybrydowych. Dokładniej, obejmują one: 1. Opracowanie prefiksowanego i internalizowanego rachunku tablicowego, które są sensowne, kompletne i terminujące dla bogatej klasy standardowych logik hybrydowych bez spoiwa. Interesującą cechą wskazanych rachunków jest nierozgałęziający się charakter reguły (D), 2. Opracowanie prefiksowanych i zinternalizowanych rachunków tableau, które są poprawne, kompletne i kończące się dla niestandardowych logik hybrydowych. Technika internalizacji zastosowana do rachunku tablicowego dla logiki modalnej z globalnymi operatorami zliczania jest nowatorska w literaturze, 3. Opracowanie pierwszego algorytmu hybrydowego obejmującego rozwiązywanie nierówności dla logik modalnych z globalnymi operatorami zliczania. Przeniesienie arytmetycznej części rozumowania do rozwiązania nierówności okazało się wystarczające do zapewnienia zakończenia.
Książka skierowana jest do filozofów i logików zajmujących się logikami modalnymi i hybrydowymi, a także do informatyków zainteresowanych systemami dedukcyjnymi i procedurami decyzyjnymi dla logik. Obszerne fragmenty pierwszej części książki mogą również służyć jako wprowadzenie do logik hybrydowych dla szerszej publiczności zainteresowanej logiką. Treść książki jest umiejscowiona w obszarach logiki formalnej i informatyki teoretycznej z pewnymi elementami teorii złożoności obliczeniowej.