Wyniki

Gównymi wynikami mojej pracy sa:

• klauzulowe systemy tablicowe i ulepszone procedury decyzyjne dla zdaniowych logik modalnych K, KD, T, KB, KDB, B, K4, KD4 i S4 (zobacz Rozdzia 3);

• ustalenie najlepszej do tej chwili górnej zozonosci pamieciowej $O(n.\log{n})$ dla zdaniowych logik modalnych K4, KD4 i S4, oraz O(n²) dla logik KB, KDB i B (zobacz Sekcje 3.7 i Twierdzenia 3.7.2, 3.7.6 i 3.7.9);

• podanie nowego dowodu dla znanych wyników innych autorów [7,1] stwierdzajacych, ze zdaniowe logiki modalne K i KD sa rozstrzygalne w pamieci rzedu $O(n.\log{n})$ (zobacz Sekcje 3.7.1 i Twierdzenie 3.7.2);

• sformuowanie pojec pozytywnych programów w zdaniowych logikach modalnych i w jezyku pierwszego rzedu MDatalog (zobacz Definicje 2.4.2 i 5.2.1);

• podanie algorytmów konstruujacych najmniejsze modele dla pozytywnych programów w jezyku zdaniowym i w MDatalog, o ile rozwazana logika modalna jest KD, T, KDB, B, KD5, KD45, S5, KD4 lub S4 (zobacz Algorytmy 4.2.1, 4.4.1 i 5.5.1); oraz warunków gwarantujacych wielomianowa zozonosc czasowa tej konstrukcji (zobacz Twierdzenia 4.2.6 i 4.4.9 oraz Wniosek 5.4.5);

• charakteryzacja pozytywnych programów (w jezyku zdaniowym i w MDatalog) w logikach KB, K5, K45 i KB5 przez jeden lub dwa modele, które moga byc efektywnie skonstruowane (zobacz Sekcje 4.3 i Wnioski 4.3.5 i 5.4.7);

• twierdzenie pokazujace wielomianowa zozonosc obliczenia zapytan w jezyku MDatalog, o ile bazowa logika modalna jest KD, T, KB, KDB, B, K5, KD5, K45, KD45, KB5 lub S5, przy zaozeniach, ze gebokosci kwantyfikatorów w zapytaniach i programie sa skonczenie ograniczone oraz gebokosc modalnosci programu jest skonczenie ograniczona w przypadku gdy rozwazana logika nie jest normalnym rozszerzeniem logiki K5 (zobacz Twierdzenie 5.4.8);

• twierdzenie pokazujace, ze problem sprawdzenia spenialnosci formu Horna o skonczenie ograniczonej gebokosci modalnosci w zdaniowych logikach modalnych KD, T, KB, KDB i B jest rozstrzygalny w czasie wielomianowym (zobacz Wnioski 4.2.7 i 4.3.6);

• podanie nowego dowodu dla znanych wyników innych autorów [3,2] stwierdzajacych, ze problem sprawdzenia spenialnosci formu Horna w zdaniowych logikach modalnych K5, KD5, K45, KD45, KB5 i S5 jest rozstrzygalny w czasie wielomianowym (zobacz Wnioski 4.2.8 i 4.3.7).

Praca zawiera równiez przykady zastosowan wspomnianych technik do modalnych dedukcyjnych baz danych. Obie moje metody oszacowania zozonosci pamieciowej dla zdaniowych logik modalnych i konstruowania najmniejszych modeli dla pozytywnych programów sa stosowalne nie tylko dla logik rozwazanych w pracy.