Metody

• Aby oszacowac zozonosc pamieciowa dla zdaniowych logik modalnych, zdefiniowaem procedury decyzyjne oparte na klauzulowych systemach tablicowych, w których saturacja gra wazna role.

• Dla zdaniowej logiki modalnej L, aby skonstruowac najmniejszy L-model dla danego pozytywnego programu P zbudowaem graf L-modelu realizujacy P.

• Dla danego programu P w jezyku MDatalog w normalnej logice modalnej pierwszego rzedu L, aby skonstruowac najmniejszy L-model (pierwszego rzedu) dla P mozemy generowac podstawowa instancje P, traktowac ja jako pozytywny program w jezyku zdaniowym i skonstruowac dla niego najmniejszy (zdaniowy) L-model. (Ta metoda jest uzywana do oszacowania zozonosci obliczenia. W pracy dyskutuje bardziej efektywna metode.)