Sistemi deduttivi e problema della decidibilità delle logiche ibride

Titolo originale:

Deductive Systems and the Decidability Problem for Hybrid Logics

Contenuto del libro:

Questo libro si colloca all'intersezione di due argomenti: la decidibilità e la complessità computazionale delle logiche ibride e i sistemi deduttivi progettati per esse. Le logiche ibride sono qui divise in due gruppi: logiche ibride standard che coinvolgono i nominali come espressioni di un tipo separato, e logiche ibride non standard, che non coinvolgono i nominali ma la cui potenza espressiva corrisponde a quella delle logiche ibride standard senza legante. I risultati originali di questo libro sono divisi in due parti. Questa divisione riflette la divisione del libro stesso. Il primo tipo di risultati riguarda le proprietà teorico-modellistiche e di complessità delle logiche ibride. Poiché le logiche ibride che chiamiamo standard sono abbastanza ben studiate, gli sforzi si sono concentrati sulle logiche ibride che in questo libro vengono chiamate non-standard. Le logiche ibride non standard sono intese come logiche modali con operatori di conteggio globale (M(En)) la cui potenza espressiva corrisponde a quella delle logiche ibride standard prive di legami. I risultati rilevanti comprendono: 1. Stabilire una assiomatizzazione solida e completa per la logica modale K con operatori di conteggio globale (MK(En)), che può essere facilmente estesa ad altre classi di frame, 2. Stabilire una logica modale K con operatori di conteggio globale (MK(En)).

Stabilire limiti di complessità stretti, ossia la completezza di tempo NExpTime per la logica modale con operatori di conteggio globale definita sulle classi di cornici arbitrarie, riflessive, simmetriche, seriali e transitive (MK(En)), MT(En)), MD(En)), MB(En)), MK4(En)) con pedici numerici codificati in binario. Stabilire la proprietà di modello di dimensione esponenziale per questa logica definita sulle classi di cornici euclidee ed equivalenti (MK5(En)), MS5(En)). I risultati del secondo tipo consistono nella progettazione di sistemi deduttivi concreti (tableau e sequenti) per logiche ibride standard e non standard. Più precisamente, essi comprendono: 1. L'ideazione di un calcolo tableau prefissato e di un calcolo tableau interiorizzato che sono validi, completi e terminanti per una ricca classe di logiche ibride standard prive di legami. Una caratteristica interessante dei calcoli indicati è il carattere non ramificante della regola (D), 2. L'ideazione di un calcolo tableau prefissato e di un calcolo tableau internalizzato che siano validi, completi e terminanti per logiche ibride non standard. La tecnica di internalizzazione applicata a un calcolo tableau per la logica modale con operatori di conteggio globale è una novità in letteratura, 3. Elaborazione del primo algoritmo ibrido che coinvolge un risolutore di disuguaglianze per logiche modali con operatori di conteggio globale. Il trasferimento della parte aritmetica del ragionamento a un risolutore di disuguaglianze si è rivelato sufficiente a garantire la terminazione.

Il libro si rivolge a filosofi e logici che lavorano con le logiche modali e ibride, nonché agli informatici interessati ai sistemi deduttivi e alle procedure decisionali per le logiche. Ampi frammenti della prima parte del libro possono anche servire come introduzione alle logiche ibride per un pubblico più ampio interessato alla logica. Il contenuto del libro si colloca nelle aree della logica formale e dell'informatica teorica, con alcuni elementi di teoria della complessità computazionale.