Powiadomienia systemowe
- Sesja wygasła!
Tytuł artykułu
Autorzy
Wybrane pełne teksty z tego czasopisma
Identyfikatory
Warianty tytułu
Języki publikacji
Abstrakty
We give algorithms to construct the least L-model for a given positive modal logic program P, where L can be one of the modal logics KD, T, KDB, B, KD4, S4, KD5, KD45, and S5. If L Î {KD5, KD45, S5}, or L Î {KD, T, KDB,B} and the modal depth of P is finitely bounded, then the least L-model of P can be constructed in PTIME and coded in polynomial space. We also show that if P has no flat models then it has the least models in KB, K5, K45, and KB5. As a consequence, the problem of checking the satisfiability of a set of modal Horn formulae with finitely bounded modal depth in KD, T, KB, KDB, or B is decidable in PTIME. The known result that the problem of checking the satisfiability of a set of Horn formulae in K5, KD5, K45, KD45, KB5, or S5 is decidable in PTIME is also studied in this work via a different method.
Słowa kluczowe
Wydawca
Czasopismo
Rocznik
Tom
Strony
29--60
Opis fizyczny
bibliogr. 12 poz.
Twórcy
autor
- Institute of Informatics Warsaw University ul. Banacha 2 02-097 Warsaw, Poland, nguyen@mimuw.edu.pl
Bibliografia
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-article-BUS1-0008-0002