Metoda tablic semantycznych

Metoda tablic semantycznych – metoda (algorytm) sprawdzania spełnialności teorii (rozumianej jako pewien podzbiór zbioru zdań języka Rachunku Zdań) przez zbudowanie jej maksymalnej tablicy semantycznej.

Objaśnienia i działanie algorytmu

Drzewem semantycznym nazywamy ukorzenione drzewo binarne, którego wierzchołkami są zbiory złożone ze zdań języka Rachunku Zdań (teorie). Wierzchołek $W$ takiego drzewa nazywamy zamkniętym, jeśli jest zdanie $\alpha$ takie, że $\{\alpha ,\mathrm{\neg }\alpha \}\subseteq W.$

Maksymalną tablicą semantyczną zbioru $G$ nazywamy drzewo semantyczne, którego korzeniem jest $G$ i dla każdego wierzchołka $W$ istnieją zdania $\alpha$ i $\beta$ takie, że spełniony jest dokładnie jeden z następujących warunków:

• $\mathrm{\neg }\mathrm{\neg }\alpha \in W,$ $W$ ma dokładnie jedno dziecko $W^{\prime }$ oraz $W^{\prime }=W\setminus \{\mathrm{\neg }\mathrm{\neg }\alpha \}\cup \{\alpha \}$
• $\alpha \wedge \beta \in W,$ $W$ ma dokładnie jedno dziecko $W^{\prime }$ oraz $W^{\prime }=W\setminus \{\alpha \wedge \beta \}\cup \{\alpha ,\beta \}$
• $\alpha \vee \beta \in W,$ $W$ ma dokładnie dwoje dzieci $W{\text{'}}_1$ i $W{\text{'}}_2$ oraz $W{\text{'}}_1=W\setminus \{\alpha \vee \beta \}\cup \{\alpha \}$ i $W{\text{'}}_2=W\setminus \{\alpha \vee \beta \}\cup \{\beta \}$
• $\mathrm{\neg }(\alpha \vee \beta )\in W,$ $W$ ma dokładnie jedno dziecko $W^{\prime }$ oraz $W^{\prime }=W\setminus \{\mathrm{\neg }(\alpha \vee \beta )\}\cup \{\mathrm{\neg }\alpha ,\mathrm{\neg }\beta \}$
• $\mathrm{\neg }(\alpha \wedge \beta )\in W,$ $W$ ma dokładnie dwoje dzieci $W{\text{'}}_1$ i $W{\text{'}}_2$ oraz $W{\text{'}}_1=W\setminus \{\mathrm{\neg }(\alpha \wedge \beta )\}\cup \{\mathrm{\neg }\alpha \}$ i $W{\text{'}}_2=W\setminus \{\mathrm{\neg }(\alpha \wedge \beta )\}\cup \{\mathrm{\neg }\beta \}$
• $\alpha \to \beta \in W,$ $W$ ma dokładnie dwoje dzieci $W{\text{'}}_1$ i $W{\text{'}}_2$ oraz $W{\text{'}}_1=W\setminus \{\alpha \to \beta \}\cup \{\mathrm{\neg }\alpha \}$ i $W{\text{'}}_2=W\setminus \{\alpha \to \beta \}\cup \{\beta \}$
• $\mathrm{\neg }(\alpha \to \beta )\in W,$ $W$ ma dokładnie jedno dziecko $W^{\prime }$ oraz $W^{\prime }=W\setminus \{\mathrm{\neg }(\alpha \to \beta )\}\cup \{\alpha ,\mathrm{\neg }\beta \}$
• $\alpha \leftrightarrow \beta \in W,$ $W$ ma dokładnie dwoje dzieci $W{\text{'}}_1$ i $W{\text{'}}_2$ oraz $W{\text{'}}_1=W\setminus \{\alpha \leftrightarrow \beta \}\cup \{\alpha ,\beta \}$ i $W{\text{'}}_2=W\setminus \{\alpha \leftrightarrow \beta \}\cup \{\mathrm{\neg }\alpha ,\mathrm{\neg }\beta \}$
• $\mathrm{\neg }(\alpha \leftrightarrow \beta )\in W,$ $W$ ma dokładnie dwoje dzieci $W{\text{'}}_1$ i $W{\text{'}}_2$ oraz $W{\text{'}}_1=W\setminus \{\mathrm{\neg }(\alpha \leftrightarrow \beta )\}\cup \{\mathrm{\neg }\alpha ,\beta \}$ i $W{\text{'}}_2=W\setminus \{\mathrm{\neg }(\alpha \leftrightarrow \beta )\}\cup \{\alpha ,\mathrm{\neg }\beta \}$
• $\{\alpha ,\mathrm{\neg }\alpha \}\subseteq W$ oraz $W$ jest liściem
• każdy element $W$ jest literałem oraz $W$ jest liściem

Zarówno pojęcie drzewa semantycznego, jak i tablicy semantycznej można zdefiniować równoważnie przez drzewa słów nad alfabetem $\{0,1\}$ z funkcją przyporządkowującą wierzchołkom podzbiory zbioru zdań logicznych. Wtedy wymienione wyżej warunki dotyczą zbiorów, które taka funkcja przyporządkowuje wierzchołkom.

Dla podanej teorii $G$ algorytm konstruuje jej maksymalną tablicę semantyczną $T.$ Jeśli wszystkie liście $T$ są zamknięte, to algorytm odpowiada, że $G$ nie jest spełnialna. W przeciwnym wypadku odpowiada, że $G$ jest spełnialna.