Составители:
Рубрика:
1) A
→ B ,
B , A |
=
B — svo$istvo 1,
2) A → B ,
B , A
|= B
— svo$istvo 2, udalenie →
,
3)
A → B ,
B
|
= A
— vvedenie
, 1, 2,
zatem vspomogatel~nu sekvenci B → A, A |= B
(lemmu 2)
1) B → A , A , B |
= A
— svo$istvo 1,
2)
B
→
A , A , B
|=
A
— svo$istvo 2, udalenie →,
3) B
→
A , A
|=
B
— vvedenie
, 1, 2,
4) B
→
A , A
|
=
B
— svo$istvo 3, udalenie , 3,
a zatem s pomow~ lemm 1, 2 dokazat~ tavtologi
1)
A → B , B |
=
A — lemma 1,
2) A → B |=
B
→
A
— vvedenie →, 1,
3)
|
= (
A
→
B
) →
(B
→
A
)
— vvedenie →
, 2,
4) B → A , A |= B
— lemma 2,
5) B → A |
= A
→
B
— vvedenie
→
, 4,
6) |
= (B
→
A
) → (
A
→ B
) — vvedenie
→, 5,
7) |= (
A → B
)
∼ (
B
→
A
)
— svo$istvo 3, vvedenie ∼
, 3, 6.
Teorema 2.7 (Podstanovka formul v tavtologii).
Pust~
B —
formula, soderawa lementarnye vyskazyvani a
1
, . . .
, a
n
;
B
0
poluqaets iz
B
odnovremenno$i podstanovko$i formul A
1
, . . .
, A
n
vmesto a
1
,
. . . , a
n
. Togda, esli |=
B
, to |=
B
0
.
D o k a z a t e l ~ s t v o . Istinnost~ ili lonost~ vyskazyvani
B
0
zavisit ne ot vyskazyvani$i A
1
,
. . . , A
n
, a ot ih znaqeni$i.
Potomu, esli |= B , to
|
=
B
0
.
J
Teorema 2.8 (Teorema o zamene). Pust~
C
A
— formula, soder-
awa podformulu A, i pust~ C
B
poluqaets iz C
A
zameno$i
A na formulu B . Togda, esli |
=
A ∼
B
, to
|
=
C
A
∼ C
B
.
D o k a z a t e l ~ s t v o . Iz |
=
A
∼
B sleduet, qto
A i
B
to-
destvenno ravny i potomu
|
= C
A
∼
C
B
.
J
Metod rezolci$i, primenemy$i v komp~ternyh programmah
dokazatel~stva tavtologi$i, osnovan na sleduwem utverdenii.
Teorema 2.9 (Rezolcii).
Dl lbyh formul
A, B, C
spraved-
livy sekvencii
(nazyvaemye rezolcimi
) : 1)
A, A
∨
B
|=
B ,
2)
A
∨ B, A ∨ C
|=
B ∨ C
.
D o k a z a t e l ~ s t v o . Rezolci 1 est~ pravilo udaleni im-
plikacii, a rezolci 2 — sekvenci 12 teoremy 2.2 posle
primeneni k ne$i sledstvi teoremy 2.7.
J
20
Страницы
- « первая
- ‹ предыдущая
- …
- 18
- 19
- 20
- 21
- 22
- …
- следующая ›
- последняя »
