Ekvivalence
A ∧ T ⇔ A
A ∧ F ⇔ F
A ∨ T ⇔ T
A ∨ F ⇔ A
A ∧ B ⇔ B ∧ A
A ∨ B ⇔ B ∨ A
A ∧ (B ∨ C) ⇔ (A ∧ B) ∨ (A ∧ C)
A ∨ (B ∧ C) ⇔ (A ∨ B) ∧ (A ∨ C)
¬¬ A ⇔ A
¬ (A ∧ B) ⇔ ¬ A ∨ ¬ B
¬ (A ∨ B) ⇔ ¬ A ∧ ¬ B
(A ⇔ B) ⇔ (A ⇒ B ∧ B ⇒ A)
(A ⇒ B) ⇔ (¬ B ⇐ ¬ A)
(A ⇔ B) ⇔ (¬ B ⇔ ¬ A)
∃ x. ∃ y.A ⇔ ∃ y. ∃ x.A
∀ x. ∀ y.A ⇔ ∀ y. ∀ x.A
¬∀ x.A je ⇔ ∃ x. ¬ A
¬∃ x.A je ⇔ ∀ x. ¬ A
∀ x . A ∧ B ⇔ [ ∀ x.A] ∧ [ ∀ x.B]
∃ x . A ∨ B ⇔ [ ∃ x.A] ∨ [ ∃ x.B]
∀ x . A ∨ B ⇔ [ ∀ x.A] ∨ B pokud B neobsahuje x
∃ x . A ∧ B ⇔ [ ∃ x.A] ∧ B pokud B neobsahuje x
Pravidla ekvivalence:
A je ekvivalentní A
Pokud A je ekvivalentní B pak B je ekvivalentní A
Pokud A je ekvivalentní B, a B je ekvivalentní C pak A je ekvivalentní C
Implikace, ekvivalence
Důkazní pravidla
Jak zjednodušovat to, co chceme dokázat?
A ∧ B: Nejdřív dokážeme A, pak B
A ∨ B: Předpokládáme ¬ A a dokážeme B
A ⇒ B: Předpokládáme A a dokážeme B.
¬ A: Předpokládáme A a zkusíme najít rozpor. Rozpor: Situace kdy pro určité P, P i ¬ P jsou známé skutečnosti.
Jak produkovat nové známé věci?
A ∧ B: Usoudíme i A i B
A ∨ B: Píšeme nejdřív ”Případ A :”, předpokládáme A a dokončíme důkaz. Pak píšeme ”Případ B :”, předpokládáme B, a dokončíme důkaz.
A ⇒ B: Pokud známe A pak usoudíme B
¬ A: Pokud už hledáme spor, pak místo ¬A dokazujeme A.
Jak zjednodušovat to, co chceme dokázat?
∃ x . A: Vybereme (intuicí, kreativitou) term t, a dokážeme A[x ← t]
∀ x . A: Vybereme novou konstantu a, píšeme ”Nechť a je libovolné ale pevné” a dokážeme A[x ← a]
A ∧ B: Nejdřív dokážeme A, pak B
A ∨ B: Předpokládáme ¬ A a dokážeme B
A ⇒ B: Předpokládáme A a dokážeme B.
¬ A: Předpokládáme A a zkusíme najít rozpor
Jak produkovat nové známé věci?
∃ x . A: Vybereme novou konstantu a, píšeme ”necht’ a je tak, že A[x ← a]”, a přiřadíme A[x ← a] do našeho seznamu známých skutečností.
∀ x . A: Vybereme (intuicí, kreativitou) term t a usoudíme A[x ← t]
A ∧ B: Usoudíme A i B
A ∨ B: Píšeme nejdřív ”Případ A :”, předpokládáme A a dokončíme důkaz. Pak píšeme ”Případ B :”, předpokládáme B, a dokončíme důkaz.
A ⇒ B: Pokud známe A pak usoudíme B
¬ A: Pokud už hledáme spor, pak místo ¬A dokazujeme A.
Správnost algoritmu
∀x ∀x' . [I (x) ∧ x' = f (x)] ⇒ O(x, x')
Axiomatizace seznamů
Funkční symboly
cons : T × L → L
first : L → T
rest : L → L
empty : → L
Axiomy (l ∈ L , x ∈ T ):
∀ l, x . first(cons(x, l)) = x
∀ l, x . rest(cons(x, l)) = l
∀ l, x . l ≠ empty() ⇒ cons(first(l), rest(l)) = l
∀ l, x . cons(x, l) ≠ empty()
Chování first(empty()), rest(empty()) není specifikováno.
Axiomatizace polí
Funkční symboly:
· [·] : A n × { 1, . . . , n } → T
write : A n × { 1, . . . , n } × T → A n
Axiomy (a, b ∈ A n, v ∈ T , i, j ∈ { 1, . . . , n } ):
∀ a, v, i, j . i = j ⇒ write(a, i, v)[j] = v
∀ a, v, i, j . i ≠ j ⇒ write(a, i, v)[j] = a[j]
∀ a, b . [ ∀ i . a[i] = b[i]] ⇔ a = b
Axiomatizace přirozených čísel
Funkční symboly:
0 : → N
1 : → N
+ : N × N → N
· : N × N → N
Axiomy (Peanova aritmetika)
∀ x . x + 1 ≠ 0
∀ x, y . x + 1 = y + 1 ⇒ x = y
∀ x . x + 0 = x
∀ x, y . x + (y + 1) = (x + y) + 1
∀ x . x0 = 0
∀ x, y x(y + 1) = xy + x
Indukce
Pro každou formuli F s přesně jednou volnou proměnnou x, další axiom
Aserce
goto l
if P then
v ← t
@ α
v1 ← t1; . . . ; vn ← tn
@ α'
!!Pozor na posloupnost přiřazení!!
while
@ α
while P do
@β
. . .
@β'
@ α'
[α ∧ P] ⇒ β
[α ∧ ¬ P] ⇒ α'
[β' ∧ P] ⇒ β
[β' ∧ ¬ P] ⇒ α'
for
@ α
for i ← l to u
@β
. . .
@β'
@ α'