Logica voor Informatica
Mehdi Dastani
Literals
Een literal is een propositieletter, of de negatie
van een propositieletter, bijvoorbeeld:
¬p , q , ¬r , r
Literals = { p , ¬p | p is een propositieletter }
Als A is een literal, dan ~A is het complement
van A.
~p = ¬p
en
~¬p = p
Normaalvormen
Disjunctieve normaalvorm (DNF)
Disjunctie van conjuncties van literals
(r ∧ q ∧ ¬r) ∨ (¬q ∧ s ∧ t) ∨ (¬p ∧ r)
Conjunctieve normaalvorm (CNF)
Conjunctie van disjuncties van literals
(r ∨ q ∨ ¬r) ∧ (¬q ∨ s ∨ t) ∧ (¬p ∨ r)
Disjunctieve normaalvormen
(DNF)
(r ∧ q ∧ ¬r) ∨ (¬q ∧ r) ∨ (¬p ∧ r)
Een DNF is waar a.e.s.a. tenminste een
component waar is.
Een component is waar a.e.s.a. er geen
complementair paar literals in voorkomt.
Dus, een DNF is waar a.e.s.a. een component
geen complementair paar literals bevat.
Converteren naar DNF
m.b.v. waarheidtafel
(p→q)→p
p
q
p→q (p→q)→p
F
F
T
T
F
T
F
T
T
T
F
T
F
F
T
T
(p ∧ ¬q) ∨ (p ∧ q)
Converteren naar DNF
m.b.v. herschrijven
1.
Elimineer → dmv
A → B ≡ ¬A ∨ B
2.
Elimineer ↔ dmv
A ↔ B ≡ (¬A ∨ B) ∧ (¬B ∨ A)
3.
4.
5.
Pas distributieve wet
A ∧ (B ∨ C)
(A ∨ B) ∧ C
≡ (A ∧ B) ∨ (A ∧ C)
≡ (A ∧ C) ∨ (B ∧ C)
Breng negatietekens binnen haakjes
¬(A ∧ B) ≡ ¬A ∨ ¬B
&
¬(A ∨ B) ≡ ¬A ∧ ¬B
Elimineer dubbele negaties mbv ¬¬A ≡ A
Conjunctieve normaalvormen
(CNF)
(r ∨ q ∨ ¬r) ∧ (¬q ∨ s ∨ t) ∧ (¬p ∨ r)
Een CNF is waar a.e.s.a. alle componenten waar
zijn.
Een component is waar a.e.s.a. er een
complementair paar literals in voorkomt.
Dus, een CNF is een waar a.e.s.a. in alle
componenten een complementair paar literals
voorkomen.
Converteren naar CNF
m.b.v. herschrijven
(¬p ∧ (¬q → r)) ↔ s
((¬p ∧ (¬q → r)) → s)
((¬p ∧ (¬¬q ∨ r)) → s)
((¬p ∧ (q ∨ r)) → s)
(¬(¬p ∧ (q ∨ r)) ∨ s)
((¬¬p ∨ ¬(q ∨ r)) ∨ s)
((p ∨ (¬q ∧ ¬r)) ∨ s)
(((p ∨ ¬q) ∧ (p ∨ ¬r)) ∨ s)
(((p ∨ ¬q) ∨ s) ∧ ((p ∨ ¬r) ∨ s))
(p ∨ ¬q ∨ s) ∧ (p ∨ ¬r ∨ s)
∧
∧
∧
∧
∧
∧
∧
∧
∧
(s →(¬p ∧ (¬q → r)))
(s →(¬p ∧ (¬¬q ∨ r)))
(s →(¬p ∧ (q ∨ r)))
(¬s ∨ (¬p ∧ (q ∨ r)))
(¬s ∨ (¬p ∧ (q ∨ r)))
(¬s ∨ (¬p ∧ (q ∨ r)))
((¬s ∨ ¬p) ∧ (¬s ∨ (q ∨ r)))
((¬s ∨ ¬p) ∧ (¬s ∨ (q ∨ r)))
(¬s ∨ ¬p) ∧ (¬s ∨ q ∨ r)
Converteren naar CNF
via DNF
Laat A een willekeurige propositie zijn.
Converteer ¬A naar DNF vorm, bijv.
¬A = (p1 ∧ p2 ∧ … ) ∨ (q1 ∧ q2 ∧ …) ∨ …
CNF van A is dan
¬¬A = ¬ ((p1 ∧ p2 ∧ … ) ∨ (q1 ∧ q2 ∧ …) ∨ …
= ¬(p1 ∧ p2 ∧ … ) ∧ ¬(q1 ∧ q2 ∧ …) ∧ …)
= (¬p1 ∨ ¬p2 ∨ … ) ∧ ¬(¬q1 ∨ ¬q2 ∨ …) ∧ …)
Toepassing: logische circuits
A
B
∧
A
A∧B
A∨B
B
A
¬
¬A
Van waarheidstafel naar circuit
Gegeven een (waarheidstafel voor een)
waarheidsfunctie R kunnen we op systematische
manier een logisch circuit maken dat R realiseert:
Beschouw alle rijen waarvoor v(R) = T
Iedere rij levert een disjunct op die zelf bestaat uit
een conjunctie van zgn literals
Vereenvoudig zo mogelijk mbv regels voor ≡
Voorbeeld
A B C R(A,B,C)
F
F
F
F
F
F
T
F
F
T
F
T
F
T
T
F
T
F
F
F
T
F
T
T
T
T
F
T
T
T
T
F
Voorbeeld
Deze procedure levert nu op voor R:
(¬A ∧B ∧ ¬C) ∨
(A ∧¬B ∧ C) ∨
(A ∧ B ∧ ¬C)
Een formule in zgn ‘Disjunctieve Normaalvorm’ (DNF)
Dit is logisch equivalent (≡) met:
(B ∧ ¬C) ∨ (A ∧¬B ∧ C)
Hiervoor circuit maken
Alternatieve methoden om
geldigheid formules te bepalen
In de praktijk is het werken met waarheidstafels
onhandig omdat ze erg groot worden in een beetje
realistische toepassing: een waarheidstafel met n
atomen heeft 2n rijen.
Voor het vaststellen van geldigheid alle rijen te
bekijken: (te)veel werk.
Zoeken naar alternatieven: bijv. zgn. semantische
tableaux en (natuurlijke) deductie.
Semantische tableaux
Semantische tableaux
Een semantisch tableau is een (vertakkende)
sequentie van propositionele vormen,
geconstrueerd volgens bepaalde regels, vaak
gerepresenteerd in een boom.
Deze methode levert modellen voor een
formule als deze bestaan: ze geeft op
systematische wijze aan welke atomen waar
moeten worden gemaakt om een formule waar
te maken, en geeft ook aan als dit niet kan!
Semantische tableaux
Kan een verzameling proposites waar zijn,
d.w.z. kan een verzameling proposities een
model hebben.
Voorbeeld: kan {p∧q , ¬p} een model hebben?
p∧q ° p
p,q ° p
X
Regels semantische tableaux
Regel (∧-links)
Regel (∧-rechts)
°A ∧ B
A∧B°
A,B°
°A
°B
Regels semantische tableaux
Regel (∨-links)
Regel (∨-rechts)
A∨B°
°A∨B
A°
°A,B
B°
Regels semantische tableaux
Regel (→-links)
A→B°
°A
Regel (→-rechts)
°A → B
B°
A°B
Regels semantische tableaux
Regel (↔-links)
A↔B°
A→B, B→A °
Regel (↔-rechts)
°A ↔ B
°A→B
°B→A
Regels semantische tableaux
Regel (¬-links)
¬A °
°A
Regel (¬-rechts)
°¬A
A°
Regels semantische tableaux
Regel 0
Als een logische vorm A in beide kanten van °
voorkomt, dan is A inconsistent en wordt de tak
gesloten (‘closed’).
Voorbeeld: {¬(A → B), ¬A ∨ B}
is inconsistent
¬(A → B),¬A ∨ B °
¬A °
°A
°A→B
A°B
closed
B°
°A → B
A°B
Wel of geen modellen?
Als alle takken ‘sluiten’ dan is de
verzameling proposities waar je mee begon
inconsistent (d.w.z. heeft geen model)
Als minstens een tak ‘open’ blijft, geeft dit
een model voor de verzameling proposities!
Voorbeeld: { P, Q, Q →¬P }
is inconsistent
P , Q , Q →¬P °
°Q
closed
°P
closed
Voorbeeld: {P, ¬Q, Q →¬P}
is consistent
P , Q →¬P ° Q
°Q
°P
closed
Model: v(Q)=F, v(P)=T
Geldigheid van een formule
Semantische tableaux leveren een
systematische manier om modellen van
een propositie te vinden
Als een propositie geen modellen heeft, is
deze inconsistent
Geldigheid is indirect te checken via:
A is inconsistent (contradictie)
⇔
¬A is geldig (tautologie)
Voorbeeld: A ∨ (¬B → ¬A)
is geldig (tautologie)
¬(A ∨ (¬B → ¬A)) °
°A ∨ (¬B → ¬A)
°A , ¬B → ¬A
¬B °A , ¬A
A °A , B
closed
Semantische tableaux en
argumenten
We kunnen de semantische tableaux methode
ook gebruiken om te checken of argumenten
geldig zijn
Beschouw weer het argument:
R → N, R N
De geldigheid hiervan is aan te tonen door te
controleren of de verzameling { R→N , R , ¬N }
inconsistent is, d.w.z. geen modellen heeft.
Semantische tableaux en
argumenten
R → N, R ° N
°R
closed
N°
closed
Dwz geen modellen: {R → N, R, ¬N} inconsistent,
dus argument R → N, R N geldig
Semantische tableaux en
argumenten
A, B → A
B is geen geldig argument.
We laten met sem. tableaux zien dat de verzameling
{A, B → A, ¬B} consistent is, d.w.z. een model heeft:
A, B → A ° B
°B
open
A°
open
model v(A)=T, v(B)=F
Nogmaals
Logische Gevolg en Model
Model (Interpretatie):
m B
Het model m (of interpretatie m) maakt B waar.
Merk op dat een model een rij van de
waarheidstafel is.
Logische Gevolg:
A1 , … , An B
Elk model van proposities A1 , … , An is ook een
model van propositie B.
Semantische tableaux:
Correctheid
Gezondheid
Als A1 , … , An
beginnend met
een open tak.
B, dan elk mogelijk tableaux
A1 , … , An °B heeft tenminste
Volledigheid
Als A1 , … , An B, dan elk mogelijk tableaux
beginnend met A1 , … , An °B bestaat uit
alleen takken die gesloten kunnen worden.
Normaalvormen met tableaux
DNF van een propositie A is te verkrijgen
door een tableaux te maken voor A °
CNF van een propositie A is te verkrijgen
door een tableaux te maken voor ° A.
(p→q)→p °
°p→q
° (p→q)→p
p°
p°q
(p ∧ ¬q) ∨ (p)
p→q ° p
q°p
°p
(¬q ∨ p) ∧ (p)
© Copyright 2024 ExpyDoc
