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é (ab), (ab),
(ab), (ab) 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, (ab), (ba), (ab), (ba), (ab), (ba), (ab), (ba)
 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’(ab),
v’(ab), v’(ab),
v’(ab) jsou
definovány tabulkou:
a b a ab ab ab ab
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 ba a  c YZ XV
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 ab je pravdivá pouze v
případě, že jsou současně pravdivé a
i b
 Konjunkce ab 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 ab je pravdivá, pokud je
pravdivá kterákoliv z komponent a,b
 Disjunkce ab 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 ab 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 ab
 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 ab 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 ab
 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 aX Y  Z UV
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: (pp)
 Zákon vyloučení třetího: pp
 Zákon totožnosti: pp
 Zákon dvojí negace: pp
 Claviův zákon (reductio ad absurdum):
 (pp)p
 (pp)p
 Zákon Dunse Scota: (pp)q
 Př. (A  B)  A  B – ekvivalentní formule
Teoretické základy
informatiky. ZS 2008/09
25
Operace s implikací
 Obměna implikace
 (ab)  (ba)
 Obrácení implikace
 (ab) není totéž jako (ba)!!!
 Implikace není komutativní
 Tranzitivita implikace
 Zákon hypotetického sylogismu
 ((pq)  (qr))  (pr)
Teoretické základy
informatiky. ZS 2008/09
26
Konjunkce a disjunkce
 Konjunkce implikuje každý ze svých
členů
 (pq)  p
 (pq)  q
 Disjunkce je implikována každým ze
svých členů
 p  (pq)
 q  (pq)
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(bc)((ac)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)
 (ab)  (ab)
 Piercova spojka (NOR)
 (ab)  (ab)
 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 (bc))(ab)
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 (bc))(ab)
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
abcab
 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 (bc))(ab)
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 (ac)
(a  c )   b  ( c  a )  přepis (ca) na (ca)
(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 (ac)
 ( 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ž ├ (PZ),
tj. když implikace PZ 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)  (nb)  (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, Aq ├ 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, AB ├ 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í
(ab), (ac), (bd)├ (cd)
 Odvození:
 a  c (P2)
 c  (cd) (disjunkce je implikována…)
 a  (cd) (tranzitivita implikace)
 (cd)  a (obměna implikace)
 b  d (P3)
 d  (cd) (disjunkce je implikována…)
 b  (cd) (tranzitivita implikace)
 (cd)  b (obměna implikace)
 (cd)  (ab) (důsledek výše uvedeného)
 (ab)  (ab) (pravidla pro negování)
 (cd)  (ab) (tranzitivita implikace)
 (ab)  (cd) (obměna implikace)
 (cd) (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 PQ ├ ab
 Jestliže P ├ ab, pak P ├ a, P├ b
 Jestliže (P, a) ├ b, pak P ├ ab
 …