Deduktív rendszerek és a hibrid logikák eldönthetőségi problémája

Eredeti címe:

Deductive Systems and the Decidability Problem for Hybrid Logics

Könyv tartalma:

Ez a könyv két téma metszéspontjában áll: a hibrid logikák eldönthetősége és számítási komplexitása, valamint a hozzájuk tervezett deduktív rendszerek. A hibrid logikákat itt két csoportra osztjuk: standard hibrid logikákra, amelyekben a nominálisok külön fajtájú kifejezésekként szerepelnek, és nem standard hibrid logikákra, amelyek nem tartalmaznak nominálisokat, de amelyek kifejezőereje megegyezik a kötőszó nélküli standard hibrid logikák kifejezőerejével. A könyv eredeti eredményei két részre oszlanak. Ez a felosztás magának a könyvnek a felosztását tükrözi. Az első típusú eredmények a hibrid logikák modellelméleti és komplexitási tulajdonságaira vonatkoznak. Mivel az általunk standardnak nevezett hibrid logikák meglehetősen jól vizsgáltak, az erőfeszítések a könyvben nem standardnak nevezett hibrid logikákra összpontosítottak. A nem szabványos hibrid logikák alatt olyan globális számlálóoperátorokkal (M(En)) rendelkező modális logikákat értünk, amelyek kifejezőereje megegyezik a kötésmentes szabványos hibrid logikák kifejezőerejével. A vonatkozó eredmények a következőket tartalmazzák: 1. A globális számlálóoperátorokkal rendelkező K modális logika (MK(En)) szilárd és teljes axiomatizációjának felállítása, amely könnyen kiterjeszthető más keretosztályokra is, 2. A modális logika K globális számlálóoperátorokkal (MK(En)).

Szoros komplexitási korlátok megállapítása, nevezetesen NExpTime-teljesség a globális számlálóoperátorokkal rendelkező modális logikára, amelyet tetszőleges, reflexív, szimmetrikus, soros és tranzitív keretek (MK(En)), MT(En)), MD(En)), MB(En)), MK4(En)) osztályai felett definiáltak, binárisan kódolt numerikus indexekkel. Az euklideszi és ekvivalenciális keretek (MK5(En)), MS5(En)) osztályai felett definiált logika exponenciális méretű modelltulajdonságának megállapítása. A második típusú eredmények konkrét deduktív (táblás és szekvenciális) rendszerek tervezése standard és nem standard hibrid logikákhoz. Pontosabban ezek közé tartoznak: 1. Olyan prefixált és internalizált tableau-kalkulusok kidolgozása, amelyek a kötésmentes standard hibrid logikák egy gazdag osztályára nézve hangosak, teljesek és terminálók. A jelzett kalkulusok érdekes tulajdonsága a (D) szabály nem elágazó jellege, 2. Olyan prefixált és internalizált tableau-kalkulusok kidolgozása, amelyek nem szabványos hibrid logikákhoz hangosak, teljesek és terminálhatók. A globális számláló operátorokkal rendelkező modális logikára alkalmazott internalizációs technika újszerű az irodalomban, 3. Az első olyan hibrid algoritmus kidolgozása, amely egyenlőtlenségmegoldót tartalmaz globális számláló operátorokkal rendelkező modális logikákra. Az érvelés aritmetikai részének átadása egy egyenlőtlenségmegoldóhoz elegendőnek bizonyult a termináció biztosításához.

A könyv a modális és hibrid logikákkal foglalkozó filozófusoknak és logikusoknak, valamint a logikák deduktív rendszerei és döntési eljárásai iránt érdeklődő informatikusoknak szól. A könyv első részének terjedelmes töredékei a logika iránt érdeklődő szélesebb közönség számára is bevezetésként szolgálhatnak a hibrid logikákba. A könyv tartalma a formális logika és az elméleti informatika területén helyezkedik el, a számítási komplexitás elméletének néhány elemével.