``Results on Modal Reasoning with Applications to Modal Deductive Databases''
autora Nguyena Anh Linha
Dedukcyjne bazy danych i programowanie w logice znajduja obszerne i wazne zastosowania. Te dziedziny sa scisle powiazane, gdyz obie uzywaja regu logiki klasycznej do reprezentacji wzajemnych zaleznosci pomiedzy relacjami. Programowanie w logice jest gównie uzywane w systemach sztucznej inteligencji, zas dedukcyjne bazy danych sa systemami, w których ilosc danych jest znacznie wieksza niz ilosc regu. W klasycznej teorii reguy logiczne maja postac uniwersalnie kwantyfikowanych klauzul Horna, zapisanych w jezyku pierwszego rzedu. Dla tak zdefiniowanego jezyka problem spenialnosci jest rozstrzygalny w czasie wielomianowym, a rozmiar generowanego najmniejszego modelu zalezy wielomianowo od dugosci formuy.
Rozszerzenie jezyka zapytan do logik modalnych prowadzi do zdefiniowania modalnego jezyka klauzul Horna. W tym przypadku zostao jednak udowodnione przez Chena i Lina [2], ze problem spenialnosci zbiorów klauzul Horna dla kazdego z nastepujacych jezyków K, KD, T, KB, KDB, B, K4, KD4 i S4 jest zupeny w klasie problemów wymagajacych wielomianowej pamieci, tzn. PSPACE-zupeny. Ze wzgledu na te trudnosc, programowanie w logikach modalnych nie zyskiwao dotad penego uznania, jak równiez teoria modalnych dedukcyjnych baz danych nie bya intensywnie rozwijana.
Z drugiej strony, teoria logik modalnych przyniosa wiele wyników dotyczacych zozonosci problemu spenialnosci formu w zdaniowych logikach modalnych. Udowodniono przez Chena i Lina [2] oraz Fariñas del Cerra i Penttonena [3], ze problem spenialnosci zbiorów klauzul Horna dla kazdej logiki, która jest normalnym rozszerzeniem logiki K5, jest rozstrzygalny w wielomianowym czasie. Górne zozonosci pamieciowe dla logik K, KD, T ( ), i K4, KD4, S4 ( ) zostay uzyskane przez Hudelmaiera [6] oraz Basina, Matthewsa i Viganò [1,10].