Výroková logika
Teoretické základy
informatiky. ZS 2008/09
2
Výroková logika I.
 Součást matematiky
 základní stavební kámen
 informatika stojí na matematice
 Zkoumá tvrzení, výroky, pravdivost,
nepravdivost, důsledky, úsudky
 Přímé použití
 formulace podmínek v programování (a
následné optimalizaci algoritmu)
 návrh logických obvodů (v procesorech aj.)
 formulace databázových dotazů
Teoretické základy
informatiky. ZS 2008/09
3
Výroková logika II.
 Etymologie
 řecké slovo logos = rozum, smysl
 Dělení logiky
 intuitivní logika = co nám připadá ,,logické" na
základě zkušeností
 formální (matematická) logika = zkoumá pouze,
zda dané tvrzení vyplývá z daných předpokladů
 Osobnosti
 G.W. Leibniz, B. Bolzano, G. Boole, G. Cantor, B.
Russel, K. Gödel
Teoretické základy
informatiky. ZS 2008/09
4
Výrok
 Def.: Výrok je tvrzení (oznamovací věta v přirozeném
jazyce), o němž je smysluplné prohlásit, zda je
pravdivé, či nepravdivé.
 Příklady výroků
 Hlavní město Burkiny Faso je Ouagadougou
 Na vrcholku Mt. Everestu je právě teď teplota -8,6°C
 1 + 1 = 3
 Během promítání tohoto slajdu na Zemi vyhynulo 5
biologických druhů
 Nebude-li pršet, nezmoknem
 Věty, které nejsou výroky
 Kolik je hodin?
 Každé koťátko je roztomilé
Teoretické základy
informatiky. ZS 2008/09
5
Složený výrok
 Def.: Složeným výrokem rozumíme takový výrok,
který je tvořen souvětím, tj. více výroky spojenými
logickými spojkami.
 Příklady složených výroků
 Nebude-li pršet, nezmoknem
 Jestliže je to pravda, pak jsem papež
 Pozn.: Za výroky budeme prozatím považovat pouze
tvrzení týkající se jednoho objektu, tj. ne tvrzení typu
 Každé číslo dělitelné 6 je dělitelné 2 a 3
 Kdo jinému jámu kopá, sám do ní padá
Tato tvrzení budou předmětem zkoumání predikátové
logiky
Teoretické základy
informatiky. ZS 2008/09
6
Součásti formálního jazyka VL
 Výroky označíme symboly (Atomické formule)
 výrokové proměnné
 logické proměnné
 atomické výrokové formule
 a, b, c, p, q, r, s, x, y, z, ...
 Pro logické spojky zavedeme symboly
 , , , , 
 Pro zdůraznění priority slouží kulaté závorky
 (, )
Teoretické základy
informatiky. ZS 2008/09
7
Definice výrokové formule
 Za výrokovou formuli (VF) budeme
považovat takovou posloupnost
symbolů jazyka VL, pro kterou platí:
 Každý elementární výrok je (atomická)
VF
 Je-li a VF, pak také a je VF
 Jsou-li a, b VF, pak také (ab), (ab),
(ab), (ab) jsou VF
 Nic jiného není VF
Teoretické základy
informatiky. ZS 2008/09
8
Konstrukce formule
 Konstrukce formule A z množiny atomických
formulí je posloupnost formulí B1, B2, ..., Bn = A
taková, kde Bi, i=1, ..., n, je buď atomická
formule nebo formule, která vznikla aplikací
pravidla 2 gramatiky jazyka výrokové formule
 Konstrukcí formule (p  q)  r  (q  r) je
tedy posloupnost p, q, r,  r, p  q, q  r, (p 
q)  r, (p  q)  r  (q  r)
Teoretické základy
informatiky. ZS 2008/09
9
Podformule výrokových formulí
 Def.: Podformule je souvislá část formule, která je sama formulí.
Je-li poslopnost B1, B2, ..., Bn nejkratší konstrukcí formule A, pak
B1, B2, ..., Bn jsou všechny podformule formule A a číslo n udává
složitost konstrukce formule A.
 Def.: Formule b se nazývá bezprostřední podformulí formule c,
má-li c jeden z následujících tvarů:
b, (ab), (ba), (ab), (ba), (ab), (ba), (ab), (ba)
 Def.: Formule b se nazývá (běžnou) podformulí formule c, jestliže
existuje taková posloupnost formulí
c1, c2, ..., cm, m  1,
že c1 = b, cm = c a ci-1 je bezprostřední podformulí formule ci pro
každé i = 2, 3, ... m.
 Pozn.: Rozklad formule na podformule tvoří stromovou strukturu
až k atomickým formulím
Teoretické základy
informatiky. ZS 2008/09
10
Formační strom formule
 Pro grafickou reprezentaci se někdy používá tzv. strom (viz
obrázek). Strukturou je podobný stromu tak jak jej známe z
běžného života, je ale otočen (má kořen nahoře). Náš strom se
bude skládat z uzlů. Nejvyšší uzel se nazývá kořen stromu. Z
uzlů vycházejí větve (také se jim říká hrany). Uzel, ze kterého
žádné větve nevycházejí, se nazývá list stromu.
Teoretické základy
informatiky. ZS 2008/09
11
Formační strom formule 2
Teoretické základy
informatiky. ZS 2008/09
12
Pravdivostní hodnota výroku
 Def.: Pravdivostní hodnotou
(elementárního) výroku je zobrazení
v: V0  {0,1}
kde V0 je množina výrokových proměnných
 Pozn.: Zobrazení přiřazuje každému výroku
(výrokové proměnné) hodnotu
PRAVDA/NEPRAVDA, TRUE/FALSE, 0/1
 tedy jednobitovou informaci
Teoretické základy
informatiky. ZS 2008/09
13
Pravdivostní hodnota VF
 Zobrazení v rozšíříme na množinu všech VF.
Dostáváme zobrazení
v': V  {0,1}
definované takto:
 v'(a) = v(a) pro a  V0
 jsou-li a,b VF, pak
v'(a), v'(ab),
v'(ab), v'(ab),
v'(ab) jsou
definovány tabulkou:
a b a ab ab ab ab
1 1 0 1 1 1 1
1 0 0 0 1 0 0
0 1 1 0 1 1 0
0 0 1 0 0 1 1
Teoretické základy
informatiky. ZS 2008/09
14
Pravdivostní hodnoty formule
 Určete pravdivostní hodnoty formule
( a c)  [ (b  a)  (a  c)]
X Y Z V
a b c a c a c ba a  c YZ XV
0 0 0 1 1 1 1 0 0 1
0 0 1 1 0 0 1 1 1 0
0 1 0 1 1 1 1 0 0 1
0 1 1 1 0 0 1 1 1 0
1 0 0 0 1 1 1 1 1 1
1 0 1 0 0 1 1 1 1 1
1 1 0 0 1 1 0 1 0 1
1 1 1 0 0 1 0 1 0 1
Teoretické základy
informatiky. ZS 2008/09
15
Negace ()
 Česky: ,,není pravda, že", předpona
,,ne"
 Anglicky: not
 Má opačnou pravdivostní hodnotu,
než původní VF
 Negace a je pravdivá, pokud je a
nepravdivé
 Negace a je nepravdivá, pokud je a
pravdivé
Teoretické základy
informatiky. ZS 2008/09
16
Konjunkce ()
 Česky: ,,a zároveň"
 Anglicky: ,,and"
 Též logický součin
 Konjunkce ab je pravdivá pouze v
případě, že jsou současně pravdivé a
i b
 Konjunkce ab je nepravdivá, pokud
je kterákoliv z komponent a,b
nepravdivá
Teoretické základy
informatiky. ZS 2008/09
17
Disjunkce ()
 Česky: ,,nebo"
 Anglicky: ,,or"
 Též logický součet
 Disjunkce ab je pravdivá, pokud je
pravdivá kterákoliv z komponent a,b
 Disjunkce ab je nepravdivá pouze v
případě, že neplatí ani a, ani b.
Teoretické základy
informatiky. ZS 2008/09
18
Implikace ()
 Česky: ,,z toho plyne"
 Anglicky: ,,if ... then ... "
 V implikaci ab nazýváme
 a předpoklad (premisa)
 b závěr (konkluze)
 Implikace je pravdivá, pokud z pravdivého
předpokladu plyne pravdivý závěr, anebo pokud
neplatí předpoklad
 Implikace je nepravdivá pouze v případě, že z
pravdivého předpokladu plyne nepravdivý závěr
 Jiná vyjádření implikace ab
 Z a plyne b. Jestliže a, pak b. B je důsledkem a. A je
postačující podmínkou pro b. B je nutnou podmínkou
pro a.
Teoretické základy
informatiky. ZS 2008/09
19
Ekvivalence ()
 Česky: ,,právě tehdy, když"
 Anglicky: ,,if and only if"
 Ekvi-valence = stejná hodnota
 Ekvivalence ab je pravdivá tehdy, mají-li výroky a a
b stejnou pravdivostní hodnotu
 tj. jsou oba pravdivé, nebo oba nepravdivé
 Ekvivalence je nepravdivá, pokud mají a a b různou
pravdivostní hodnotu
 Jiná vyjádření ekvivalence ab
 A platí tehdy a jen tehdy, když b. B platí tehdy a jen
tehdy, když a. A je nutnou a postačující podmínkou
pro b. B je nutnou a postačující podmínkou pro a.
Teoretické základy
informatiky. ZS 2008/09
20
Příklad
 Určete pravdivostní hodnoty formule
[(a  (b  c)]  [(a  b)  (a c)]
Teoretické základy
informatiky. ZS 2008/09
21
Příklad - tautologie
[(a  (b  c)]  [(a  b)  (a c)]
X Y Z U V
a b c b  c a  b a c aX Y  Z UV
0 0 0 0 1 1 1 1 1
0 0 1 1 1 1 1 1 1
0 1 0 1 1 1 1 1 1
0 1 1 1 1 1 1 1 1
1 0 0 0 0 0 0 0 1
1 0 1 1 0 1 1 1 1
1 1 0 1 1 0 1 1 1
1 1 1 1 1 1 1 1 1
Teoretické základy
informatiky. ZS 2008/09
22
Tautologie a kontradikce
 Def.: Výrokovou formuli nazveme tautologie, pokud je
vždy pravdivá bez ohledu na pravdivostní hodnotu
výrokových proměnných, které obsahuje.
 Označení: |= [(a  (b  c)]  [(a  b)  (a c)]
 Def.: Výrokovou formuli nazveme kontradikce, pokud
je vždy nepravdivá bez ohledu na pravdivostní hodnotu
výrokových proměnných, které obsahuje
Teoretické základy
informatiky. ZS 2008/09
23
Věta o substitucích
 Nechť T(x1, x2, ... xn) je tautologie.
Jestliže za libovolnou z proměnných xi
dosadíme libovolnou formuli, potom
výsledná formule je opět tautologií.
 Analogické tvrzení platí i pro
kontradikce
Teoretické základy
informatiky. ZS 2008/09
24
Význačné tautologie
 Zákon sporu: (pp)
 Zákon vyloučení třetího: pp
 Zákon totožnosti: pp
 Zákon dvojí negace: pp
 Claviův zákon (reductio ad absurdum):
 (pp)p
 (pp)p
 Zákon Dunse Scota: (pp)q
 Př. (A  B)  A  B ­ ekvivalentní formule
Teoretické základy
informatiky. ZS 2008/09
25
Operace s implikací
 Obměna implikace
 (ab)  (ba)
 Obrácení implikace
 (ab) není totéž jako (ba)!!!
 Implikace není komutativní
 Tranzitivita implikace
 Zákon hypotetického sylogismu
 ((pq)  (qr))  (pr)
Teoretické základy
informatiky. ZS 2008/09
26
Konjunkce a disjunkce
 Konjunkce implikuje každý ze svých
členů
 (pq)  p
 (pq)  q
 Disjunkce je implikována každým ze
svých členů
 p  (pq)
 q  (pq)
Teoretické základy
informatiky. ZS 2008/09
27
Komutativní zákony
 Operace je komutativní, pokud
nezáleží na pořadí operandů.
 Komutativní jsou konjunkce,
disjunkce a ekvivalence.
 NE implikace!
 (a  b)  (b  a)
 (a  b)  (b  a)
 (a  b)  (b  a)
Teoretické základy
informatiky. ZS 2008/09
28
Asociativní zákony
 Operace je asociativní, pokud
nezáleží na uzávorkování
 Asociativní jsou konjunkce, disjunkce
a ekvivalence.
 NE implikace!
 ((a  b)  c)  (a  (b  c))
 ((a  b)  c)  (a  (b  c))
 ((a  b)  c)  (a  (b  c))
Teoretické základy
informatiky. ZS 2008/09
29
Distributivní zákony
 ,,roznásobování" logických spojek
 (a  (b  c))  ((a  b)  (a  c))
 (a  (b  c))  ((a  b)  (a  c))
Teoretické základy
informatiky. ZS 2008/09
30
Dualita konjunkce a disjunkce
 deMorganovy zákony
 negace konjunkce je disjunkce negací
 negace disjunkce je konjunkce negací
 (a  b)  (a  b)
 (a  b)  (a  b)
Teoretické základy
informatiky. ZS 2008/09
31
Logická ekvivalence výroků
 Def.: Řekneme, že výroky p a q jsou
logicky ekvivalentní, jestliže
výroková formule a  b je tautologie
 Logicky ekvivalentní výroky mají tedy
vždy stejnou pravdivostní hodnotu
 Příklady logicky ekvivalentních výroků
 (p  (q  r)))  ((p  q)  r))
 (p  q)  ((p  q)  (q  p))
Teoretické základy
informatiky. ZS 2008/09
32
Negování složených výroků
 Pozn.: Negovat složený výrok znamená
formulovat výrok, který je logicky
ekvivalentní s negací původního výroku a
neobsahuje negaci složeného výroku jako
svoji podformuli
 Pravidla pro negování logických spojek
 (a  b)  (a  b)
 (a  b)  (a  b)
 (a  b)  (a  b)
 (a  b)  ((a  b)  (b  a))
 Příklad: Negujte výrokovou formuli
(a(bc)((ac)b)
Teoretické základy
informatiky. ZS 2008/09
33
Úplný systém logických spojek
 Def.: Řekneme, že množina logických spojek L tvoří
úplný systém logických spojek, jestliže ke každé
formuli existuje formule, která je s ní logicky
ekvivalentní, a která obsahuje pouze spojky z L.
 Úplný systém log. spojek tvoří:
 negace a implikace
 negace a konjunkce
 negace a disjunkce
 Otázka: Kolik různých (binárních) logických spojek
můžeme definovat?
 Netvoří některá z nich sama o sobě úplný systém?
Teoretické základy
informatiky. ZS
2008/09
34
Piercova a Shefferova spojka
 Shefferova spojka (NAND)
 (ab)  (ab)
 Piercova spojka (NOR)
 (ab)  (ab)
 Všechny logické spojky je možné
vyjádřit pouze pomocí
Shefferovy/Piercovy spojky
Teoretické základy
informatiky. ZS
2008/09
35
Způsoby zápisu výrazů
 Infixový zápis
 Klasický způsob ­ operátor je mezi operandy
 3 + 5, a  b
 Prefixový zápis
 Operátor je před operandy
 + 3 5,  a b
 Postfixový zápis
 Operátor je za operandy
 3 5 +, a b 
 Jedná se o různý zápis téhož výrazu
 Jiná syntaxe, jiný způsob vyhodnocení
 Stejná sémantika, stejný výsledek
 Prefix a postfix nepotřebují závorky
Teoretické základy
informatiky. ZS
2008/09
36
Převod z infixu do prefixu
 Pomocí stromového rozkladu
 Nakreslíme si rozklad výrazu
 Přečteme kořen, pak rekurzivně levý
podstrom a rekurzivně pravý podstrom
 Jednodušší výrazy lze intuitivně
 Příklad: Vyjádřete prefixovou notací
formuli (a (bc))(ab)
Teoretické základy
informatiky. ZS
2008/09
37
Převod z infixu do postfixu
 Předpokládejme ,,dobře uzávorkovaný"
výraz
 Algoritmus slepé koleje
 Čteme výraz v infixu zleva doprava
 Proměnná pokračuje na výstup
 Operátor padá do zásobníku (slepé koleje)
 Levá závorka padá do zásobníku (slepé koleje)
 Pravá závorka vyráží ze zásobníku vše až po
levou závorku. Závorky na výstup nepíšeme
 Na konci vyprázdníme zásobník
 Příklad: Vyjádřete postfixovou notací formuli
(a (bc))(ab)
Teoretické základy
informatiky. ZS
2008/09
38
Vyhodnocení výrazu v postfixu
 Pomocí zásobníkového automatu
 Čteme výraz zleva doprava
 Přečteme-li operand, uložíme jej na zásobník
 Přečteme-li operátor, vybereme ze zásobníku tolik
operandů, kolik je arita operátoru, aplikujeme na ně
operátor a výsledek uložíme na zásobník
 Po dočtení výrazu je na zásobníku pouze výsledek
výrazu
 Stejným způsobem lze převádět z postfixu do infixu
 Příklad: Převeďte z postfixu do infixu formuli
abcab
 Příklad: Vyhodnoťte postfixově zapsaný aritmetický
výraz 16 4 + 2 3 2 + * / 1 -
Teoretické základy
informatiky. ZS
2008/09
39
Disjunktivní normální forma
 Výroková formule je v disjunktivním
normálním tvaru (DNF), je-li
disjunkcí formulí, pro které platí:
 každá je konjunkcí atomických
výrokových formulí a jejich negací
 v žádné se nevyskytuje žádná atomická
formule současně se svou negací
 DNF je úplná, pokud jsou ve všech
konjunkcích stejné atomické formule
Teoretické základy
informatiky. ZS
2008/09
40
Disjunktivní normální forma 2
 Příkladem formule v DNF je
(a  b  c)  (a  b  c)
 Př.: Najděte úplnou disjunktivní
normální formu formule
A = (b  c)  (a  b)
Teoretické základy
informatiky. ZS
2008/09
41
Disjunktivní normální forma př.
A = (b  c)  (a  b)
(a  b  c)  (a  b  c)  (a  b  c)
X Y
A b c c b  c b a  b X  Y
0 0 0 1 1 1 0 0
0 0 1 0 0 1 0 1
0 1 0 1 1 0 0 0
0 1 1 0 1 0 0 0
1 0 0 1 1 1 1 1
1 0 1 0 0 1 1 1
1 1 0 1 1 0 0 0
1 1 1 0 1 0 0 0
Teoretické základy
informatiky. ZS
2008/09
42
Konjunktivní normální forma
 Výroková formule je v
konjunktivním normálním tvaru
(KNF), je-li konjunkcí formulí, pro
které platí:
 každá je disjunkcí atomických
výrokových formulí a jejich negací
 v žádné se nevyskytuje žádná atomická
formule současně se svou negací
 KNF je úplná, pokud jsou ve všech
konjunkcích stejné atomické formule
Teoretické základy
informatiky. ZS
2008/09
43
DNF a KNF
 Ke každé výrokové formuli lze nalézt
ekvivalentní formuli v úplném DNF a KNF
 Úplný DNF/KNF je určen jednoznačně až na
volbu a pořadí proměnných
 I prázdná disjunkce (disjunkce prázdné
množiny konjunkcí) je v DNF a v KNF
 Jaký je algoritmus převodu do DNF/KNF?
 Pomocí pravdivostní tabulky
 Pomocí pravidel pro úpravy logických formulí
 Převeďte do (úplné) DNF a KNF formuli
(a (bc))(ab)
Teoretické základy
informatiky. ZS
2008/09
44
Pravidla při převodu do DNF
1) Nahrazení výrokových spojek  a  pomocí funkčně úplné množiny , , , tedy
pomocí ekvivalencí
|= ( X  Y )  ( X  Y )
|= ( X  Y )  [( X  Y )  ( Y  X)]  [( X  Y )  ( Y  X)]
2) Převedení negací dovnitř závorek pomocí de Morganových pravidel
|= ( X  Y )  ( X   Y )
|= ( X  Y )  ( X   Y )
3) Odstranění dvojí negace pomocí ekvivalence
|= ( X )  X
4) Použití distributivních zákon
|= ( X  ( Y  Z ) ) (( X  Y )  ( X  Z ))
|= ( X  ( Y  Z ) ) (( X  Y )  ( X  Z ))
Teoretické základy
informatiky. ZS
2008/09
45
Pravidla při převodu do KNF
Převedení formule do ekvivalentní konjunktivní normální formy lze provést též přímo
úpravami bez pomoci tabulky. Používáme k tomu následující ekvivalentní úpravy:
1) nahrazení spojky  spojkami  a  podle ekvivalence
2) Přepis spojky  spojkami  a  podle ekvivalence
3) Použití podle potřeby De Morganových zákonů a distributivních zákonů.
Teoretické základy
informatiky. ZS
2008/09
46
Příklad převodu
Převeďte ekvivalentními úpravami do DNF formuli
[ (a  b)  a]  [( a  b ) ]
Budeme postupně formuli přepisovat pomocí ekvivalencí:
[ (a  b)  a]  [( a  b ) ] použijeme ekvivalence
[ ( a  b)  a]  (a  b) ekvivalence
[ (a  a)  (b  a) ]  (a  b) ekvivalence
[false  (b  a) ]  (a  b) ekvivalence
(b  a)  (a  b)
Další:
(a  (b  a)) do DNF
( a  c )   b  ( c  a )  do KNF
Teoretické základy
informatiky. ZS
2008/09
47
Příklad řešení
( a  c )   b  ( c  a )  přepis ( a  c) na (ac)
(a  c )   b  ( c  a )  přepis (ca) na (ca)
(a  c )   b  (c  a )  přepis 
( a  c )   b  ( c  a )  ( a  c ) na ( a   c )
( a   c )   b  ( c  a ) , úprava 
 ( a   c)  b    ( a   c )  (c  a)  ( a  c) na (ac)
 ( a   c )  b   (a  c )  ( c  a )  ... na true
 ( a   c )  b  true ...  true
 ( a   c )  b podle
( a  b )  ( c  b )
Teoretické základy
informatiky. ZS
2008/09
48
Deduktivní soustava výrokové
logiky
 Správnost a nesprávnost úsudků
 Jak rozhodnout, zda je úsudek
správný?
Teoretické základy
informatiky. ZS
2008/09
49
Formální definice úsudku I.
Nechť P1, P2, ... Pm jsou výrokové formule v
proměnných x1, x2, ... xk. Nechť rovněž Z
je výroková formule.
Říkáme, že z formulí P1, P2, ... Pm vyplývá
závěr Z a píšeme
P1, P2, ... Pm  Z
právě tehdy, když pro libovolné pravdivostní
hodnoty proměnných x1, x2, ... xk platí, že
nabývá-li pravdivostní funkce formulí P1,
P2, ... Pm současně hodnoty 1, pak nabývá
i pravdivostní funkce formule Z hodnoty 1.
Teoretické základy
informatiky. ZS
2008/09
50
Formální definice úsudku II.
 P1, P2, ... Pm  Z
právě tehdy, když
 (P1 P2  ...  Pm)  Z
 P  Z právě tehdy, když  (PZ),
tj. když implikace PZ je tautologie
Teoretické základy
informatiky. ZS
2008/09
51
Ověření správnosti úsudku
Úsudek
P1, P2, ... Pm  Z
je správný, jestliže formule
(P1 P2  ...  Pm)  Z
je tautologie.
Úsudek je tedy správný, jestliže implikace
důsledku z konjunkce premis je tautologie.
Teoretické základy
informatiky. ZS
2008/09
52
Příklad: Ověření správnosti úsudku
 Předpoklady:
 Jestliže prší a mrzne, vzniká náledí
 Jestliže vzniká náledí, v této zatáčce se vždy někdo
vybourá
 V této zatáčce se nikdo nevyboural
 Závěr:
 Usuzujeme, že nepršelo.
 Formalizujeme předpoklady a závěr
 (p  m)  n; n  b; b
 p
 Ověříme, zda je tautologií formule
 (((p  m)  n)  (nb)  (b))  p
Teoretické základy
informatiky. ZS
2008/09
53
Pravidlo odloučení (modus ponens)
 Nechť X a Y jsou formule.
 Potom platí (X, X  Y)  Y.
 Tedy z platnosti formulí X a X  Y
můžeme odvodit platnost formule Y.
 Důkaz plyne z pravdivostní tabulky
formule (X  (X  Y))  Y
Teoretické základy
informatiky. ZS
2008/09
54
Příklad: Ověření správnosti úsudků
 Předpoklady:
 Jestliže Jarda nepřišel ke snídani, je nemocný
 Jarda přišel ke snídani
 Co z toho plyne?
 Jarda je unavený
 Jarda je doma
 Jarda přišel ke snídani
 Jarda je nemocný
 Jarda není nemocný
Teoretické základy
informatiky. ZS
2008/09
55
Substituční pravidlo pro proměnnou
 Buď X formule a q její proměnná.
 Jestliže do X za q dosadíme formuli A,
pak formuli vzniklou touto substitucí
označíme S(A/q, X)
 Pak platí
X, Aq  S(A/q, X)
Teoretické základy
informatiky. ZS
2008/09
56
Substituční pravidlo pro proměnnou
v tautologii
 Buď T tautologie a q její proměnná.
 Jestliže do T za q dosadíme formuli A,
pak formuli vzniklou touto substitucí
označíme S(A/q, T)
 Pak platí
T  S(A/q, T)
Teoretické základy
informatiky. ZS
2008/09
57
Substituční pravidlo pro formuli
 Buď X formule a B její podformule.
 Jestliže do X za B dosadíme formuli A,
pak formuli vzniklou touto substitucí
označíme S(A/B, X)
 Pak platí
X, AB  S(A/B, X)
Teoretické základy
informatiky. ZS
2008/09
58
Odvození formule
 Formule Z je důsledkem formulí P1, P2, ...
Pm právě tehdy, když existuje posloupnost
formulí X1, X2, ... Xn taková, že Xn = Z a pro
každé i platí:
 Xi = Pj pro vhodné j
 Xi = S(A/t, T) nebo Xi = S(A/B, T)
 kde T je libovolná tautologie
 Xi je důsledkem aplikace pravidla modus ponens
na některé z předchozích formulí
 Tato posloupnost formulí se nazývá
odvození formule Z z formulí P1, P2, ... Pm.
Teoretické základy
informatiky. ZS
2008/09
59
Příklad odvození
 Dokažte odvozením, že platí
(ab), (ac), (bd) (cd)
 Odvození:
 a  c (P2)
 c  (cd) (disjunkce je implikována...)
 a  (cd) (tranzitivita implikace)
 (cd)  a (obměna implikace)
 b  d (P3)
 d  (cd) (disjunkce je implikována...)
 b  (cd) (tranzitivita implikace)
 (cd)  b (obměna implikace)
 (cd)  (ab) (důsledek výše uvedeného)
 (ab)  (ab) (pravidla pro negování)
 (cd)  (ab) (tranzitivita implikace)
 (ab)  (cd) (obměna implikace)
 (cd) (modus ponens)
Teoretické základy
informatiky. ZS
2008/09
60
Další vlastnosti úsudků
 Jestliže  a, pak b a pro lib. b
 Tautologie je důsledkem libovolné formule
 Jestliže  a, a b, pak také  b
 Důsledkem tautologie je opět tautologie
 Nechť P,Q jsou množiny formulí, a, b
formule:
 Jestliže P  a, Q  b, pak PQ  ab
 Jestliže P  ab, pak P  a, P b
 Jestliže (P, a)  b, pak P  ab
 ...