Klauzulowe systemy tablicowe dla zdaniowych logik modalnych

Przedstawione sa w pracy klauzulowe systemy tablicowe dla zdaniowych logik modalnych K, KD, T, KB, KDB, B, K4, KD4 i S4 (zobacz Sekcje 2.5 i 3.1 oraz Tablice 3.1, 3.2 i 3.3). Za pomoca tych systemów skonstruowaem procedury decyzyjne dla powyzszych logik z ulepszona zozonoscia pamieciowa.

Wspomniane systemy tablicowe sa zdefiniowane tylko dla zbiorów podstawowych klauzul. Uzywajac maych liter a i b do oznaczania zmiennych zdaniowych i ich negacji, podstawowa klauzula jest formua jednej z postaci $\Box^s\lnot\Box a$, $\Box^s(a_1 \lor \ldots \lor a_k)$ i $\Box^s(a \lor B)$, gdzie $s \geq 0$, $k \geq 1$, a B jest formua postaci $\Box b$ lub $\lnot\Box b$. Mozemy sprowadzic dowolna formue do równo-spenialnego zbioru podstawowych klauzul (w kazdej normalnej logice modalnej), aby bya w postaci wymaganej przez wspomniane systemy (zobacz Sekcje 2.3).

Omówione systemy tablicowe sa sformuowane w sposób podobny do systemów tablicowych Hintikki [5], Rautenberga [9], Gorégo [4] i Hudelmaiera [7]. Dla logik K, KD, T, KB, KDB i B, uzywam dodatkowego spójnika $\blacksquare$, który ma taka sama semantyke co $\Box$ lecz inna role syntaktyczna (formuy postaci $\blacksquare^s\phi$ nie moga byc gównymi klauzulami regu). Dla logik K4 i KD4, uzywam nowego spójnika $\boxdot$ do symulowania spójnika $\Box$ logiki S4 (w taki sposób, ze $M,w \vDash\boxdot\phi$ wtw, gdy $M,w \vDash(\Box\phi \land \phi)$). Dla logik K4 i KD4, spójnik $\blacksquare$ ma taka sama semantyke co $\boxdot$, ale formuy postaci $\blacksquare^s\phi$ nie moga byc gównymi klauzulami regu.

Wspomniane systemy tablicowe sa poprawne i zupene (zobacz Twierdzenia 3.4.9, 3.5.9 i 3.6.9) i maja wasnosc skonczonej tablicy (zobacz Sekcje 3.3).