Логика. Множества. Вероятность. Лексаченко В.А. - 21 стр.

UptoLike

ВУЗ: 

СПб ГУАП | Санкт-Петербург

Составители: 

Рубрика: 

Pust~ trebuets proverit~ predpoloenie, qto formula
F
vlets tavtologie$i. Soglasno metodu rezolci$i otrica-
nie togo vyskazyvani, predstavlennoe v konnktivno$i nor-
mal~no$i forme F = D
1
∧···∧D
n
, rassmatrivaets v kaqestve
dopuweni nekotoro$i sekvencii. Po pravilu raswepleni F
mono zamenit~ spiskom dopuweni$i
D
1
, . . . , D
n
. Esli v tom
spiske imets vno protivoreqawie drug drugu dopuweni
D
i
i D
j
= D
i
, to po pravilu vvedeni otricani vyskazyvanie
F
vlets tavtologie$i. V protivnom sluqae v spiske otyskiva-
ts para diznkci$i vida
A, A
∨ B ili A ∨
B, A
∨ C , iz
kotoryh po teoreme 2.9 sleduet D
n
+1
=
B
ili D
n+1
=
B ∨
C .
Esli
D
n+1
otsutstvuet v ishodnom spiske, to popoln spi-
sok D
1
, . . . , D
n
formulo$i
D
n+1
, poluqim ravnosil~ny$i spisok
D
1
,
. . . , D
n+1
. V tom spiske otyskivats vnye protivoreqi
i pri otsutstvii takovyh vyvodits novoe dopuwenie. Process
vyvoda dopuweni$i prodolaets do teh por, poka novyh dopu-
weni$i poluqat~s ne budet. Esli v okonqatel~nom spiske est~
protivoreqie, to F vlets tavtologie$i, v protivnom sluqae
F
ne vlets tavtologie$i.
Primer 2.4 (Dokazatel~stvo metodom rezolci$i).
Dokazat~
|= (
A →
B
)
→ (
C
∨ A
→ C
∨
B
).
1. Privedem otricanie dokazyvaemogo vyskazyvani k KNF
(
A
→ B
)
→ (
C ∨
A → C
∨
B) =
= A
→
B ∨ C
∨
A ∨
C
∨
B = (
A
∨
B)
∧
(
A ∨
C)
∧
C
∧
B .
2. Ispol~zu KNF kak dopuwenie nekotoro$i sekvencii, po pra-
vilu raswepleni poluqim spisok dopuweni$i:
1) A
∨ B ,
2)
A ∨ C ,
3)
C ,
4) B .
Poskol~ku tot spisok ne soderit vnogo protivoreqi, po-
polnim ego, primen rezolcii.
5) A — rezolci 1 po otnoxeni k strokam 1, 4,
6) A — rezolci 1 po otnoxeni k strokam 2, 3.
3. Protivoreqie v strokah 5, 6 dokazyvaet tavtologi. J
21

Страницы