``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 regu
y logiczne maja postac uniwersalnie kwantyfikowanych klauzul Horna, zapisanych w jezyku pierwszego rzedu. Dla tak zdefiniowanego jezyka problem spe
nialnosci jest rozstrzygalny w czasie wielomianowym, a rozmiar generowanego najmniejszego modelu zalezy wielomianowo od d
ugosci formu
y.
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 spe
nialnosci zbiorów klauzul Horna dla kazdego z nastepujacych jezyków K, KD, T, KB, KDB, B, K4, KD4 i S4 jest zupe
ny w klasie problemów wymagajacych wielomianowej pamieci, tzn. PSPACE-zupe
ny.
Ze wzgledu na te trudnosc, programowanie w logikach modalnych nie zyskiwa
o dotad pe
nego uznania, jak równiez teoria modalnych dedukcyjnych baz danych nie by
a intensywnie rozwijana.
Z drugiej strony, teoria logik modalnych przyniosa wiele wyników dotyczacych z
ozonosci problemu spe
nialnosci formu
w zdaniowych logikach modalnych.
Udowodniono przez Chena i Lina [2] oraz Fariñas del Cerra i Penttonena [3], ze problem spe
nialnosci zbiorów klauzul Horna dla kazdej logiki, która jest normalnym rozszerzeniem logiki K5, jest rozstrzygalny w wielomianowym czasie.
Górne z
ozonosci pamieciowe dla logik K, KD, T (
), i K4, KD4, S4 (
)
zosta
y uzyskane przez Hudelmaiera [6] oraz Basina, Matthewsa i Viganò [1,10].