Tabkrz, 06-DLOGLI0 Podstawy logiki i teorii mnogości
[ Pobierz całość w formacie PDF ]Klasyczny Rachunek Zda«:
Tablice Analityczne
(Logika Matematyczna: Wykłady 11,12)
Semestr Zimowy 2007–2008
Jerzy Pogonowski
Zakład Logiki Stosowanej UAM
11.0. Wprowadzenie
Omówimy teraz jeszcze jedn¡ operacj¦ konsekwencji w KRZ, a mianowicie konsekwencj¦ wyznaczon¡
przez
tablice analityczne
.
Systematyczne badania nad tego typu konsekwencjami prowadzone s¡ od prawie pół wieku. Sama metoda
znana jest pod ró»nymi nazwami, mówi si¦ np. o:
²
tablicach analitycznych
²
tablicach semantycznych
²
tablicach Smullyana
²dual tableaux
²
drzewach semantycznych.
Pocz¡tki stosowania tej metody odnoszone s¡ do prac Gentzena, jednak mo»na jej zastosowania znale¹¢
ju» w wieku XIX u Lewisa Carrolla, jak wspominali±my na poprzednim wykładzie dotycz¡cym metody
rezolucji.
Pierwsze u»ycia omawianej metody (około pół wieku temu) wi¡»e si¦ zwykle z nazwiskami E. Betha,
K. Schütte’go, J. Hintikki oraz S. Kripke’go. Informacje historyczne znale¹¢ mo»na np. w podanych ni»ej
pozycjach bibliograficznych:
Handbook of Tableau Methods
1999, Marciszewski, Murawski 1995, Annelis
1990. Najwi¦ksz¡ popularno±¢ omawiana metoda (pod nazw¡
tablic analitycznych
) zyskała dzi¦ki pracom
Raymonda Smullyana (np. Smullyan 1968) oraz Richarda Jereya (zob. Jerey 1991). Logicy polscy tak»e
do±¢ wcze±nie zajmowali si¦ (ró»nymi odmianami) tablic analitycznych (zobacz np. Rasiowa, Sikorski 1960,
Lis 1960, Pawlak 1965).
Coraz wi¦ksze zainteresowanie omawian¡ metod¡ wi¡»e si¦ m.in. z jej zastosowaniami w automatycznym
dowodzeniu twierdze«.
11.0.1. O drzewach
Dotychczas posługiwali±my si¦ poj¦ciem
drzewa
w sposób intuicyjny, podaj¡c przykłady: drzew syntak-
tycznych formuł oraz drzew dowodowych. Omawiana teraz metoda robi istotny u»ytek z tego poj¦cia, nale»y
je wi¦c precyzyjnie zdefiniowa¢.
Grafem
nazywamy dowoln¡ par¦
hX;Ri
, gdzie
X
jest zbiorem, a
R
jest podzbiorem
X£X
. Elementy
zbioru
X
nazywamy
wierzchołkami
, a elementy zbioru
Rkraw¦dziami
grafu
hX;Ri
.
Mówimy, »e relacja
R
na zbiorze
X
jest (ostrym)
cz¦±ciowym porz¡dkiem
w
X
, je±li jest ona asyme-
tryczna i przechodnia w
X
(lub, co na to samo wychodzi: przeciwzwrotna i przechodnia w
X
).
Ka»dy spójny porz¡dek cz¦±ciowy nazywamy
porz¡dkiem liniowym
.
Liniowy porz¡dek
R
w
X
nazywamy
dobrym porz¡dkiem
w
X
, je±li ka»dy niepusty podzbiór
X
ma
element
R
-najmniejszy.
Drzewem (o korzeniux
0
)nazwiemy ka»dy układ
hX;R;x
0
i
taki, »e:
²hX;Ri
jest grafem;
²x
0
jest elementem
R
-najmniejszym w
X
;
²R
jest przechodnia w
X
;
²R
jest asymetryczna w
X
;
²
dla ka»dego elementu zbioru
X¡fx
0
g
, zbiór jego wszystkich
R
-poprzedników jest dobrze uporz¡dko-
wany przez relacj¦
R
.
25
Zauwa»my, »e je±li
hX;R;x
0
i
jest drzewem, to:
²
zbiór wszystkich
R
-poprzedników ka»dego elementu zbioru
X¡fx
0
g
jest liniowo uporz¡dkowany;
²
relacja
R
jest przeciwzwrotna w
X
.
Niech
D
=
hX;R;x
0
i
b¦dzie drzewem o korzeniu
x
0
.
Li±¢mi
drzewa
D
nazywamy wszystkie te jego wierzchołki, które nie maj¡
R
-nast¦pników.
Je±li
D
jest drzewem, to przez
r
D
oznaczmy korze«
D
, przez
jDj
zbiór wszystkich wierzchołków
D
, przez
e
(
D
)zbiór wszystkich kraw¦dzi
D
, a przez
L
D
zbiór wszystkich li±ci drzewa
D
.
Je±li(
x;y
)
2R
jest kraw¦dzi¡ w
D
, to
x
nazywamy
przodkiemy
, a
y
nazywamy
potomkiemx
.
Je±li(
x;y
)
2R¡R
2
jest kraw¦dzi¡ w
D
, to
x
nazywamy
bezpo±rednim przodkiemy
, a
y
nazywamy
bezpo±rednim potomkiemx
.
Ka»dy podzbiór zbioru wierzchołków drzewa
D
, który jest uporz¡dkowany liniowo przez
R
nazywamy
ła«cuchem
w
D
. Ka»dy ła«cuch maksymalny (wzgl¦dem inkluzji) w
D
nazywamy
gał¦zi¡
w
D
. Zamiast
terminu
ła«cuch
u»ywa si¦ równie» terminu
±cie»ka
. Przez
długo±¢
ła«cucha
P
rozumiemy liczb¦ elementów
zbioru
P
.
Pniem
drzewa
D
nazywamy cz¦±¢ wspóln¡ wszystkich gał¦zi
D
.
Rz¦dem
wierzchołka
x
nazywamy moc zbioru wszystkich potomków
x
.
Rz¦dem
drzewa
D
jest kres
górny rz¦dów wszystkich wierzchołków drzewa
D
.
Drzewo
D
jest
sko«czone
, je±li zbiór jego wierzchołków jest sko«czony. Drzewo
D
jest
niesko«czone
,
je±li zbiór jego wierzchołków jest niesko«czony. Drzewo
D
jest
rz¦du sko«czonego
, je±li jego rz¡d jest
liczb¡ sko«czon¡.
Przez indukcj¦ definiujemy
poziomy
drzewa:
²
poziom
zerowy
to zbiór jednoelementowy, zło»ony z korzenia drzewa;
²
poziom
k+1
to zbiór wszystkich bezpo±rednich nast¦pników wierzchołków poziomu
k
.
Wysoko±ci¡
drzewa jest najwi¦ksza liczba
n
taka, »e istnieje poziom
n
w drzewie. Je±li drzewo ma
wierzchołki poziomu
n
dla ka»dej liczby naturalnej
n
, to mówimy, »e wysoko±¢ drzewa jest
niesko«czona
(równa
!
).
Ka»de drzewo, w którym ka»dy wierzchołek nie b¦d¡cy li±ciem ma najwy»ej
n
bezpo±rednich potomków,
nazywamy
drzewemn-arnym
. W szczególno±ci:
²
Ka»de drzewo, w którym ka»dy wierzchołek nie b¦d¡cy li±ciem ma najwy»ej dwóch bezpo±rednich
potomków nazwiemy
drzewem nierozwojowym w sensie watyka«skim
, w skrócie
nw-drzewem
.
²
Ka»de drzewo, w którym ka»dy wierzchołek nie b¦d¡cy li±ciem ma dokładnie dwóch bezpo±rednich
potomków nazywamy
drzewem dwójkowym
(u»ywa si¦ te» terminu
drzewo binarne
).
Wa»nym twierdzeniem, z którego wielokrotnie b¦dziemy korzysta¢, jest nast¦puj¡cy:
Lemat Königa.
Je±li drzewo
D
rz¦du sko«czonego jest niesko«czone, to ma gał¡¹ niesko«czon¡.
Dowód.
Przypu±¢my, »e
D
jest niesko«czone. Zdefiniujemy gał¡¹ niesko«czon¡
fx
0
;x
1
;x
2
;:::g
w
D
przez induk-
26
cj¦.
Za element
x
0
bierzemy korze« drzewa
D
. Poniewa»
D
jest niesko«czone, wi¦c
x
0
ma niesko«czenie wiele
R
-nast¦pników.
Przypu±¢my, »e
x
0
;x
1
;x
2
;:::;x
n¡
1
zostały zdefiniowane tak, »e
x
i
nale»y do
i
-tego poziomu drzewa
D
oraz
x
i
ma niesko«czenie wiele
R
-nast¦pników. Z zało»enia,
x
n¡
1
ma tylko sko«czenie wiele
bezpo±rednich
R
-nast¦pników. Poniewa»
x
n¡
1
ma niesko«czenie wiele
R
-nast¦pników, wi¦c co najmniej jeden z jego bezpo-
±rednich
R
-nast¦pników tak»e ma niesko«czenie wiele
R
-nast¦pników. Wybieramy wi¦c element
x
n
z
n
-tego
poziomu drzewa
D
o tej wła±nie własno±ci. Wtedy
x
n
ma niesko«czenie wiele
R
-nast¦pników. Poniewa» jest
tak dla ka»dego
n
, pokazali±my istnienie niesko«czonej gał¦zi
fx
0
;x
1
;x
2
;:::g
w drzewie
D
.
Q.E.D.
Lemat Königa mo»na te» wysłowi¢ nast¦puj¡co:
²
Je±li
D
jest drzewem rz¦du sko«czonego i dla ka»dej liczby naturalnej
n
w
D
istniej¡ ła«cuchy o co
najmniej
n
elementach, to
D
ma ła«cuch niesko«czony.
Mówimy, »e
hY;Q;y
0
i
jest
poddrzewem
drzewa
hX;R;x
0
i
, gdy:
1)
YµX
,
Q
=
R\Y
2
2)
hY;Q;y
0
i
jest drzewem o wierzchołku
y
0
.
Je±li
D
1
jest poddrzewem
D
2
, to piszemy
D
1
¿D
2
.
Je±li
P
jest gał¦zi¡ (sko«czon¡) w drzewie
D
, to niech
P
f
oznacza li±¢ drzewa
D
nale»¡cy do
P
.
Niech
D
1
=
hX;R;x
0
i
i
D
2
=
hY;Q;y
0
i
b¦d¡ drzewami,
X\Y
=
;
, niech
P
b¦dzie gał¦zi¡ w
D
1
i niech
drzewo
D
3
=
hZ;S;z
0
i
b¦dzie zdefiniowane w sposób nast¦puj¡cy:
²Z
=
X[Y
²z
0
=
x
0
²S\X
2
=
R
²S\Y
2
=
Q
²
(
P
f
;y
0
)
2S
.
Mówimy wtedy, »e drzewo
D
3
jest
przedłu»eniem
drzewa
D
1
na gał¦zi
P
o drzewo
D
2
i piszemy
D
1
t
P
f
D
2
@
D
3
.
Przedłu»anie polega zatem, intuicyjnie mówi¡c, na „doczepianiu” drzewa do li±ci innego drzewa. Za-
uwa»my, »e jest to relacja czteroargumentowa.
Dla dowolnych drzew
D
1
oraz
D
3
oraz gał¦zi
P
drzewa
D
1
, je±li istnieje
D
2
takie, »e
D
1
t
P
f
D
2
@
D
3
,
to piszemy
D
1
@
P
f
D
3
. Dla dowolnych drzew
D
1
oraz
D
3
, piszemy
D
1
@
D
3
, je±li istnieje gał¡¹
P
w
D
1
taka, »e
D
1
@
P
f
D
3
.
Piszemy
D
=
D
1
t
P
f
D
2
, je±li istnieje
D
3
takie, »e
D
1
t
P
f
D
2
@
D
3
. Piszemy
D
=
D
1
tD
2
, je±li istnieje
gał¡¹
P
w
D
1
taka, »e
D
1
t
P
f
D
2
@
D
.
Relacje
¿
oraz@s¡ cz¦±ciowymi porz¡dkami (w ustalonej rodzinie drzew). Nie b¦d¡ nam potrzebne
»adne specjalne operacje na drzewach (m.in. wyznaczone przez te porz¡dki), oprócz pewnego specjalnego
sumowania drzew. Niech mianowicie
D
=
fD
1
;D
2
;:::g
b¦dzie rodzin¡ (by¢ mo»e niesko«czon¡) drzew,
dobrze uporz¡dkowan¡ przez relacj¦@. Przez
sum¦
rodziny
D
rozumiemy najmniejsze drzewo, które jest
Wszystkie wierzchołki dowolnego drzewa mo»na liniowo uporz¡dkowa¢ (odpowiednio je koduj¡c). Szcze-
gólnie wa»ne s¡ dwa tego typu porz¡dki:
27
przedłu»eniem wszystkich drzew z
D
. Tak zdefiniowan¡ sum¦ rodziny
D
oznaczamy przez
F
D
.
²
„Porz¡dek poprzeczny”. Niech dana b¦dzie ±ci±le rosn¡ca funkcja
f
ze zbioru wierzchołków drzewa
D
w zbiór liczb naturalnych
N
. Wierzchołek
xf
-poprzedza wierzchołek
y
wtedy i tylko wtedy, gdy:
poziom
x
jest mniejszy od poziomu
y
lub, gdy
x
i
y
s¡ na tym samym poziomie drzewa,
f
(
x
)
<f
(
y
).
²
„Porz¡dek wzdłu»ny”. Niech dana b¦dzie ±ci±le rosn¡ca funkcja
f
ze zbioru wierzchołków drzewa
D
=
hX;R;x
0
i
w zbiór liczb naturalnych
N
. Tym razem
f
-porz¡dek wierzchołków drzewa
D
okre±limy przez
indukcj¦. Za bezpo±redni
f
-nast¦pnik korzenia
x
0
drzewa
D
(czyli za
x
1
) bierzemy ten z elementów
pierwszego poziomu drzewa, dla którego warto±¢ funkcji
f
jest najmniejsza. Je±li
x
1
nie jest li±ciem,
to rozpatrujemy z kolei zbiór wszystkich jego bezpo±rednich
R
-nast¦pników, dla znalezienia kolejnego
elementu
f
-porz¡dku, tj. elementu
x
2
: b¦dzie to ten z bezpo±rednich
R
-nast¦pników wierzchołka
x
1
,
dla którego warto±¢ funkcji
f
jest najmniejsza. Je±li
x
1
jest li±ciem, to za nast¦pny w
f
-porz¡dku (czyli
za
x
2
) bierzemy ten z bezpo±rednich
R
-nast¦pników
x
0
ró»nych od
x
1
, dla którego warto±¢ funkcji
f
jest najmniejsza. Przypu±¢my, »e wierzchołki
x
0
;x
1
;:::;x
n¡
1
zostały ju» ustawione w ci¡g liniowy.
Spo±ród bezpo±rednich
R
-nast¦pników wierzchołka
x
n¡
1
wybieramy ten, dla którego warto±¢ funkcji
f
jest najmniejsza i niech b¦dzie to kolejny wierzchołek w budowanym
f
-porz¡dku, tj. wierzchołek
x
n
.
Je±li wierzchołek ten nie jest li±ciem, to rozpatrujemy z kolei zbiór wszystkich jego bezpo±rednich
R
-
nast¦pników, dla znalezienia kolejnego elementu
f
-porz¡dku, tj. elementu
x
n
+1
. Je±li
x
n
jest li±ciem, to
za nast¦pny w
f
-porz¡dku (czyli za
x
n
+1
) bierzemy ten z bezpo±rednich
R
-nast¦pników
x
n¡
1
ró»nych
od
x
n
, dla którego warto±¢ funkcji
f
jest najmniejsza.
Rozwa»a¢ b¦dziemy tzw.
drzewa znakowane
. Przez
drzewo znakowane
(elementami ze zbioru
L
)
rozumiemy par¦ uporz¡dkowan¡(
D;f
), gdzie
D
jest drzewem, a
f
jest funkcj¡ ze zbioru wierzchołków
drzewa
D
w zbiór
L
. Zwykle
L
b¦dzie pewnym zbiorem formuł. Znakowanie drzew formułami pozwala w
precyzyjny sposób mówi¢ o
wyst¡pieniach
danej formuły w drzewie.
Graficzne reprezentacje drzew s¡ rysunkami, na których wierzchołki (jako± znakowane — punktami,
liczbami, formułami, itd.) poł¡czone s¡ liniami, odpowiadaj¡cymi kraw¦dziom. Przy tym, je±li
hX;R;x
0
i
jest drzewem, to na rysunku zaznaczamy tylko kraw¦dzie nale»¡ce do
R¡R
2
(przy tym, poprzedniki
R
umieszczane s¡ nad nast¦pnikami).
Dla przykładu, poka»my dwa rysunki drzew:
(1)
©
©
©
©©
H
H
H
HH
(11)
(3)
(12)
©
©©
H
HH
(13)
(4)
©
©
H
H
(5)
(15)
(7)
(14)
(16)
(6)
(8)
(9)
(10)
W tym drzewie s¡ cztery gał¦zie, zaczynaj¡ce si¦ w korzeniu drzewa (wierzchołek oznaczony przez(1)) i
ko«cz¡ce si¦ li±¢mi drzewa:(6),(10),(14)oraz(16). Pie« drzewa jest tu zbiorem jednoelementowym:
f
(1)
g
.
28
(2)
[ Pobierz całość w formacie PDF ]