====== MI-FME Formalni metody a specifikace ======
  * http://cs.cas.cz/~ratschan
  * stefan.ratschan at cs.cas.cz
  * FIT 319


==== 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 ===

  * A ⇒ B je zkratka pro ¬ A ∨ B
  * A ⇔ B je zkratka pro A ⇒ B ∧ B ⇒ A
**Z toho plyne:**
  * A ⇒ B je ekvivalentni ¬ B ⇐ ¬ A
  * A ⇔ B je ekvivalentni ¬ B ⇔ ¬ A

<html>
<p style="page-break-after:always"> <p>
</html>

==== 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.


<html>
<p style="page-break-after:always"> <p>
</html>

==== Správnost algoritmu ====


∀x ∀x' . [I (x) ∧ x' = f (x)] ⇒ O(x, x')

==== Axiomatizace seznamů ====
=== Funkční symboly ===
  * cons : T × L → L
  * ﬁrst : 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
  * [ F[x ← 0] ∧ [∀ x . F ⇒ F [x ← x + 1] ] ] ⇒ ∀ x . F

<html>
<p style="page-break-after:always"> <p>
</html>

==== Aserce ====

=== goto l ===
  * αi ⇒ αl

=== input v ===
  * αi ⇒ αi+1[v ← v0]

=== if P then ===

  * [[αi ∧ P] ⇒ αi+1] ∧ [[αi ∧ ¬ P] ⇒ αl ]
  
=== v ← t ===
<code>
@ α
  v1 ← t1; . . . ; vn ← tn
@ α'
</code>  

  * α ⇒ α'[vn ← tn] . . . [v1 ← t1]

**!!Pozor na posloupnost přiřazení!!**


=== while ===

<code>
@ α
while P do
  @β
  . . .
  @β'
@ α'
</code>

  * [α ∧ P] ⇒ β
  * [α ∧ ¬ P] ⇒ α'
  * [β' ∧ P] ⇒ β
  * [β' ∧ ¬ P] ⇒ α'

=== for ===
<code>
@ α
for i ← l to u
  @β
  . . .
  @β'
@ α'
</code>
  * [α ∧ l ≤ u] ⇒ β[i ← l]
  * [α ∧ l > u] ⇒ α'
  * [β' ∧ i < u] ⇒ β[i ← i + 1]
  * β'[i ← u] ⇒ α'