Klauzulowe systemy tablicowe dla zdaniowych logik modalnych

Next: Definicje dotyczace logik modalnych Up: No Title Previous: Modalne formuy Horna i

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 skonstruowa $\l$ em procedury decyzyjne dla powyzszych logik z ulepszona z $\l$ ozonoscia pamieciowa.

Wspomniane systemy tablicowe sa zdefiniowane tylko dla zbiorów podstawowych klauzul. Uzywajac ma $\l$ ych liter a i b do oznaczania zmiennych zdaniowych i ich negacji, podstawowa klauzula jest formu $\l$ a 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 formu $\l$ a postaci $\Box b$ lub $\lnot\Box b$ . Mozemy sprowadzic dowolna formu $\l$ e do równo-spe $\l$ nialnego zbioru podstawowych klauzul (w kazdej normalnej logice modalnej), aby by $\l$ a w postaci wymaganej przez wspomniane systemy (zobacz Sekcje 2.3).

Omówione systemy tablicowe sa sformu $\l$ owane 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 (formu $\l$ y postaci $\blacksquare^s\phi$ nie moga byc g $\l$ ównymi klauzulami regu $\l$ ). 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 formu $\l$ y postaci $\blacksquare^s\phi$ nie moga byc g $\l$ ównymi klauzulami regu $\l$ .

Wspomniane systemy tablicowe sa poprawne i zupe $\l$ ne (zobacz Twierdzenia 3.4.9, 3.5.9 i 3.6.9) i maja w $\l$ asnosc skonczonej tablicy (zobacz Sekcje 3.3).

Next: Definicje dotyczace logik modalnych Up: No Title Previous: Modalne formuy Horna i

Nguyen Anh Linh
2000-04-01