Z Wikipedii, wolnej encyklopedii
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[1]
Objaśnienia i działanie algorytmu [ edytuj | edytuj kod ] 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
{\displaystyle W}
zamkniętym , jeśli jest zdanie
α
{\displaystyle \alpha }
{
α
,
¬
α
}
⊆
W
.
{\displaystyle \{\alpha ,\lnot \alpha \}\subseteq W.}
Maksymalną tablicą semantyczną zbioru
G
{\displaystyle G}
G
{\displaystyle G}
W
{\displaystyle W}
α
{\displaystyle \alpha }
β
{\displaystyle \beta }
¬
¬
α
∈
W
,
{\displaystyle \lnot \lnot \alpha \in W,}
W
{\displaystyle W}
W
′
{\displaystyle W'}
W
′
=
W
∖
{
¬
¬
α
}
∪
{
α
}
{\displaystyle W'=W\setminus \{\lnot \lnot \alpha \}\cup \{\alpha \}}
α
∧
β
∈
W
,
{\displaystyle \alpha \land \beta \in W,}
W
{\displaystyle W}
W
′
{\displaystyle W'}
W
′
=
W
∖
{
α
∧
β
}
∪
{
α
,
β
}
{\displaystyle W'=W\setminus \{\alpha \land \beta \}\cup \{\alpha ,\beta \}}
α
∨
β
∈
W
,
{\displaystyle \alpha \lor \beta \in W,}
W
{\displaystyle W}
W
1
′
{\displaystyle W'_{1}}
W
2
′
{\displaystyle W'_{2}}
W
1
′
=
W
∖
{
α
∨
β
}
∪
{
α
}
{\displaystyle W'_{1}=W\setminus \{\alpha \lor \beta \}\cup \{\alpha \}}
W
2
′
=
W
∖
{
α
∨
β
}
∪
{
β
}
{\displaystyle W'_{2}=W\setminus \{\alpha \lor \beta \}\cup \{\beta \}}
¬
(
α
∨
β
)
∈
W
,
{\displaystyle \lnot (\alpha \lor \beta )\in W,}
W
{\displaystyle W}
W
′
{\displaystyle W'}
W
′
=
W
∖
{
¬
(
α
∨
β
)
}
∪
{
¬
α
,
¬
β
}
{\displaystyle W'=W\setminus \{\lnot (\alpha \lor \beta )\}\cup \{\lnot \alpha ,\lnot \beta \}}
¬
(
α
∧
β
)
∈
W
,
{\displaystyle \lnot (\alpha \land \beta )\in W,}
W
{\displaystyle W}
W
1
′
{\displaystyle W'_{1}}
W
2
′
{\displaystyle W'_{2}}
W
1
′
=
W
∖
{
¬
(
α
∧
β
)
}
∪
{
¬
α
}
{\displaystyle W'_{1}=W\setminus \{\lnot (\alpha \land \beta )\}\cup \{\lnot \alpha \}}
W
2
′
=
W
∖
{
¬
(
α
∧
β
)
}
∪
{
¬
β
}
{\displaystyle W'_{2}=W\setminus \{\lnot (\alpha \land \beta )\}\cup \{\lnot \beta \}}
α
→
β
∈
W
,
{\displaystyle \alpha \to \beta \in W,}
W
{\displaystyle W}
W
1
′
{\displaystyle W'_{1}}
W
2
′
{\displaystyle W'_{2}}
W
1
′
=
W
∖
{
α
→
β
}
∪
{
¬
α
}
{\displaystyle W'_{1}=W\setminus \{\alpha \to \beta \}\cup \{\lnot \alpha \}}
W
2
′
=
W
∖
{
α
→
β
}
∪
{
β
}
{\displaystyle W'_{2}=W\setminus \{\alpha \to \beta \}\cup \{\beta \}}
¬
(
α
→
β
)
∈
W
,
{\displaystyle \lnot (\alpha \to \beta )\in W,}
W
{\displaystyle W}
W
′
{\displaystyle W'}
W
′
=
W
∖
{
¬
(
α
→
β
)
}
∪
{
α
,
¬
β
}
{\displaystyle W'=W\setminus \{\lnot (\alpha \to \beta )\}\cup \{\alpha ,\lnot \beta \}}
α
↔
β
∈
W
,
{\displaystyle \alpha \leftrightarrow \beta \in W,}
W
{\displaystyle W}
W
1
′
{\displaystyle W'_{1}}
W
2
′
{\displaystyle W'_{2}}
W
1
′
=
W
∖
{
α
↔
β
}
∪
{
α
,
β
}
{\displaystyle W'_{1}=W\setminus \{\alpha \leftrightarrow \beta \}\cup \{\alpha ,\beta \}}
W
2
′
=
W
∖
{
α
↔
β
}
∪
{
¬
α
,
¬
β
}
{\displaystyle W'_{2}=W\setminus \{\alpha \leftrightarrow \beta \}\cup \{\lnot \alpha ,\lnot \beta \}}
¬
(
α
↔
β
)
∈
W
,
{\displaystyle \lnot (\alpha \leftrightarrow \beta )\in W,}
W
{\displaystyle W}
W
1
′
{\displaystyle W'_{1}}
W
2
′
{\displaystyle W'_{2}}
W
1
′
=
W
∖
{
¬
(
α
↔
β
)
}
∪
{
¬
α
,
β
}
{\displaystyle W'_{1}=W\setminus \{\lnot (\alpha \leftrightarrow \beta )\}\cup \{\lnot \alpha ,\beta \}}
W
2
′
=
W
∖
{
¬
(
α
↔
β
)
}
∪
{
α
,
¬
β
}
{\displaystyle W'_{2}=W\setminus \{\lnot (\alpha \leftrightarrow \beta )\}\cup \{\alpha ,\lnot \beta \}}
{
α
,
¬
α
}
⊆
W
{\displaystyle \{\alpha ,\lnot \alpha \}\subseteq W}
W
{\displaystyle W}
każdy element
W
{\displaystyle W}
literałem oraz
W
{\displaystyle W}
Zarówno pojęcie drzewa semantycznego, jak i tablicy semantycznej można zdefiniować równoważnie przez drzewa słów nad alfabetem
{
0
,
1
}
{\displaystyle \{0,1\}}
zdań logicznych . Wtedy wymienione wyżej warunki dotyczą zbiorów, które taka funkcja przyporządkowuje wierzchołkom[1]
Dla podanej teorii
G
{\displaystyle G}
T
.
{\displaystyle T.}
T
{\displaystyle T}
G
{\displaystyle G}
G
{\displaystyle G}
[1]
