Deductive Systems and the Decidability Problem for Hybrid Logics
Táto kniha stojí na priesečníku dvoch tém: rozhodnuteľnosti a výpočtovej zložitosti hybridných logík a deduktívnych systémov pre ne navrhnutých. Hybridné logiky sú tu rozdelené do dvoch skupín: štandardné hybridné logiky zahŕňajúce nominály ako výrazy samostatného druhu a neštandardné hybridné logiky, ktoré nezahŕňajú nominály, ale ktorých vyjadrovacia sila zodpovedá vyjadrovacej sile štandardných hybridných logík bez väzby. Pôvodné výsledky tejto knihy sú rozdelené do dvoch častí. Toto rozdelenie odráža rozdelenie samotnej knihy. Prvý typ výsledkov sa týka modelovo-teoretických a zložitostných vlastností hybridných logík. Keďže hybridné logiky, ktoré nazývame štandardnými, sú pomerne dobre preskúmané, úsilie sa sústredilo na hybridné logiky označované v tejto knihe ako neštandardné. Pod neštandardnými hybridnými logikami sa rozumejú modálne logiky s globálnymi počítacími operátormi (M(En)), ktorých vyjadrovacia sila zodpovedá vyjadrovacej sile štandardných hybridných logík bez väzby. Relevantné výsledky zahŕňajú: 1. Stanovenie spoľahlivej a úplnej axiomatizácie pre modálnu logiku K s globálnymi počítacími operátormi (MK(En)), ktorá sa dá ľahko rozšíriť na iné triedy rámcov, 2.
Stanovenie tesných hraníc zložitosti, konkrétne NExpTime-úplnosti pre modálnu logiku s globálnymi operátormi počítania definovanými nad triedami ľubovoľných, reflexívnych, symetrických, sériových a tranzitívnych rámcov (MK(En)), MT(En)), MD(En)), MB(En)), MK4(En)) s číselnými indexmi kódovanými v dvojkovej sústave. Stanovenie vlastnosti modelu exponenciálnej veľkosti pre túto logiku definovanú nad triedami euklidovských a ekvivalentných rámcov (MK5(En)), MS5(En)). Výsledky druhého typu spočívajú v návrhu konkrétnych deduktívnych (tabuľkových a sekvenčných) systémov pre štandardné a neštandardné hybridné logiky. Presnejšie povedané, zahŕňajú: 1. Navrhnutie prefixovaných a internalizovaných tableau kalkulov, ktoré sú zdravé, úplné a terminujúce pre bohatú triedu štandardných hybridných logík bez väzby. Zaujímavou vlastnosťou uvedených kalkulov je nerozvetvený charakter pravidla (D), 2. navrhnutie prefixovaného a internalizovaného tableau kalkulu, ktoré sú zdravé, úplné a terminujúce pre neštandardné hybridné logiky. Technika internalizácie aplikovaná na tableau kalkul pre modálnu logiku s globálnymi počítacími operátormi je v literatúre nová, 3. Vypracovanie prvého hybridného algoritmu zahŕňajúceho riešiteľa nerovností pre modálne logiky s globálnymi počítacími operátormi. Ukázalo sa, že prenesenie aritmetickej časti uvažovania na riešiteľa nerovností je dostatočné na zabezpečenie ukončenia.
Kniha je určená filozofom a logikom, ktorí sa zaoberajú modálnymi a hybridnými logikami, ako aj informatikom, ktorí sa zaujímajú o deduktívne systémy a rozhodovacie postupy pre logiky. Rozsiahle fragmenty prvej časti knihy môžu slúžiť aj ako úvod do hybridných logík pre širší okruh záujemcov o logiku. Obsah knihy je situovaný do oblasti formálnej logiky a teoretickej informatiky s niektorými prvkami teórie výpočtovej zložitosti.