Deduktivní systémy a problém rozhodnutelnosti pro hybridní logiky

Původní název:

Deductive Systems and the Decidability Problem for Hybrid Logics

Obsah knihy:

Tato kniha je průsečíkem dvou témat: rozhodnutelnosti a výpočetní složitosti hybridních logik a deduktivních systémů pro ně navržených. Hybridní logiky jsou zde rozděleny do dvou skupin: standardní hybridní logiky zahrnující nominály jako výrazy samostatného druhu a nestandardní hybridní logiky, které nominály nezahrnují, ale jejichž vyjadřovací síla odpovídá vyjadřovací síle standardních hybridních logik bez vazby. Původní výsledky této knihy jsou rozděleny do dvou částí. Toto rozdělení odráží rozdělení samotné knihy. První typ výsledků se týká modelově-teoretických a složitostních vlastností hybridních logik. Protože hybridní logiky, které nazýváme standardními, jsou poměrně dobře prozkoumány, soustředilo se úsilí na hybridní logiky označované v této knize jako nestandardní. Nestandardními hybridními logikami rozumíme modální logiky s globálními počítacími operátory (M(En)), jejichž vyjadřovací síla odpovídá vyjadřovací síle standardních hybridních logik bez vazby. Důležité výsledky zahrnují: 1. Stanovení spolehlivé a úplné axiomatiky pro modální logiku K s globálními počítacími operátory (MK(En)), kterou lze snadno rozšířit na další třídy rámců, 2. Stanovení axiomatiky pro modální logiku K s globálními počítacími operátory (MK(En)), kterou lze snadno rozšířit na další třídy rámců.

Stanovení těsných hranic složitosti, konkrétně NExpTime-úplnosti pro modální logiku s globálními počítacími operátory definovanými nad třídami libovolných, reflexivních, symetrických, sériových a tranzitivních rámců (MK(En)), MT(En)), MD(En)), MB(En)), MK4(En)) s číselnými indexy kódovanými v binárním tvaru. Stanovení vlastnosti modelu exponenciální velikosti pro tuto logiku definovanou nad třídami euklidovských a ekvivalentních rámců (MK5(En)), MS5(En)). Výsledky druhého typu spočívají v návrhu konkrétních deduktivních (tabulkových a sekvenčních) systémů pro standardní a nestandardní hybridní logiky. Přesněji řečeno zahrnují: 1. Navržení prefixovaných a internalizovaných tableau kalkulací, které jsou zdravé, úplné a terminující pro bohatou třídu standardních hybridních logik bez vazby. Zajímavým rysem uvedených kalkulů je nevětvící charakter pravidla (D), 2. navržení prefixovaného a internalizovaného tableau kalkulu, které jsou zdravé, úplné a terminující pro nestandardní hybridní logiky. Technika internalizace aplikovaná na tableau kalkul pro modální logiku s globálními počítacími operátory je v literatuře nová, 3. Vypracování prvního hybridního algoritmu zahrnujícího řešitele nerovností pro modální logiky s globálními počítacími operátory. Přenesení aritmetické části uvažování na řešitel nerovností se ukázalo jako dostatečné pro zajištění terminace.

Kniha je určena filozofům a logikům, kteří se zabývají modálními a hybridními logikami, a také informatikům, kteří se zajímají o deduktivní systémy a rozhodovací procedury pro logiky. Rozsáhlé fragmenty první části knihy mohou sloužit i jako úvod do hybridních logik pro širší okruh zájemců o logiku. Obsah knihy je situován do oblasti formální logiky a teoretické informatiky s některými prvky teorie výpočetní složitosti.