Sisteme deductive și problema decidabilității logicii hibride

Titlul original:

Deductive Systems and the Decidability Problem for Hybrid Logics

Conținutul cărții:

Această carte se află la intersecția a două subiecte: decidabilitatea și complexitatea computațională a logicii hibride și sistemele deductive concepute pentru acestea. Logica hibridă este împărțită aici în două grupuri: logica hibridă standard, care implică nominali ca expresii de un tip separat, și logica hibridă non-standard, care nu implică nominali, dar a cărei putere de exprimare este egală cu puterea de exprimare a logicii hibride standard fără legături. Rezultatele originale ale acestei cărți sunt împărțite în două părți. Această împărțire reflectă împărțirea cărții în sine. Primul tip de rezultate se referă la proprietățile modelelor teoretice și de complexitate ale logicii hibride. Deoarece logicile hibride pe care le numim standard sunt destul de bine investigate, eforturile s-au concentrat asupra logicilor hibride denumite non-standard în această carte. Logica hibridă non-standard este înțeleasă ca logică modală cu operatori de numărare globală (M(En)), a cărei putere expresivă se potrivește cu puterea expresivă a logicii hibride standard fără binder. Rezultatele relevante cuprind: 1. Stabilirea unei axiomatizări solide și complete pentru logica modală K cu operatori de numărare globală (MK(En)), care poate fi extinsă cu ușurință la alte clase de cadre

Stabilirea unor limite strânse de complexitate, și anume NExpTime-completeness pentru logica modală cu operatori de numărare globală definită pe clasele de cadre arbitrare, reflexive, simetrice, seriale și tranzitive (MK(En)), MT(En)), MD(En)), MB(En)), MK4(En)) cu subscripții numerice codificate în binar. Stabilirea proprietății modelului de mărime exponențială pentru această logică definită pe clasele de cadre euclidiene și echivalențiale (MK5(En)), MS5(En)). Rezultatele celui de-al doilea tip constau în proiectarea unor sisteme deductive concrete (tablouri și secvențe) pentru logici hibride standard și non-standard. Mai exact, acestea includ: 1. Conceperea unui calcul de tablou prefixat și a unui calcul de tablou internalizat care sunt solide, complete și terminante pentru o clasă bogată de logici hibride standard fără liant. O caracteristică interesantă a calculelor indicate este caracterul fără ramificare al regulii (D), 2. Elaborarea unui tabel de calcul prefixat și a unui tabel de calcul internalizat care sunt solide, complete și terminante pentru logici hibride non-standard. Tehnica de internalizare aplicată unui tableau calculus pentru logica modală cu operatori de numărare globală este nouă în literatura de specialitate, 3. Conceperea primului algoritm hibrid care implică un rezolutor de inegalități pentru logici modale cu operatori de numărare globală. Transferul părții aritmetice a raționamentului către un soluționator de inegalități s-a dovedit a fi suficient pentru a asigura terminarea.

Cartea se adresează filosofilor și logicienilor care lucrează cu logici modale și hibride, precum și informaticienilor interesați de sistemele deductive și procedurile de decizie pentru logici. Fragmente extinse din prima parte a cărții pot servi, de asemenea, ca o introducere în logicile hibride pentru publicul larg interesat de logică. Conținutul cărții este situat în domeniile logicii formale și informaticii teoretice, cu unele elemente din teoria complexității computaționale.