Составители:
Рубрика:
Opredelenie 2.6 (Shema aksiom IS). A
`A
.
Opredelenie 2.7 (Pravila vyvoda IS). Pravilami vyvoda IS
nazyvats shemy vida
Σ
1
, . . . , Σ
k
Σ
, gde sekvenci Σ nazyvaets
neposredstvennym sledstviem sekvenci$i
Σ
1
, . . . , Σ
k
po dannomu
pravilu vyvoda. Pravilami vyvoda IS vlts:
1)
Γ
1
`
A
; Γ
2
`B
Γ
1
, Γ
2
`A
∧
B
(
vvedenie
∧
)
,
2)
Γ `A
∧
B
Γ
`
A
(
udalenie ∧),
3)
Γ
`A
∧B
Γ
`B
(udalenie ∧
),
4)
Γ
`
A
Γ
`A ∨ B
(vvedenie ∨
),
5)
Γ
`B
Γ
`A
∨
B
(vvedenie
∨)
,
6)
Γ
1
`A
∨ B
; Γ
2
, A
`C ;
Γ
3
, B `
C
Γ
1
, Γ
2
, Γ
3
`C
(
udalenie ∨
),
7)
Γ, A `B
Γ
`
A → B
(vvedenie
→)
,
8)
Γ
1
`
A ; Γ
2
`
A →
B
Γ
1
, Γ
2
`B
(
udalenie →
)
,
9)
Γ, A
`
Γ
`
A
(
vvedenie
),
10)
Γ
1
`A
;
Γ
2
`
A
Γ
1
, Γ
2
`
(
svedenie k protivoreqi)
,
11)
Γ,
A
`
Γ `A
(
udalenie
)
,
12)
Γ `
Γ `A
(utonqenie)
,
13)
Γ
`
A
Γ, B `
A
(
rasxirenie
)
,
14)
Γ
1
, A, B, Γ
2
`C
Γ
1
, B, A, Γ
2
`
C
(
perestanovka),
15)
Γ
1
, A, A, Γ
2
`
C
Γ
1
, A, Γ
2
`
C
(sokrawenie
)
.
27
Страницы
- « первая
- ‹ предыдущая
- …
- 25
- 26
- 27
- 28
- 29
- …
- следующая ›
- последняя »