Theorie Formele logica

Theorie Formele logica Daan Pape 2e bach informatica Ugent 21 januari 2013

1

Inhoudsopgave 1 Propositie logica 1.1 Terminologie en notatie . . . . . 1.2 Regels voor natuurlijke deductie 1.3 Afgeleide bewijsregels . . . . . . 1.4 Bewijstechnieken . . . . . . . . . 1.5 Propositielogica . . . . . . . . . . 1.6 Conjunctieve normaalvorm . . . 1.7 Horn clausules . . . . . . . . . . 1.8 SAT solvers . . . . . . . . . . . . 1.9 Tseitintransformatie . . . . . . .

. . . . . . . . .

3 3 3 4 6 6 12 15 16 18

2 Predikaatlogica 2.1 Begrippen en definities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.2 Regels voor natuurlijke deductie . . . . . . . . . . . . . . . . . . . . . . . . . 2.3 Modellen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

19 19 21 22

3 Verification by model checking 3.1 Lineaire-tijd temporele logica of LTL . . . 3.2 Computational Tree Logic of CTL . . . . 3.3 Algoritmes voor model checking . . . . . . 3.4 Karakterisering van CTL via vaste punten 3.5 CTL* en de vergelijking met CTL en LTL

. . . . .

30 31 36 43 46 47

. . . . .

47 47 51 55 55 58

5 Binaire beslissingsdiagramma’s 5.1 Voorstellen van booleanse functies . . . . . . . . . . . . . . . . . . . . . . . . 5.2 Algoritmen voor gereduceerde OBDD’s . . . . . . . . . . . . . . . . . . . . . . 5.3 Symbolic model checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

59 59 63 66

6 Algebra¨ısche normaalvorm en resolutie 6.1 Adequate verzamelingen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6.2 Algebra¨ısche normaalvorm . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

71 71 71

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . .

. . . . . . . . .

. . . . .

. . . . . . . . .

. . . . .

. . . . . . . . .

. . . . .

. . . . . . . . .

. . . . .

4 Modale logica en agenten 4.1 Begrippen en notaties van basis modale logica . . . 4.2 Logische engineering en correspondentietheorie . . 4.3 Natuurlijke deductie . . . . . . . . . . . . . . . . . 4.4 Redeneren over kennis in een multi-agentensysteem 4.5 Natuurlijke deductie . . . . . . . . . . . . . . . . .

2

. . . . . . . . .

. . . . .

. . . . .

. . . . . . . . .

. . . . .

. . . . .

. . . . . . . . .

. . . . .

. . . . .

. . . . . . . . .

. . . . .

. . . . .

. . . . . . . . .

. . . . .

. . . . .

. . . . . . . . .

. . . . .

. . . . .

. . . . . . . . .

. . . . .

. . . . .

. . . . . . . . .

. . . . .

. . . . .

. . . . . . . . .

. . . . .

. . . . .

. . . . . . . . .

. . . . .

. . . . .

. . . . . . . . .

. . . . .

. . . . .

. . . . . . . . .

. . . . .

. . . . .

. . . . . . . . .

. . . . .

. . . . .

. . . . . . . . .

. . . . .

. . . . .

1 1.1

Propositie logica Terminologie en notatie

In de propositielogica draait het er om dat enkel de logische structuur van zinnen overgehouden worden. Men werkt dus enkel met proposities of declaratieve zinnen die waar of vals kunnen zijn. We breken deze proposities op in basiszinnen die we met kleine letters p, q, r, . . . aanduiden en verbinden met ¬, ∨, ∧, ⇒. Om abigu¨ıteit te vermijden kunnen we haakjes gebruiken maar ook afspraken. ¬ heeft voorrang op ∧ en ∨ welke op hun beurt voorrang hebben op ⇒. De implicatie is rechts associatief, dit wil zeggen dat p ⇒ q ⇒ r moet ge¨ınterpreteerd worden als p ⇒ (q ⇒ r). Met natuurlijke deductie wordt het afleiden van conclusies uit premissen bedoelt. Meestal worden deze met griekse letters aangeduid. Stel dat we formules φ1 , φ2 , φ3 , . . . , φn hebben (premissen) en een formule ψ (conclusie), dan wordt deze deductie aangeduidt met: φ1 , φ2 , φ3 , . . . , φn ` ψ

1.2

Regels voor natuurlijke deductie

De eerste regel die we bekijken is en-introductie. Het stelt ons in staat φ ∧ ψ te concluderen als we φ and ψ al appart hebben geconcludeerd: φ ψ φ∧ψ

∧i

Hand in hand met en-introductie gaat en-eliminatie: φ∧ψ φ

φ∧ψ ψ

∧e1

∧e2

Deze regels stellen dat als men een bewijs van φ ∧ ψ heeft dat we daaruit een bewijs voor φ of ψ kunnen halen. Intutief zijn de regels van dubbele negatie: ¬¬φ φ

φ ¬¬φ

¬¬e

¬¬i

Er zijn ook regels om ⇒ te introduceren en te elimineren. We beginnen met implicatieeliminatie of modus ponens: φ

φ→ψ ψ

→e

Een andere manier van implicatie-eliminatie is de zogenaamde modus tollens: φ→ψ ¬ψ ¬φ

3

MT

De formule van implicatie-introductie kan niet zomaar gebruikt worden, er moet een veronderstelling worden gemaakt. Meer over deze veronderstellingen staat in het puntje ’Bewijstechnieken’ verder in deze cursus. We kunnen nu de implicatie-introductie als volgt noteren: φ .. . ψ →i

φ→ψ

De regels in verband met conjucties gedragen zich wat anders. De of-introducties zijn makkelijkst in te zien: φ φ∨ψ

ψ φ∨ψ

∨i1

∨i2

De of-eliminatie is minder makkelijk toe te passen:

φ∨ψ

φ .. .

ψ .. .

χ

χ ∨e

χ

Definitie 1. Contradicties zijn uitdrukkingen van de vorm φ∧¬φ of ¬φ∧φ met φ een formule. Een contradictie wordt met falsum ⊥ aangeduidt. Elke formule kan wordt afgeleidt uit een contradictie, dit wordt genoteerd als: ⊥ φ

⊥e

Het feit dat ⊥ zelf een contradictie voorstelt wordt aangeduidt met de bewijsregel: ¬φ

φ ⊥

¬e

Met behulp van ⊥ kunnen we ook een ¬ introduceren. Dit gaat als volgt: φ .. . ⊥ ¬φ

1.3

¬i

Afgeleide bewijsregels

Zoals eerder gezecht zijn niet alle regels hierboven absolute basis. Zo kan modus tollens φ→ψ ¬ψ ¬φ bewezen worden uit → e, ¬e en ¬i: 4

MT



φ→ψ

premise



¬ψ

premise



φ

assumption



ψ

→ e1, 3



⊥

¬e4, 2



¬φ

¬i3 − 5

Om modus tollens te gebruiken moeten we bovenstaand dus steeds in het achterhoofd houden. Het zelfde geld voor de dubbele negatie introductie:



φ

premise



¬φ

assumption



⊥

¬e1, 2



¬¬φ

¬i2 − 3

We kunnen nog veel gelijkaardige afgeleide regels definiëren maar eigenlijk kan het meeste met PBC en LEM bewezen worden. PBC of Proof By Contradiction wordt als volgt gedefiniëerd: ¬φ .. . ⊥ P BC

φ

Dit lijkt goed op ¬i buiten het feit dat de negatie op een andere plaats staat. PBC wordt als volgt afgeleidt:



¬φ →⊥

premise



¬φ

assumption



⊥

→ e1, 2



¬¬φ

¬i2 − 3



φ

¬¬e4

De meest handige wet is waarschijnlijk LEM of wet van het uitgesloten derde, deze wet stelt dat φ ∨ ¬φ waar is ongeacht de waarheidswaarde van φ. Ofwel is φ waar, ofwel is φ vals en dus ¬φ waar. Er is geen derde mogelijkheid, vandaar de naam. Volgend is de afleiding van LEM:

5

1.4



¬(φ ∨ ¬φ)

assumption



φ

assumption



φ ∨ ¬φ

∨i1 2



⊥

¬e3, 1



¬φ

¬i2 − 4



φ ∨ ¬φ

∨i2 5



⊥

¬e6, 1



¬¬(φ ∨ ¬φ)

¬i1 − 7



φ ∨ ¬φ

¬¬e8

Bewijstechnieken

In een bewijs kunnen we van zogenaamde veronderstellingen gebruik maken, deze zijn echter maar beperkt geldig en we bakenen de geldigheid af met een box. Met een bewijs kunnen we theorema’s gaan bewijzen, dit zijn alle formules φ die een geldig consequent ` ψ hebben. Definitie 2. Iets is bewijsbaar equivalent (we schrijven ’als en slechts dan als’) indien geldt dat φ ` ψ en ψ ` φ. Dit wordt genoteerd als a`.

1.5

Propositielogica

In de propositielogica worden de griekse letters in voorgaande secties vervangen door goed gevormde formules. Deze worden opgebouwd uit een onbegrensd aantal atomen p, q, r, . . ., of p1 , p2 , p3 , . . .. Definitie 3. Een bedeling (toekenning van waarheidswaarden) is een afbeelding v : atomen → {T,F} Zo kunnen we de uitbreiding v van v voor alle formules gaan vastleggen. Bijvoorbeeld: 1. v(p) = v(p) T als v(φ) = F 2. v(¬φ) = F als v(φ) = T T als v(φ) = v(ψ) = T 3. v(φ ∧ ψ) = F anders F als v(φ) = v(ψ) = F 4. v(φ ∨ ψ) = T anders F als v(φ) = T en v(ψ) = F 5. v(φ → ψ) = T anders

6

Waar in voorgaande secties door middel van calculus bewezen werd dat φ1 , φ2 , . . . , φn ` ψ geldig was kan er ook een nieuwe relatie φ1 , φ2 , . . . , φn |= ψ gedefinieërd worden. Deze kijkt naar de waarheidswaarden van de formules en trekt daaruit een conclusie. Op deze manier worden waarheidstabellen opgesteld. We mogen de verschillende begrippen dus niet verwarren: • Geldig gevolg: φ1 , . . . , φn |= ψ is een geldig gevolg als en slechts dan als ∀v : v(φ1 ) = · · · = v(φn ) = T ⇒ v(ψ) = T • Tautologie: een formule φ met |= φ • Semantisch equivalent: twee formules φ en ψ heten semantisch equivalent (φ ≡ ψ) als φ |= ψ en ψ |= φ. • Geldig: een formule φ is geldig als voor alle bedelingen v geldt dat v(φ) = T . • Vervulbaar: een formule φ is vervulbaar als er een bedeling v bestaat met v(φ) = T Geldigheid en vervulbaarheid zijn beslisbaar, dit wil zeggen dat een computer kan nagaan of een formule geldig of vervulbaar is. Nu we al deze regels geformuleerd en toegepast hebben om de geldigheid van stellingen te bewijzen moeten we ons misschien afvragen of deze afleidingen kloppen of correct zijn. We moeten hiervoor twee zaken bewijzen: 1. De propositionele logica is correct: als φ1 , . . . , φn ` ψ afleidbaar is dan φ1 , . . . , φn |= ψ. Met andere woorden dat alle bewijsbare uitspraken geldige uitspraken zijn. 2. De propositionele logica is volledig: als φ1 , . . . , φn |= ψ geldig is dan φ1 , . . . , φn ` ψ. Met andere woorde ndat alle geldige uitspraken bewijsbaar zijn. Vooraleer we de correctheidsstelling kunnen bewijzen moeten we eerst iets meer vertellen over uitgebreide sequenten. Bij een uitgebreid sequent schrijft men de aannames die men in het bewijs doet bij de premissen. We bewijzen eerst de correctheidsstelling door middel van inductie op de lengte van een afleiding: • Te bewijzen: Stel φ1 , φ2 , . . . , φn en ψ propositionele logische formules. We moeten bewijzen dat als φ1 , φ2 , . . . , φn ` ψ geldig is dat φ1 , φ2 , . . . , φn |= ψ steek houdt. Met steek houden bedoelen we dat dat ψ enkel waar mag zijn als φ1 , φ2 , . . . , φn allemaal waar zijn. • Bewijsmethode: We zullen inductie toepassen op de lengte van het bewijs φ1 , φ2 , . . . , φn ` ψ waarbij met de lengte het aantal lijnen in dit bewijs wordt bedoelt. We gaan sterke inductie uitvoeren op deze lengte. • Bewijs met sterke inductie: – Inductiehypothese: We nemen M (k) aan: voor alle sequenten φ1 , φ2 , . . . , φn ` ψ(n ≥ 0) hebben we een bewijs van lengte k waardoor φ1 , φ2 , . . . , φn |= ψ steek houdt. 7

– Basisstap: als het bewijs lengte 1 heeft (k = 1) dan moet het van de vorm φ



premise

zijn. We zitten dus in het geval waarbij n = 1 en dus φ1 en ψ gelijk zijn aan φ. We verkrijgen zo het sequent φ ` φ waardoor φ |= φ duidelijk steek houdt. – Sterke inductiestap: we veronderstellen dat het bewijs van het sequent φ1 , φ2 , . . . , φn ` ψ lengte k heeft en dat de te bewijzen stelling waar is voor alle aantallen kleiner dan k. Het bewijs heeft dan volgende structuur: φ1 φ1 .. .

premise premise

n

φ1 .. .

premise

k

ψ

bewijsregel

1 2

Er zijn op dit punt twee zaken onbekend: 1. Welke constructies zijn er gebeurt tussen de puntjes? Het is niet belangrijk om dit uit te zoeken, de inductiehypothese garandeert ons namelijk dat deze stappen correct zijn. 2. Wat is de laatst toegepaste bewijsregel? Hier zegt inductie nog niets over en het is onmogelijk om te weten welke regel werd toegepast. We zijn dus verplicht om de correctheid voor alle mogelijke regels te controleren. We controleren enkele van deze regels om de structuur duidelijk te maken: ∗ ∧i: we weten nu dat ψ van de vorm ψ1 ∧ ψ2 is en de bewijsregel op lijn k naar de twee lijnen hogerop waar ψ1 en ψ2 staan, stel k1 en k2 , refereert. Aangezien k1 en k2 kleiner zijn dan k weten we dat er bewijzen van de sequenten φ1 , φ2 , . . . , φn ` ψ1 en φ1 , φ2 , . . . , φn ` ψ2 bestaan met lengte kleiner dan k. De inductiehypothese garandeert ons dan dat φ1 , φ2 , . . . , φn |= ψ1 en φ1 , φ2 , . . . , φn |= ψ2 steek houden. Daaruit volgt dat φ1 , φ2 , . . . , φn |= ψ1 ∧ ψ2 ook steek houdt. ∗ ∨e: indien φ op deze manier bewezen is dan moet er een voorgaande aaname, premise zijn van de vorm η1 ∨ η2 op een lijn k 0 met k 0 < k. De bewijsregel op lijn k zal dus naar lijn k 0 refereren via ∨e. De inductiehypothese zegt ons dan dat er een korter bewijs van het sequent φ1 , φ2 , . . . , φn ` η1 ∨ η2 bestaat. Daar ∨e met gevallenonderzoek werkt zijn er daarvoor 2 boxen gebruikt, als we met de aannames in die boxen uitgebreide sequenten maken dan bekomen we dat er bewijzen zijn voor φ1 , φ2 , . . . , φn , η1 ` ψ en φ1 , φ2 , . . . , φn , η2 ` ψ. De inductiehypothese garandeert dan dat φ1 , φ2 , . . . , φn , η1 |= ψ ne φ1 , φ2 , . . . , φn , η2 |= ψ steek houden waardoor φ1 , φ2 , . . . , φn |= ψ ook steek houdt. Op deze manier dienen dus alle bewijsregels gecontroleerd te worden. Het gaat er dus steeds om dat we moeten bewijzen dat de deductieregels zich semantisch gezien het zelfde gedragen als de waarheidstabellen. 8

Het feit dat deze correctheidsstelling geldt maakt het mogelijk om voor een sequent φ1 , φ2 , . . . , φn ` ψ aan te tonen dat het niet afleidbaar/bewijsbaar is. Het volstaat een bedeling te vinden waarvoor φi waar is terwijl ψ vals is. Daaruit volgt dan dat φ1 , φ2 , . . . , φn |= ψ geen steek houdt. Uit de correctheidsstelling volgt dan dat φ1 , φ2 , . . . , φn ` ψ niet geldig kan zijn en er dus geen bewijs voor is. We gaan nu over tot het bewijzen van de volledigheid van de propositie logica en willen dus bewijzen dat als φ1 , φ2 , . . . , φn |= ψ steek houdt, er dan een bewijs bestaat voor het sequent φ1 , φ2 , . . . , φn ` ψ. Met andere woorden alle geldige uitspraken zijn bewijsbaar. We nemen in het bewijs dus steeds aan dat φ1 , φ2 , . . . , φn |= ψ steek houdt en bewijzen in 3 stappen: 1. We tonen aan dat |= φ1 → (φ1 → (φ3 → (. . . (φn → ψ) . . .))) steek houdt. 2. We tonen aan dat ` φ1 → (φ1 → (φ3 → (. . . (φn → ψ) . . .))) geldig is. 3. We tonen aan dat φ1 , φ2 , . . . , φn ` ψ geldig is. We bewijzen dus: 1. We weten dus dat φ1 , φ2 , . . . , φn |= ψ steek houdt en we gaan na dat |= φ1 → (φ1 → (φ3 → (. . . (φn → ψ) . . .))) een tautologie is. Daar deze formule een geneste implicatie is, is er maar één mogelijkheid om vals te bekomen. Alle φ1 , φ2 , . . . , φn moeten waar zijn en ψ moet vals zijn. Dit spreekt het feit dat φ1 , φ2 , . . . , φn |= ψ steek houdt echter tegen, dus houdt |= φ1 → (φ1 → (φ3 → (. . . (φn → ψ) . . .))) steek. 2. Theorema 1. Als |= η steek houdt, dan is ` η geldig. Met andere woorden, als η een tautologie is, dan is η een theorema. Deze tweede stap is de moeilijkste en langste stap. Stel dat |= η steek houdt en dat gegeven is dat η n verschillende propositionele atomen p1 , p2 , . . . , pn bevat. We weten dan dat η naar > evalueert voor alle 2n lijnen in de waarheidstabel. Om het bewijs op te bouwen gaan we nu elke lijn in de waarheidstabel van η interpreteren als een sequent. Voor elk van deze 2n sequenten stellen we een bewijs op waarna we deze bewijzen terug samenstellen tot een bewijs voor η. Propositie 1. Stel φ een formule met als enige propositionele atomen p1 , p2 , . . . , pn . Stel l gelijk welk lijnnummer in de waarheidstabel van φ. Stel nu voor alle i in 1 ≤ i ≤ n pî als pi voor indien pi op lijn l > is, stel anders pî als ¬pi voor. Met andere woorden: pî =

φ als v(φ) = T ¬φ als v(φ) = F

We bekomen nu • pˆ1 , pˆ2 , . . . , pˆn ` φ is bewijsbaar als φ op lijn l T is. • pˆ1 , pˆ2 , . . . , pˆn ` ¬φ is bewijsbaar als φ op lijn l F is. We bewijzen deze propositie nu met inductie op (de lengte) van φ:

9

• Basisstap: φ bestaat nu uit één propositioneel atoom p en we moeten dus p ` p en ¬p ` ¬p aantonen wat duidelijk geldig is. • Inductiestap: ook hier moeten we weer voor elke formule onderzoeken of we tot een sluitend bewijs komen. We overlopen er een paar: – Als φ van de vorm ¬φ1 is moeten we twee gevallen onderscheiden. Stel eerst dat φ T is dan is φ1 F. We merken op dat φ1 dezelfde atomaire structuur heeft als φ. We kunnen nu de inductiehypothese toepassen op φ1 om te concluderen dat pˆ1 , pˆ2 , . . . , pˆn ` ¬φ1 . Maar aangezien ¬φ1 structureel gelijk is aan φ zijn we klaar. – Stel φ van de vorm φ1 → φ2 . Als φ F is, dan weten we dat φ1 T is en φ2 F is. Uit de inductiehypothese volgt dan dat qˆ1 , . . . , qˆl ` φ1 en rˆ1 , . . . , rˆk ` φ2 waaruit pˆ1 , . . . , pˆn ` φ1 ∧ ¬φ2 volgt. We moeten aantonen dat pˆ1 , . . . , pˆn ` ¬(φ1 → φ2 ) wat gebruik makend van pˆ1 , . . . , pˆn ` φ1 ∧ ¬φ2 leidt tot het aantonen van φ1 ∧ ¬φ2 ` ¬(φ1 → φ2 ). Dit kan met een simpele waarheidstabel. Als φ T is hebben we drie gevallen: (a) Als φ1 F is en φ2 F is krijgen we door middel van de inductiehypothese dat qˆ1 , . . . , qˆl ` ¬φ1 en rˆ1 , . . . , rˆk ` ¬φ2 waaruit pˆ1 , . . . , pˆn ` ¬φ1 ∧ ¬φ2 volgt. Weer kunnen we nu met een simpele waarheidstabel ¬φ1 ∧ ¬φ2 ` φ1 → φ2 aantonen. (b) Als φ1 F is en φ2 T is krijgen we door middel van de inductiehypothese dat pˆ1 , . . . , pˆn ` ¬φ1 ∧ φ2 en we moeten dus op gelijkaardige manier bewijzen dat ¬φ1 ∧ φ2 ` ¬φ1 → φ2 . (c) Als φ1 T is en φ2 T is krijgen we door middel van de inductiehypothese dat pˆ1 , . . . , pˆn ` φ1 ∧ φ2 en we moeten dus op gelijkaardige manier bewijzen dat φ1 ∧ φ2 ` φ1 → φ2 . – Als φ van de vorm φ1 ∧ φ2 is dan moeten we weer 4 gevallen beschouwen: (a) Als φ1 T is en φ2 T is krijgen we door middel van de inductiehypothese dat qˆ1 , . . . , qˆl ` φ1 en rˆ1 , . . . , rˆk ` φ2 waaruit pˆ1 , . . . , pˆn ` φ1 ∧ φ2 volgt. (b) Als φ1 F is en φ2 T is krijgen we door middel van de inductiehypothese en de ∧i regel dat pˆ1 , . . . , pˆn ` ¬φ1 ∧ φ2 . We moeten dus enkel bewijzen dat ¬φ1 ∧ φ2 ` ¬(φ1 ∧ φ2 ). (c) Als φ1 F is en φ2 F is krijgen we door middel van de inductiehypothese en de ∧i regel dat pˆ1 , . . . , pˆn ` ¬φ1 ∧ ¬φ2 . We moeten dus enkel bewijzen dat ¬φ1 ∧ ¬φ2 ` ¬(φ1 ∧ φ2 ). (d) Als φ1 T is en φ2 F is krijgen we door middel van de inductiehypothese dat ∧i regel dat pˆ1 , . . . , pˆn ` φ1 ∧ ¬φ2 . We moeten dus enkel bewijzen dat φ1 ∧ ¬φ2 ` ¬(φ1 ∧ φ2 ). – Als φ van de vorm φ1 ∨ φ2 is dan moeten we weer 4 gevallen beschouwen: (a) Als φ1 F is en φ2 F is krijgen we door middel van de inductiehypothese en de ∧i regel dat pˆ1 , . . . , pˆn ` ¬φ1 ∧ ¬φ2 . We moeten dus enkel bewijzen dat ¬φ1 ∧ ¬φ2 ` ¬(φ1 ∨ φ2 ). (b) Als φ1 T is en φ2 T is krijgen we door middel van de inductiehypothese dat pˆ1 , . . . , pˆn ` φ1 ∧ φ2 . We moeten dus enkel bewijzen dat φ1 ∧ φ2 ` φ1 ∨ φ2 .

10

(c) Als φ1 F is en φ2 T is krijgen we door middel van de inductiehypothese dat pˆ1 , . . . , pˆn ` ¬φ1 ∧φ2 . We moeten dus enkel bewijzen dat ¬φ1 ∧φ2 ` φ1 ∨φ2 . (d) Als φ1 T is en φ2 F is krijgen we door middel van de inductiehypothese dat pˆ1 , . . . , pˆn ` φ1 ∧¬φ2 . We moeten dus enkel bewijzen dat φ1 ∧¬φ2 ` φ1 ∨φ2 . We passen deze techniek nu toe op de formule |= φ1 → (φ1 → (φ3 → (. . . (φn → ψ) . . .))). Aangezien dat een tautologie is evalueert het als T in alle 2n lijnen in de waarheidstabel. We moeten dus 2n aantal bewijzen van de vorm pˆ1 , pˆ2 , . . . , pˆn ` η opstellen, één voor elk van de gevallen dat pî pi of ¬pi is. Daarna moeten we al deze bewijzen samenstellen tot een enkelvoudig bewijs voor η zonder premissen. We demonstreren deze techniek met de tautologie p ∧ q → p die twee propositionele atomen p en q heeft. Door bovenstaande propositie hebben we de garantie dat er een bewijs is voor elk van de volgende vier sequenten: (a) p, q ` p ∧ q → p (b) ¬p, q ` p ∧ q → p (c) p, ¬q ` p ∧ q → p (d) ¬p, ¬q ` p ∧ q → p We willen p ∧ q → p bewijzen door de 4 bewijzen samen te nemen en we moeten de premissen dus op één of andere manier zien te verliezen. Hiervoor gebruiken we de wet van het uitgesloten derde of LEM. Deze stelt dat r ∨ ¬r voor elke r geldt. We gebruiken nu LEM voor alle propositionele atomen (hier p en q) en nemen ze dan appart aan door middel van ∨e. Op deze manier kunnen we alle vier de bovenstaande sequenten appart bewijzen:



p ∨ ¬p



p

aanname

¬p

aanname



q ∨ ¬q

LEM

q ∨ ¬q

LEM



q .... ..

aanname

q .... ..



LEM

aanname ¬q .... ..

aanname ¬q .... ..

aanname

 

p∧q →p



p∧q →p



p∧q →p

p∧q →p

p∧q →p ∨e

p∧q →p

p∧q →p ∨e ∨e

3. Als laatste moeten we een bewijs vinden voor φ1 , φ2 , . . . , φn ` ψ. We nemen hiervoor het bewijs uit stap 2 (|= φ1 → (φ1 → (φ3 → (. . . (φn → ψ) . . .)))) en introduceren φ1 , φ2 , . . . , φn als premissen. We passen dan → e n keer toe op elk van deze premissen. Op deze manier komen we aan de conclusie ψ en we hebben het gestelde dus bewezen. 11

1.6

Conjunctieve normaalvorm

Definitie 4. Een literaal is een atoom p of een ontkennend atoom ¬p. Twee literalen l1 en l2 heten complementair als l1 = ¬l2 of ¬l1 = l2 . Definitie 5. Twee formules φ en ψ zijn semantisch equivalent als φ |= ψ en ψ |= φ steek houden. Indien twee formules φ en ψ sementisch equivalent zijn wordt dit aangeduidt door φ ≡ ψ. Definitie 6. Een conjunctieve normaalvorm of CNV is een conjunctie van disjuncties van literalen. Meer abstract wordt dit genoteerd als: L D C

::= ::= ::=

p | ¬p L|L∨D D|D∧C

Conjunctieve normaalvormen worden gebruikt omdat er een efficiënt algoritme bestaat om de geldigheid ervan te testen. Een conjunctieve normaalvorm φ is geldig als en slechts dan als iedere conjunctie van φ een koppel van complementaire literalen bevat. Dit is een veralgemening van volgend lemma: Lemma 1. Een disjunctie van literalen l1 ∨ l2 , ∨ · · · ∨ lm is geldig als er een i, j bestaan met 1 ≤ i, j ≤ m zodat li = ¬lj . We bewijzen dit lemma. Als li gelijk is aan ¬lj dan zal l1 ∨ l2 ∨ · · · ∨ lm T zijn voor elke bedeling. Zo kan p ∨ q ∨ r ∨ ¬q bijvoorbeeld nooit F zijn. Stel nu dat geen enkele literaal lk een complementair literaal lr bevat in l1 ∨ l2 ∨ · · · ∨ lm . Dan kunnen we voor elke k, 1 ≤ k ≤ n aan lk F toewijzen als lk een atoom is of T als lk de negatie van een atoom is waardoor we false uitkomen. Zo kan de disjunctie ¬q ∨ p ∨ r vals gemaakt worden door p en r F te maken en q T te maken. Het is dus belangrijk dat het complementaire literaal in de zelfde disjunctie gevonden wordt. Vooraleer we verder gaan dienen we eerst een nieuw begrip in te voeren, vervulbaarheid. Definitie 7. Een formule φ is vervulbaar indien er een bedeling v(φ) bestaat die T uitkomt. Een formule φ is vervulbaar als ¬φ niet geldig is. Er zijn verschillende algoritmes om conjunctieve normaalvormen op te stellen. We geven er twee: 1. Door middel van een waarheidstabel. Het aantal disjuncties in de conjunctieve normaalvorm wordt nu gegeven door het aantal keer dat de formule φ F uitkomt. Elke disjunctie bevat nu de literaal tegengesteld met de bedeling in de waarheidstabel, dus ¬p voor T en p voor F. Op deze manier kan men meteen de CNV aflezen. We geven een voorbeeld voor volgende waarheidstabel:

12

p T T T T F F F F

q T T F F T T F F

r T F T F T F T F

φ T F T T F F F T

Er zijn 4 rijen waar de formule F uitkomt en de CNV is dus vande vorm ψ1 ∧ψ2 ∧ψ3 ∧ψ4 . We kunnen nu de ψi aflezen uit de tabel: • ψ1 = ¬p ∨ ¬q ∨ r • ψ2 = p ∨ ¬q ∨ ¬r • ψ3 = p ∨ ¬q ∨ r • ψ4 = p ∨ q ∨ ¬r Dit maakt dat de CNV gegeven wordt door: (¬p ∨ ¬q ∨ r) ∧ (p ∨ ¬q ∨ ¬r) ∧ (p ∨ ¬q ∨ r) ∧ (p ∨ q ∨ ¬r) 2. Een tweede manier werkt rechtstreeks in op de formule φ en bestaat uit het uitvoeren van 3 stappen: (a) Verwijder alle implicaties met φ → ψ ≡ ¬φ ∨ ψ. (b) Schuif ontkenningen door naar de atomen met De Morgan ¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ of ¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ en verwijder dubbele negaties ¬¬φ ≡ φ. (c) Verdeel disjuncties over conjuncties met φ∨(ψ∧χ) ≡ (φ∨ψ)∧(ψ∨χ) of (φ∧ψ)∨χ ≡ (ψ ∨ χ) ∧ (ψ ∨ χ) Het is belangrijk te onthouden dat conjunctieve normaalvormen niet uniek bepaald zijn. Voor alle formules φ bestaat er een CNV ψ zo dat φ ≡ ψ en deze kan bepaald worden door middel van bovenstaande deterministische procedure. We zullen deze nu iets formeler schrijven door verschillende procedures te schrijven. We beginnen met het verwijderen van implicaties: function IMPL FREE(φ) : switch φ : case φ literaal return φ case φ is ¬φ1 return ¬IMPL FREE(φ1 ) case φ is φ1 ∧ φ2 return IMPL FREE(φ1 ) ∧ IMPL FREE(φ2 ) case φ is φ1 ∨ φ2 return IMPL FREE(φ1 ) ∨ IMPL FREE(φ2 )

13

case φ is φ1 → φ2 return ¬IMPL FREE(φ1 ) ∨ IMPL FREE(φ2 ) end function Het is noodzakelijk om ontkenningen door te schuiven naar de literalen. Eens dit gebeurt is bekomen we een zogenaamde negatie normaal vorm of NNV. Dit gaat als volgt: function NNF(φ) : switch φ : case φ literaal return φ case φ is ¬¬φ1 return NNF(φ1 ) case φ is φ1 ∧ φ2 return NNF(φ1 ) ∧ NNF(φ2 ) case φ is φ1 ∨ φ2 return NNF(φ1 ) ∨ NNF(φ2 ) case φ is ¬(φ1 ∧ φ2 ) return NNF(¬φ1 ) ∨ NNF(¬φ2 ) case φ is ¬(φ1 ∨ φ2 ) return NNF(¬φ1 ) ∧ NNF(¬φ2 ) end function Als laatste hebben we nog een functie/procedure nodig om de disjuncties te verdelen: function DISTR(η1 , η2 ) : switch η1 , η2 : case η1 is η11 ∧ η12 return DISTR(η11 , η2 ) ∧ DISTR(η12 , η2 ) case η2 is η21 ∧ η22 return DISTR(η1 , η21 ) ∧ DISTR(η1 , η22 ) case default return η1 ∨ η2 end function Nu kunnen we de CNF functie, die eveneens disjuncties verdeelt, definiëren: function CNF(φ) : switch φ : case φ literaal return φ case φ is φ1 ∧ φ2 return CNF(φ1 ) ∧ CNF(φ2 ) case φ is φ1 ∨ φ2 return DISTR(CNF(φ1 ), CNF(φ2 )) end function 14

Nu we deze functies gedefiniëerd hebben gelden volgende uitspraken: • CNF(NNF(IMPL FREE(φ))) is een CNV van φ. • CNF(NNF(IMPL FREE(φ))) ≡ φ. • Het afwerken van CNF(NNF(IMPL FREE(φ))) eindigt (het bewijs wordt in het vak herschrijfsystemen gegeven).

1.7

Horn clausules

Definitie 8. Een Hornclausule is een formule van de vorm p1 ∧ · · · ∧ pn → q met n ≤ 1 en waarbij p1 , . . . , pn atomen, ⊥ of > zijn. Definitie 9. Een Hornformule is een conjunctie van Hornclausules. Het is dus een instantie van H in: P A C H

::= ::= ::= ::=

⊥|>|p P|P∧A A → P (C is dus een Hornclausule) C|C∧H

Horn formules zijn interessant omdat er een efficiënt algoritme bestaat om de vervulbaarheid ervan na te gaan: function HORN(φ) : Maak een lijst van alle atomen inclusief ⊥ en > die in φ optreden. Markeer > als het in de lijst optreedt. while ∃ Hornclausule P1 ∧ · · · Pn → Q in φ zodat alle P1 ∧ · · · Pn gemarkeerd zijn en als Q nog niet gemarkeerd is do markeer Q. end while if ⊥ gemarkeerd is then return niet vervulbaar else T als P gemarkeerd is return vervulbaar met bedeling v(P ) = F als P niet gemarkeerd is end if end function Theorema 2. Het HORN algoritme is correct om de vervulbaarheid van een Horn formule φ te beslissen. Daarbij heeft de while-loop niet meer dan n + 1 iteraties nodig als n het aantal atomen in φ is, met andere woorden HORN stopt altijd bij een correcte input. We bewijzen dit in drie delen: 1. Bewijs dat het algorimte eindigt: als we in de body van de while-loop gaan heeft dit het effect dat een niet-gemarkeerde P die niet > is gemarkeerd wordt. Aangezien het markeren toegepast wordt op alle voorkomens van P in φ kan de while-loop ten hoogste één iteratie meer doen dan het aantal atomen in φ.

15

2. Bewijs dat de while-lus correct is: om dit te bewijzen bespreken we eerst de rol van de markeringen. Een markering van P duidt op het feit dat P T moet zijn opdat de formule φ vervulbaar zou kunnen zijn. We gebruiken nu inductie om aan te tonen dat Alle gemarkeerde P zijn T voor alle bedelingen waarin φ T is. steek houdt na gelijk welk aantal iteraties van de while-loop. • Basisgeval: als er nul iteraties geweest zijn zijn enkel alle voorkomens van > gemarkeerd. Aangezien > T moet zijn in alle bedelingen volgt het gestelde. • Inductiehypothese: we nemen aan dat de uitspraak klopt na k iteraties van de while-loop. • Inductiestap: we bewijzen nu dat de uitspraak geldt na k + 1 iteraties. Als we de (k + 1)de iteratie starten is de conditie in de while-lus zeker waar. Er bestaat dus een conjunctie P1 ∧ P2 ∧ · · · ∧ Pki → P 0 van φ zodat alle Pj gemarkeerd zijn. Stel nu v gelijk welke bedeling waarvoor φ T is. Door de inductiehypothese weten we dan dat alle Pj en dus P1 ∧ P2 ∧ · · · ∧ Pki ook T zijn in v waaruit we afleiden dat P 0 T moet zijn in v. 3. Bewijs dat het if-statement altijd correct is: • als ⊥ gemarkeerd is moet er een conjuctie van de vorm P1 ∧ P2 ∧ · · · ∧ Pki →⊥ zijn in φ waarvan alle Pi ook gemarkeerd zijn. Die conjuctie is dan gelijk aan T → F = F vanaf dat φ T is. Dit is onmogelijk dus is het antwoord ’niet vervulbaar’ correct. • als ⊥ niet gemarkeerd is weizen we T toe aan alle gemarkeerde atomen en F aan alle niet gemarkeerde atomen waarna we met PBC aantonen dat φ T moet zijn met die bedeling. Moest φ niet T zijn met die bedeling moet één van zijn conjucties P1 ∧ P2 ∧ · · · Pki → P 0 F zijn. Dit kan enkel indien alle Pj T zijn en P 0 F is, dit zou betekenen dat alle Pj gemarkeerd zijn en dus dat P1 ∧ P2 ∧ · · · Pki → P 0 behandeld is geweest in één van de iteraties van de while-loop waardoor P 0 gemarkeerd zou moeten zijn. Aangezien ⊥ niet gemarkeerd is moet P 0 > of een atoom q zijn wat leidt tot het waar zijn van de conjuctie, een contradictie. We merken als laatste op dat als een hornformule φ vervulbaar is het algoritme de kleinste bedeling v geeft die φ waar maakt.

1.8

SAT solvers

Een SAT-solver is een andere manier om de vervulbaarheid van een formule in gelijk welke vorm te controleren. Het is een NP-volledig probleem. Er zijn verschillende soorten SATsolvers waarvan we enkel de eerste twee zullen behandelen: 1. Lineaire oplosser: deze is vergelijkbaar met het markeringsalgoritme voor Horn. 2. Kubische oplosser 3. Volledige oplosser

16

De eerste twee oplossers zijn correct maar onvolledig. We bespreken eerst de lineaire SAT solver, vooraleer deze toegepast wordt moeten we de formule φ recursief transformeren om ∨ en → te verwijderen:  φ als φ een atoom is     ¬T (φ ) als φ = ¬φ1  1 T (φ1 ) ∧ T (φ2 ) als φ = φ1 ∧ φ2 T (φ) =   ¬(¬T (φ ) ∧ ¬T (φ )) als φ = φ1 ∨ φ2  1 2   ¬(T (φ1 ) ∧ ¬T (φ2 )) als φ = φ1 → φ2 Daarna moet de parseboom van de formule worden opgesteld waarna dan alle toppen door middel van de propagatieregels moeten worden gemarkeerd. De propagatieregels zijn de volgende: 1:T ¬

1:F ¬

2:F

2:T ¬

2:T

◦

1:F

◦

◦ 2:T ∧

2:T ◦

1:T ◦

2:F ∧ 1:F ◦

1:T ◦ 2:F ∧

◦

1:F ◦

◦

1:F ∧ 1:T ◦

1:T

◦

1:T ∧ 2:T ◦

2:F ¬

1:F ∧ 2:F ◦

2:F ◦

1:T ◦

Figuur 1: Propagatieregels voor SAT

Het kan zijn dat dit algoritme geen antwoord levert, dit merkt men meteen in de parseboom. Zo kan men niet verder als men een ¬(a ∧ b) tegenkomt. Er zijn dan verschillende mogelijkheden en dus zit de lineaire SAT-oplosser vast. Een kubische SAT-solver kan dit probleem wel oplossen door alle gevallen uit te proberen.

17

1.9

Tseitintransformatie

Definitie 10. Twee formules φ en ψ zijn vervulbaarheidsequivalent als φ vervulbaar betekent dat ψ vervulbaar is. De meeste SAT-oplossers gebruiken conjunctieve normaalvormen als input. De transformatie van een formule naar een CNV is echter een dure operatie, er bestaat echter wel een algoritme om in lineaire tijd een formule tot een vervulbaarheidsequivalente CNV om te zetten. Dit is de zogenaamde Tseitintransformatie: T T (φ) = Iφ ∧ T T 0 (φ) met  >      T T 0 (ψ) ∧ (Iφ ↔ ¬Iψ ) T T 0 (ψ1 ) ∧ T T 0 (ψ2 ) ∧ (Iφ ↔ Iψ 1 ∧ Iψ 2 ) T T 0 (φ) =   T T 0 (ψ1 ) ∧ T T 0 (ψ2 ) ∧ (Iφ ↔ Iψ 1 ∨ Iψ 2 )    T T 0 (ψ1 ) ∧ T T 0 (ψ2 ) ∧ (Iφ ↔ Iψ 1 → Iψ 2 )

als als als als als

φ een atoom is φ = ¬ψ φ = ψ1 ∧ ψ2 φ = ψ1 ∨ ψ2 φ = ψ1 → ψ2

en Iψ =

ψ als ψ atoom nieuw atoom anders

De formules φ en T T (φ) zijn nu vervulbaarheidsequivalent. Met behulp van enkele equivalenties kunnen we een Tseitinnormaalvorm herschrijven als een conjunctieve normaalvorm: φ ↔ ¬ψ φ↔ψ∧χ φ↔ψ∨χ φ ↔ (ψ → χ)

≡ ≡ ≡ ≡

(ψ ∨ φ) ∧ (¬ψ ∨ ¬φ) (¬ψ ∨ ¬χ ∨ φ) ∧ (ψ ∨ ¬φ) ∧ (χ ∨ ¬φ) (ψ ∨ χ ∨ ¬φ) ∧ (¬ψ ∨ φ) ∧ (¬χ ∨ φ) (¬ψ ∨ χ ∨ ¬φ) ∧ (ψ ∨ φ) ∧ (¬χ ∨ φ)

Lemma 2. De formule T T 0 (φ) → (Iφ ↔ φ) is geldig. We bewijzen dit met behulp van inductie op de lengte van φ: • Basisstap: als φ een atoom is, dan is de bewering duidelijk. • Inductiestap: Stel dat φ van de vorm ψ → χ is. Zij v een bedeling met v(T T 0 (φ)) = T . Dan geldt v(T T 0 (ψ)) = T en v(T T 0 (χ)) = T en v(Iφ ↔ (Iψ → Iχ )) = T . Door middel van de inductiehypothese halen we hieruit dat v(Iψ ) = v(ψ) en v(Iχ ) = v(χ) en uiteindelijk v(Iφ ) = v(Iψ → Iχ ) = v(ψ → χ) = v(φ). Stel v een bedeling met v(T T (φ)) = T . Dan geldt v(Iφ )) = T en v(T T 0 (φ)) = T . Lemma 2 geeft dan dat v(φ) = T . Omgekeerd, zij v een bedeling met v(φ) = T en w een bedeling met w(Iψ ) = T als en slechts dan als v(ψ) = T voor alle deelformules van φ. In het bijzonder geldt dan dat w(p) = v(p) voor alle atomen die in φ optreden en dus w(φ) = v(φ). Met inductie op de lengte van ψ tonen we aan dat w(T T 0 (ψ)) = T geldt voor alle deelformules ψ van φ: – Basisstap: de bewering geldt als ψ een atoom is.

18

– Inductiestap: Stel nu dat ψ = ψ1 → ψ2 . De inductiehypothese geeft dan dat w(T T 0 (ψ1 )) = T en w(T T 0 (ψ2 )) = T . We hebben w(Iψ ) = v(ψ) = v(ψ1 → ψ2 ) = w(Iψ 1 → Iψ 2 ) omdat v(ψi ) = w(Iψ i ) voor i = 1, 2. Dus geldt w(Iψ ↔ (Iψ 1 → Iψ 2 )) = T en bijgevolg w(T T 0 (ψ)) = T . Verder hebben we dat w(Iφ ) = v(φ) = T en dus in totaal w(T T (φ)) = T .

2

Predikaatlogica

2.1

Begrippen en definities

De predikaatlogica of eerste orde logica is ontstaan uit de nood voor meer subtiele uitdrukkingen. De predikaatlogica bevat volgende concepten: • Predikaatsymbolen: P, Q, R, A, B duiden een predikaat zoals P (x) aan waarbij P meer betekenis geeft aan de variabele x. Het zijn dus relaties over het domein. Stel F (x, y) staat voor x is vader van y, dan is F een predikaatsymbool. • Variabelen: x, y, z worden in een predicaat ingevuld en zijn ’plaatshouders’ voor objecten. Het zijn dus nog niet gespecifieerde elementen van het domein. • Functiesymbolen: f, g, h, a, b duiden functies over het domein aan. Stel m staat voor ’ik’ dan is dat een functiesymbool van ariteit 0, dit wordt ook een constante genoemd. Stel m(y) als ’de moeder van y’ dan is dit een functiesymbool van ariteit 1. • Kwantoren: ∃ en ∀ zijn de twee kwantoren die respectievelijk staan voor ’er bestaat’ en ’voor alle’. • Connectieven: deze zijn gelijk aan die van de propositielogica: ¬, ∧, ∨, →. De functie- en predikaatsymbolen hebben een vast aantal argumenten. Dit aantal argumenten wordt de ariteit of plaatsigheid van het predikaat genoemd. Op deze manier spreekt men soms van unaire of binaire predikaten. Zo heeft het predikaatsymbool ’=’ een ariteit van 2 en is het dus een binair predikaat. Een functie geeft dus opnieuw een object terug terwijl een predikaat een waarheidswaarde teruggeeft. In het algemeen zijn termen uitdrukkingen die objecten aanduiden en formules uidrukkingen die een waarheidswaarde uitdrukken. De notationele conventies gelden nog steeds: • ¬, ∃y en ∀y binden het sterkst, • daarna komen ∨ en ∧, • dan komt → welke rechts-associatief is. Het is belangrijk onderscheidt te maken tussen vrije en gebonden variabelen. We tonen eerst het verschil aan door een parseboom te maken van de formule (∀x(P (x) ∧ Q(x))) → (¬P (x) ∨ Q(y)). Deze parseboom bevat twee extra’s tegenover propositionele parsebomen: • De kwantoren ∀x en ∃y hebben maar 1 kind. • Predikaten zoals P (t1 , t2 , . . . , tn ) hebben het symbool P als top met n kinderen, namelijk de parsebomen van de termen t1 , t2 , . . . , tn . 19

We bekomen voor (∀x(P (x) ∧ Q(x))) → (¬P (x) ∨ Q(y)) dus de parseboom: →

∨

∀x

¬

∧

Q vrij

P gebonden x

Q

P

gebonden x

y

vrij x

Variabelen interageren dus op twee manieren met kwantoren: • Gebonden variabele: een variabele is gebonden in een (deel)-formule ∀xφ of ∃xφ als x in φ optreedt. • Vrije variabele: een variabele x in een formule φ heet vrij als dit optreden van x niet in een deelformule van φ gebonden optreedt. Met andere woorden is x in φ vrij als het een blad is in de parseboom van φ zodat er geen opwaards pad bestaat van dat blad tot een top met een kwantor in. Het bereik van ∀x/∃x in een formule ∀xφ/∃x is φ zonder in φ optredende subformules ∀xψ of ∃xψ. De verzameling van vrije variabelen van een formule φ is dus de verzameling van de in φ optredende variabelen die niet in het bereik van een kwantor in φ zitten. Variabelen zijn niet meer dan ’plaatshouders’ en moeten dus substitueerbaar zijn. Het is heel belangrijk om enkel de vrije voorkomens van een variabele te substitueren. Indien ook de gebonden variabelen gesubstitueerd worden is de semantiek van de formule niet langer correct. Definitie 11. Gegeven een variabele x, een term t een een formule φ. Dan is φ[t/x] de formule φ waarin alle vrije voorkomens van de variabele x vervangen zijn door t. Definitie 12. Stel een term t, een variabele x en een formule φ. We zeggen dat t vrij is voor x in φ als de variabelen van t niet gebonden worden in φ[t/x]. Of dus als geen er geen vrij x blad voorkomt in φ dat binnen het bereik van een kwantor ∀y of ∃y valt voor gelijk welke variabele y in t. Indien een substitutie gedaan wordt van een variabele x met een term t die niet vrij is voor x kan dit ongewenste effecten hebben. Zo kan een extra variabele y van t plots gebonden worden. We spreken daarom af enkel φ[t/x] tot te passen als t vrij voor x is in φ, in de rest van de cursus wordt dit bij een substitutie impliciet verondersteld.

20

2.2

Regels voor natuurlijke deductie

Alle bewijsregels van de propositielogica gelden ook voor de predikaatlogica, daarbovenop zijn er enkele extra regels • Introductie van identiteiten. =i

t=t Dit is een axioma en wordt bedoeld als gelijkheid van uitkomsten. Daardoor kan het enkel gebruikt op termen. • Eliminatie van identiteiten.

t1 = t2 φ[t1 /x] φ[t2 /x]

=e

Dit maakt het mogelijk om iets te zeggen over de gelijkheid van substituties als t1 en t2 vrij zijn voor x in φ. • ∀-eliminatie

∀xφ φ[t/x]

∀xe

Deze regel zegt dus dat als alle termen x in φ geldig zijn kunnen we deze door gelijk welke term t vervangen en nog steeds concluderen dat φ[t/x] geldig is. • ∀-introductie x0 .. . φ[x0 /x] ∀xi

∀xφ Deze regel start door een dummy-variabele x0 binnen een box te definiëren en die mag nergens anders voorkomen dan in die box. Als φ bewezen kan worden door x met x0 te substitueren en over die x0 werden geen veronderstellingen gemaakt kunnen we x dus door gelijk welke term vervangen. Vandaar dat we de ∀ mogen introduceren. • ∃-introductie

φ[t/x] ∃xi ∃xφ Als we weten dat het geldt voor gelijk welke t geldt het dus ook voor één van de t’s.

• ∃-eliminatie x0 φ[x0 /x] .. . χ

∃xφ

∃e χ We voeren hier een gevallenonderzoek uit voor alle mogelijke x0 , indien het voor een van die x0 geldt zonder dat we iets wisten over x0 kunnen we de ∃ elimineren.

Er bestaan heel wat basisgelijkheden in verband met kwantoren die we allemaal met bovenstaande bewijsregels kunnen bewijzen. Stel φ en ψ formules uit de predikaatlogica, dan geldt: 21

1. Zonder veronderstellingen over x: • ¬∀xφ a` ∃x¬φ • ¬∃xφ a` ∀x¬φ 2. Indien x niet vrij is in ψ: • ∀xφ ∧ ψ a` ∀x(φ ∧ ψ) • ∀xφ ∨ ψ a` ∀x(φ ∨ ψ) • ∃xφ ∧ ψ a` ∃x(φ ∧ ψ) • ∃xφ ∨ ψ a` ∃x(φ ∨ ψ) • ∀x(ψ → φ) a` ψ → ∀xφ • ∃x(φ → ψ) a` ∀xφ → ψ • ∀x(φ → ψ) a` ∃xφ → ψ • ∃x(ψ → φ) a` ψ → ∃xφ 3.

• ∀xφ ∧ ∀xψ a` ∀x(φ ∧ ψ) • ∃xφ ∨ ∀xψ a` ∃x(φ ∨ ψ)

4.

• ∀x∀yφ a` ∀y∀xφ • ∃x∃yφ a` ∃y∃xφ

Daar deze regels eenvoudig te bewijzen zijn worden de bewijzen hier niet verder besproken, ze staan weergegeven in het boek ’Logic in Computer Science - second edition’ op pagina’s 118-122.

2.3

Modellen

We gaan nu dieper in op de semantiek van de predikaatlogica, dat is het deel waar we iets zoals waarheidstabellen uit de propositielogica verwachten. Definitie 13. Stel Γ als afkorting voor een mogelijk oneindige lijst formules φ1 , φ2 , . . . , φn . Nu is Γ ` ψ geldig als er een afleiding met behulp van natuurlijke deductie bestaat met premissen enkel in Γ. Dus een bewijs van ψ naar Γ. Er zijn twee soorten karakterisatie van logica: 1. Een positieve karakterisatie: bewijstheorie geeft een positieve karakterisatie omdat het gemakkelijk is aan te tonen dat een gevolgtrekking geldig is. Het is echter heel moeilijk om te bewijzen dat er geen bewijs is. 2. Een negatieve karakterisatie: semantiek geeft een negatieve karakterisatie omdat het gemakkelijk is aan te tonen dat een gevolgtrekking niet geldig is, een tegenvoorbeeld volstaat. Het bewijzen is echter veel moeilijker omdat alle gevallen bekeken moeten worden. Bij predikaatlogica zijn er echter oneindig veel mogelijke bedelingen. Zo’n ’bedeling’ noemen we in de predikaatlogica een model. Gödels volledigheidsstelling stelt dat de predikaatlogica correct en volledig is, met andere woorden Γ |= φ als en slechts als Γ ` φ. Daarom is het belangrijk zowel de semantiek als de bewijstheorie goed onder de knie te hebben. 22

Definitie 14. Stel F een verzameling van functiesymbolen en P een verzameling predikaatsymbolen. Het koppel (F, P) kan men nu zien als een taal L. Een model M = (A, {f M }f ∈F , {P M }P ∈P ) voor L bestaat nu uit volgende onderdelen: • Een niet lege verzameling A welke het universum of domein van concrete objecten wordt genoemd. • Voor ieder functiesymbool met ariteit 0 (=M ) een concreet element f M of A. • Voor ieder functiesymbool f ∈ F van ariteit n > 0 een functie f M : An → A. • Voor ieder predikaatsymbool P ∈ F van ariteit n > 0 een deelverzameling P M ⊆ An . Het is belangrijk het onderscheid tussen f en f M en P en P M in te zien. De f en P symbolen zijn niet meer dan sybmolen, maar de f M en P M zijn respectievelijk echt een functie (of element) en een relatie in een model M. Een taal L is dus een verzameling functie- en predikaatsymbolen (F, P) terwijl een model M een taal is waaraan een verzameling A van concrete elementen is toegevoegd zoals nu wordt gedemonstreerd. Om het concept model te verduidelijken geven we een voorbeeld. Veronderderstel: def

• F = {i} met i een constante. De verzameling functiesymbolen bestaat dus uit 1 constante. def

• P = {R, F } met F een unair predicaat en R een predicaat met ariteit 2. De verzameling predikaatsymbolen bestaat dus uit 2 predikaten. Een model M bestaat uit een verzameling concrete elementen A zoals een verzameling ’toestanden’ van een computerprogramma. We interpreteren nu als volgt: • iM : de initiële- of begintoestand van het systeem. • RM : een predikaat die de mogelijke toestandsveranderingen bepaalt. • F M : een predikaat die een verzameling van eindtoestanden bepaalt. In het voorbeeld definiëren we al deze elementen als volgt: def

• A = {a, b, c} def

• iM = a def

• RM = {(a, a), (a, b), (a, c), (b, c), (c, c)} def

• F M = {b, c} We kunnen nu gemakkelijk enkele formules in dit model testen. De formule ∃yR(i, y) stelt dat er een toestandsverandering bestaat vanaf de begintoestand naar een willekeurige toestand van het model. Dit is waar omdat in RM overgangen (a, a), (a, b) en (a, c) gedefiniëerd zijn. De formule ¬F (i) stelt dat de begintoestand geen eindtoestand is. Dit klopt omdat a de begintoestand is en niet gedefiniëerd is als eindtoestand in F M . Wat hierboven informeel gebeurt is, is het checken van formules over een model. Dit wordt modelchecking genoemd. 23

Met deze modellen kunnen uitdrukkingen van de vorm ∀xφ of ∃xφ nog niet goed uitgedrukt worden. Stel namelijk dat x vrij voorkomt, dan zou men φ[a/x] kunnen proberen. Dit is echter niet geldig omdat a geen term is maar een element van het model. Het is dus noodzakelijk om formules relatief aan een omgeving te interpreteren. Een omgeving is een soort opzoekingstabel l is waarin voor elke variabele x een waarde l(x) wordt bijgehouden. Of men kan dus zeggen dat een omgeving een functie: l : var → A is die de verzameling variabelen var in de formule afbeeldt op het universum van waarden van A van het onderliggende model M. Definitie 15. Een M-bedeling of opzoekingstabel voor een model M = (A, {f M }f ∈F , {P M }P ∈P ) is een functie l van de verzameling van variabelen var naar A. De waarde van een term t in een model M relatief tot een M-bedeling l is inductief gedefiniëerd door: l(t) als t een variabele is M,l t = M,l M,l M f (t1 , . . . , tn ) als t = f (t1 , . . . , tn ) Voor een M-bedeling l, een variabele x en een element a ∈ A is de (update-)bedeling l[x 7→ a] gedefiniëerd door: a als y = x (l[x 7→ a])(y) = l(y) als y 6= x Het is nu mogelijk om een correcte semantiek te definiëren voor formules in de predikaatlogica. Definitie 16. Stel een model M voor een paar (F, P) en een M-bedeling l. Dan noemen we M |=l φ een geldigheidsrelatie M |=l φ voor elke logische formule φ over (F, P) en l door structurele inductie op φ. Als M |=l φ steek houdt, zeggen we dat φ waar is in het model M met betrekking tot de M-bedeling l. Wat volgt is dus de enige juiste syntax voor semantische berekeningen met predikaatlogica: • P : Als φ van de vorm P (t1 , t2 , . . . , tn ) is moeten de termen t1 , t2 , . . . , tn vervangen worden door de waardes opgegeven in l zodat a1 , a2 , . . . , an worden bekomen. Door nu elk functiesymbool f ∈ F als f M te interpreteren bekomen we dat M |=l P (t1 , t2 , . . . , tn ) steek houdt als (a1 , a2 , . . . , an ) in de verzameling P M zit. • ∀x: De relatie M |=l ∀xψ houdt steek als M |=l[x7→a] ψ steek houdt voor alle a ∈ A. • ∃x: De relatie M |=l ∃xψ houdt steek als M |=l[x7→a] ψ steek houdt voor enkele a ∈ A. • ¬: De relatie M |=l ¬ψ houdt steek als het niet het geval is dat M |=l ψ steek houdt. • ∨: De relatie M |=l ψ1 ∨ ψ2 houdt steek als M |=l ψ1 of M |=l ψ2 steek houdt. • ∧: De relatie M |=l ψ1 ∧ ψ2 houdt steek als M |=l ψ1 en M |=l ψ2 steek houden. • →: De relatie M |=l ψ1 → ψ2 houdt steek als M |=l ψ2 steek houdt van zodra M |=l ψ1 steek houdt. Soms wordt M 6|=l φ geschreven om aan te duiden dat M |=l φ geen steek houdt.

24

Lemma 3. Zij M een model voor een taal l, dan geldt: 1. Als t een term is en l, l0 twee M-bedelingen zijn met l(x) = l0 (x) voor alle variabelen 0 die in t optreden, dan geldt dat tM,l = tM,l . 2. Voor twee termen s, t en een M-bedeling l geldt dat (t[s/x])M,l = tM,l[x7→s

M,l ]

.

We bewijzen nu de eerste bewering met behulp van inductie over de lengte van t, het bewijs van de tweede redenering verloopt analoog: • Basisgeval: Stel dat t een variabele x is, dan treedt x op in t en geldt dat tM,l = l(x) = 0 l0 (x) = tM,l . 0

= tM,l voor i = 1, ..., n • Inductiehypothese: tM,l i i • Inductiestap: Stel nu dat t van de vorm f (t1 , . . . , tn ) is met kortere deeltermen ti . Elke variabele die in ti optreedt, treedt ook in t op. Uit de inductiehyphothese volgt nu 0 0 M,l M M,l , . . . , tM,l ) = tM,l0 waarmee het gelstelde dat tM,l = f M (tM,l n 1 , . . . , tn ) = f (t1 bewezen is. Lemma 4. Zij M een model voor een taal l, dan geldt: 1. Als φ een formule is en l, l0 twee M-bedelingen zijn met l(x) = l0 (x) voor alle x die vrij zijn in φ, dan geldt dat M |=l φ ⇔ M |=l0 φ. 2. Voor een term t, een formule φ en een M-bedeling l geldt M |=l φ[t/x] ⇔ M |=l[x7→tM,l ] φ. We bewijzen nu de eerste bewering met behulp van inductie op de lengte van φ, het bewijs van de tweede redenering verloopt analoog: • Inductiebasis: stel φ een atomaire formule P (t1 , . . . , tn ). Als x een variabele van een term ti is, dan geldt wegens het te bewijzen dat l(x) = l0 (x). Wegens lemma 3 geldt 0 dat tM,l = tM,l voor i = 1, . . . , n en dus: i i M,l M M |=l φ ⇔ (tM,l 1 , . . . , tn ) ∈ P 0 0 ⇔ (tM,l , . . . , tM,l ) ∈ PM n 1 ⇔ M |=l0 φ • Inductiehypothese: M |=l φ ⇔ M |=l0 φ voor (x1 , . . . , xn ) vrij in φ. • Inductiestap: Stel dat φ een formule ψ ∧ χ is, dan gelden: M |=l φ ⇔ M |=l ψ en M |=l χ ⇔ M |=l0 ψ en M |=l0 χ ⇔ M |=l0 φ Stel tenslotte dat φ een formule ∀xψ is. Dan zitten de vrije variabelen van φ in ψ voorgesteld als x. Hieruit volgt dat voor alle a ∈ A de bedelingen l[x 7→ a] en l0 [x 7→ a] overeenkomen voor de vrije variabelen in ψ. Hierdoor geldt dus dat: M |=l φ ⇔ M |=l[x7→a] ψ voor alle a ∈ A ⇔ hI.H.i M |=l0 [x7→a] ψ voor alle a ∈ A ⇔ M |=l0 φ. De overige gevallen zijn gelijkaardig. 25

Definitie 17. Een zin is een formule zonder vrije variabelen. Als φ een zin is geldt dat M |=l φ ⇔ M |=l0 φ voor alle M-bedelingen l en l0 omdat er geen termen door model specifieke elementen worden vervangen. De waarheidswaarde van zinnen hangt dus niet af van de bedeling. We noteren M |= φ voor zinnen φ. Definitie 18. Voor een (mogelijk oneindige) verzameling Γ van l-formules en een formule ψ stellen we dat: 1. ψ is een semantisch gevolg van Γ(Γ |= ψ) als en slechts als dan voor alle l-modellen M en M-bedelingen l geldt: uit M |=l φ voor alle φ ∈ Γ volgt dat M |=l ψ. 2. ψ is vervulbaar als M |=l ψ voor tenminste één l-model M en één M-bedeling l. 3. Γ is vervulbaar of consistent als voor tenminste één l-model M en één M-bedeling l geldt dat voor alle φ ∈ Γ : M |=l φ. 4. ψ is geldig als M |=l ψ voor alle l-modellen M en alle M-bedelingen l. In de predikaatlogica is het |= symbool dus overladen, het kan twee dingen betekenen: • Het kan duiden op model-checking: M |= φ. • Het kan duiden op semantische gevolgtrekking: φ1 , φ2 , . . . , φn |= ψ. In beide gevallen is het niet steeds mogelijk alle controles op een computer uit te voeren. In het eerste geval treedt een probleem op als het universum van waardes A van het model M oneindig is. Dit zou namelijk betekenen dat om de zin ∀xψ, waarbij x vrij is in ψ, te testen, geverifieerd moet worden dat M |=[x7→a] ψ voor een oneindig aantal elementen a. In het tweede geval is het probleem dat als men wil verifiëren dat φ1 , φ2 , . . . , φn |= ψ steek houdt, alle relevante tests voor alle mogelijke modellen met de juiste structuur - dus modellen met functies en predicaten met overeenkomende ariteit - moeten uitgevoerd worden. Dit is dus steeds onmogelijk. Soms kan men deze problemen oplossen door over de semantiek te redeneren, dit werkt echter maar op een zeer beperkt aantal gevallen waaronder gelijkheid van kwantoren. We verduidelijken met een voorbeeld: ∀x(P (x) → Q(x)) |= ∀xP (x) → ∀xQ(x) Stel M een model dat ∀x(P (x) → Q(x)) vervulbaar maakt, dan moeten we aantonen dat dit model ook ∀xP (x) → ∀xQ(x) vervulbaar maakt. Als we kijken naar de definitie van M |= ψ1 → ψ2 zijn er nu twee gevallen: 1. Als niet elk element van M P vervulbaar maakt klopt het omdat F → · vervulbaar is voor gelijk welke ·. 2. Als wel elk element van M P vervulbaar maakt dan moet, omdat M ∀x(P (x) → Q(x)) vervulbaar maakt, elk element van M ook Q vervulbaar maken. Deze twee gevallen gecombineerd tonen dus aan dat M ook ∀xP (x) → ∀xQ(x) vervulbaar maakt.

26

De formule in omgekeerde richting aantonen is echter niet mogelijk. ∀xP (x) → ∀xQ(x) |= ∀x(P (x) → Q(x)) Stel M0 een model dat ∀xP (x) → ∀xQ(x) vervulbaar maakt. Indien A0 de onderliggende 0 0 verzameling van M0 is en P M en QM de onderligende representaties van P en Q, dan zegt 0 0 M0 |= ∀xP (x) → ∀xQ(x) niets anders dan dat als P M = A0 dat QM ook gelijk moet zijn aan 0 A0 . Echter is het zo dat als P M niet gelijk is aan A0 dat de implicatie zonder meer waar is (wegens F → · ≡ T ). Er kunnen dus geen beperkingen over het model M0 worden afgeleidt. def

0

def

0

def

Er bestaat zelfs een tegenvoorbeeld: Stel A0 = {a, b}, P M = {a} en QM = {b}. Dan houdt M0 |= ∀xP (x) → ∀xQ(x) steek, maar M0 |= ∀x(P (x) → Q(x)) niet. Stelling 1. De predikaatlogica is correct en volledig: Γ |= ψ ⇔ Γ ` ψ Bovenstaande stelling staat bekend als G¨ odels volledigheidsstelling en heeft een vrij lang bewijs dat we niet volledig zullen bespreken. We bewijzen nu echter wel enkele lemma’s die in het bewijs gebruikt worden. Lemma 5. Zij L een taal van de eerste orde en B een bewijs met natuurlijke deductie van ψ met premissen φ1 en aannames φ2 . Zij x1 , . . . , x2 een lijst van de variabelen die vrij optreden in φ1 , φ2 en ψ. Stel nu M een gepaste structuur voor L met m1 , . . . , mn als onderliggende elementen van M. Stel als laaste l een bedeling voor M met l(xi ) = mi voor i = 1, . . . , n. Als M |=l φ1 ∪ φ2 dan geldt M |=l ψ We bewijzen dit met inductie op de lengte van B: • Inductiebasis: Als ψ ∈ φ1 ∪ φ2 dan volgt de bewering uit de opgave. • Inductiehypothese: De variabelen x1 , . . . , xn bevatten alle vrije variabelen die in φ1 , φ2 , ψ optreden. • Inductiestap: We onderscheiden verschillende gevallen: – Stel dat ψ = χ1 → χ2 met implicatie-introductie werd bewezen. Dan bestaat het bewijs van ψ uit premissen φ1 in χ1 en aannames φ2 in χ2 . Stel nu dat M |=l φ1 ∪ φ2 , om M |=l ψ te bewijzen mogen we M |=l φ1 aannemen en het volstaat dan om M |=l φ2 te bewijzen. We weten echter dat M |=l φ1 ∪ φ2 , χ1 en uit de inductiehypothese volgt dan dat M |=l φ2 . – Stel dat ψ = ∀xχ(x) met ∀-introductie werd bewezen. Dan bestaat er een deelbewijs B 0 met conclusie χ[x0 /x] waarbij de variabele x0 niet optreedt (behalve in gesloten boxen) in de premissen en aannames van B. Stel nu M |=l φ1 ∪ φ2 . We moeten nu M |=l ψ bewijzen. Zij m een willekeurig element uit M en zij l0 = l[x0 7→ m]. Omdat x0 niet in φ1 ∪ φ2 optreedt geldt ook dat M |=l0 φ1 ∪ φ2 . De variabelen x0 , x1 , . . . , xn bevatten alle vrije variabelen die in φ1 , φ2 , χ[x0 /x] optreden en met behulp van de inductiehypothese volgt hieruit dat M |=l0 χ[x0 /x]. Omdat m willekeurig was volgt het te bewijzen. 27

– Stel nu dat ψ door ∃-eliminatie werd bewezen. Dan is er een deelbewijs B1 van ∃xχ(x) en een deelbewijs B2 met premissen uit φ1 en aannames uit φ2 ∪ {χ[x0 /x]} waarbij de variabele x0 niet vrij voorkomt in φ1 ∪ φ2 .Stel nu M |=l φ1 ∪ φ2 en we moeten M |=l ψ bewijzen. Omdat x0 niet als vrije variabele voorkomt in B1 volgt M |=l ∃xχ(x) uit de inductiehypothese toegepast op B1 . Zij m een element uit M met M |=l[x0 7→m] χ[x0 /x], uit M |=l φ1 ∪ φ2 volgt dan dat M |=l[x0 7→m] φ1 , φ2 omdat x0 niet optreedt in φ1 ∪ φ2 . Er geldt dus dat M |=l[x0 7→m] φ1 , φ2 , χ[x0 /x]. Als we de inductiehypothese toepassen op B2 verkrijgen we dat M |=l[x0 7→m] ψ en dus dat M |=l ψ omdat x0 niet vrij voorkomt in ψ. De overige gevallen kunnen analoog worden behandeld.

Een belangrijk gevolg van deze stelling is dat als Γ ` φ dan Γ |= φ, wat dus het bewijs van Gödels volledigheidsstelling in één richting is. Definitie 19. Een verzameling van L-zinnen φ heet: • consistent als φ 6`⊥. • maximaal consistent als φ consistent is en geen echte extensie φ0 ⊃ φ van L-zinnen consistent is. • gesatureerd als voor alle L-formules φ(x) met hoogstens één vrije variabele x een constante c ∈ L bestaat met φ ` ∃xφ(x) → φ(c). Lemma 6. Zij φ een maximaalconsistente verzameling van L-zinnen die gesatureerd is, dan heeft φ een model. We bewijzen. Zij C de verzameling van constanten in L, dan is C 6= ∅. We definiëren nu een equivalentierelatie ∼ op C: c ∼ d :⇔ φ ` c = d Met de regels voor = kan men nagaan dat ∼ wel degelijk een equivalentierelatie is. Stel nu M := C/ ∼ de resulterende verzameling van equivalentieklassen waaruit we een model maken en stel f een functiesymbool van ariteit n. We definiëren f M ([c1 ], . . . , [cn ]) = [c] als c een constante is met φ ` f (c1 , . . . , cn ) = c. Er bestaat zo’n c omdat φ ` (∃x)[f (c1 , . . . , cn ) = x] en omdat φ gesatureerd is. Deze twee kenmerken samen tonen namelijk aan dat er een c bestaat met φ ` (∃x)[f (c1 , . . . , cn ) = x] → F (c1 , . . . , cn ) = c f M is een goed model omdat het onafhankelijk van de keuze van representanten van de equivalentieklassen werd gedefiniëerd. Dat kan men aantonen met de regels voor de identiteit. Stel nu R een relatiesymbool van ariteit n en ([c1 ], . . . , [cn ]) ∈ RM ⇔ φ ` R(c1 , . . . , cn ) RM is hier ook goed omdat onafhankelijk van de keuze van representanten van de equivalentieklassen werd gedefiniëerd. Ook hier kan men dit met de regels voor de identiteit bewijzen.

28

Voor een gesloten L-term t is tM = [c] voor iedere constante c met φ ` t = c. Zo’n constante bestaat omdat φ gesatureerd is (ook dit is goed gedefiniëerd). Daaruit volgt dat M |= t = s ⇔ φ ` t = s. Met inductie op de lengte van ψ tonen we nu het volgende aan: M |= ψ ⇔ φ ` ψ Als ψ = R(t1 , . . . , tn ) en tM i = [ci ] voor i = 1, . . . , n, dan geldt: M |= R(t1 , . . . , tn )

⇔ ⇔ ⇔ ⇔

M M (tM i , . . . , tn ) ∈ R ([c1 ], . . . , [cn ]) ∈ RM φ ` R(c1 , . . . , cn ) φ ` R(t1 , . . . , tn )

Stel nu dat ψ : χ ∨ γ, dan geldt M |= ψ als en slechts als (M |= χ of M |= γ) als en slechts als (φ ` χ of φ ` γ) als en slechts als φ ` ψ. De laatste equivalentie volgt uit het feit dat φ maximaal consistent is. Daaruit volgt namelijk eerst dat voor iedere L-zin ρ geldt dat ofwel ρ ∈ φ ofwel ¬ρ ∈ φ. Verder volgt vanwege de maximaliteit van φ uit χ ∨ γ ∈ φ dat χ ∈ φ of γ ∈ φ. De overige connectieven kan men analoog afwerken. Stel nu dat ψ = ∀xχ(x), dan geldt M |= ψ als en slechts dan als M |= χ[c/x] voor alle c ∈ CM |= χ[c/x] voor alle c ∈ C als en slechts dan als φ ` χ[c/x] voor alle c ∈ C als en slechts dan als φ ` ∀xχ(x). Vanzelfsprekend volgt φ ` χ[c/x] voor alle c ∈ C uit φ ` ∀xχ(x). Om de andere richting te bewijzen kiezen we vanwege de gesatureerdheid van φ een c met φ ` ∃x¬χ(x) → ¬χ[c/x]. Uit φ ` χ[c/x] volgt dus dat φ ` ¬∃x¬χ(x). Daaruit volgt dan dat φ ` ∀xχ(x) waarmee het gestelde is bewezen. Predikaatlogica biedt dus de mogelijkheid om veel meer uit te drukken dan propositielogica. Dit gaat echter ten koste van de beslisbaarheid wat wil zeggen dat er geen uniforme oplossingsmethode bestaat om een formule φ uit de predikaatlogica te bewijzen, controleren op vervulbaarheid, ... Daarom werd model checking ingevoerd, dit is wel makkelijk met een computer te checken. Een model M is namelijk niets meer dan een interpretatie van een predikaatsymbool R van ariteit 2 over een verzameling ’toestanden’ A. We geven een voorbeeld: • A = {s0 , s1 , s2 , s3 } • RM = {(s0 , s1 ), (s1 , s0 ), (s1 , s1 ), (s1 , s2 ), (s2 , s0 ), (s3 , s0 ), (s3 , s2 )} Dit model kunnen we voorstellen als een gerichte graaf: s0

s3

s1

s2

In het algemeen zal een computerprogramma moeten controleren of het model niet van een ’goede’ toestand in een ’slechte’ toestand kan geraken. Welke deze toestanden zijn zal afhangen van de situatie. Dit probleem wordt bereikbaarheid genoemd. Definitie 20. Zij n en n0 twee toppen in een gerichte graaf. Men noemt bereikbaarheid het probleem om uit te maken of het mogelijk is van n naar n0 te gaan in een eindig aantal toestandsovergangen. 29

In de figuur is toestand s2 bereikbaar vanaf staat s0 via het pad s0 → s1 → s2 . We spreken hierbij af dat elke node bereikbaar is voor zichzelf via een pad van lengte 0. s3 is hier bijvoorbeeld niet bereikbaar vanaf s0 . De vraag stelt zich nu of het mogelijk is een formule φ op te stellen met behulp van de predikaatlogica met u en v als enige vrije variabelen en R als het enige predikaatsymbool van ariteit 2 zodat φ steek houdt indien er een pad in een gerichte graaf bestaat van u naar v. Probeer bijvoorbeeld: u = v ∨ ∃x(R(u, x) ∧ R(x, v)) ∨ ∃x1 ∃x2 (R(u, x1 ) ∧ R(x1 , x2 ) ∧ R(x2 , v)) ∨ · · · Deze formule zou oneindig moeten doorgaan, dus is het geen goed gevormde formule. Volgende stellingen, welke we niet allemaal bewijzen, tonen formeel aan dat het niet mogelijk is zo’n formule op te stellen. Meer bewijzen en formules staan in het boek ’Logic in Computer Science - second edition’ op pagina’s 137-138. Stelling 2. (Compactheidstheorema) Zij Γ een verzameling van L-zinnen. Als alle eindige deelverzamelingen van Γ een model hebben (vervulbaar zijn), dan heeft ook Γ een model. We bewijzen met behulp van contradictie. Stel dat Γ niet vervulbaar is, dan houdt het semantisch equivalent Γ |=⊥ steek omdat er geen model is waarvoor all φ ∈ Γ waar zijn. Wegens de volledigheidsstelling is het sequent Γ `⊥ dan ook geldig waardoor er een bewijs met natuurlijke deductie voor moet bestaan. Dit eindig bewijs kan dus maar een eindig aantal premissen ∆ van Γ gebruiken. Hierdoor is ∆ `⊥ ook geldig waaruit met volledigheid volgt dat ∆ |=⊥. Dit is echter in tegenspraak met het feit dat alle eidndige deelverzamelingen van Γ consistent zijn. Dit wordt het L¨ owenheim-Skolem theorema genoemd. Stelling 3. Zij φ een consistente verzameling van L-zinnen. Dan bestaat er een extensie L0 van L door nieuwe constanten en een verzameling φ0 van L0 -zinnen die φ omvat zodat φ0 maximaal consistent en gesatureerd is. Stelling 4. Zij Γ een verzameling van L-zinnen en φ een L-zin. Als Γ ` φ dan bestaat er een eindige verzameling Γ0 ⊆ Γ met Γ0 ` φ. Een belangrijk gevolg van deze stellingen is dat indien ψ een zin is zodat er voor ieder natuurlijk getal n een model van ψ met meer dan n elementen bestaat, er dan ook een onV eindig model van ψ bestaat. Inderdaat, zij χn := ∃x1 ∃x2 , . . . , ∃xn 1≤i<j≤n ¬(xi = xj ) en zij Γ := {ψ} ∪ {χn : n ≥ 0}. Als ∆ een eindige verzameling van Γ is dan heeft ∆ een model. Met compactheid heeft dus ook Γ een model maar dat is oneindig.

3

Verification by model checking

Er zijn zeer veel toepassingen voor dit domein, bestaande uit het testen van kritieke veiligheidssystemen, commericeel kritische processen, ... De formele verificatietechnieken zijn recent bruikbaar geworden voor de industrie en er is steeds meer vraag naar professionals die ze kunnen toepassen. In dit hoofdstuk wordt de model checking verificatiemethode gebruikt. Het is gebaseerd op temporele logica. Definitie 21. In temporele logica wordt het statische waar/vals zijn van formules vervangen door een dynamisch waar/vals zijn van formules. Waar in propositionele logica een formule steeds waar of vals is, hangt dit in temporele logica af van de toestand waarin het systeem zich bevindt. 30

In model checking zijn de modellen M overgangssystemen en de eigenschappen φ zijn formules in temporele logica. Om te verifieren dat een systeem aan een eigenschap voldoet moeten drie dingen gedaan worden: 1. Het systeem moet gemodelleerd worden in de beschrijvingstaal van de model checker zodat men een model M bekomt. 2. Men met de eigenschap coderen in de specificatietaal van de model checker zodat men een formule φ in temporele logica bekomt. 3. Men moet de model checker uitvoeren met model M en formule φ. De output van een model checker is ’ok’ als M |= φ en ’niet ok’ in het andere geval waarbij meestal een oorzaak van de fout wordt gegeven. Er zijn heel veel soorten temporele logica en ze worden ingedeeld volgens tijd : • Lineair-time logica: hier wordt tijd voorgesteld als een verzameling paden waarbij een pad een opeenvolging is van tijdsinstanties. • Branching-time logica: hier wordt tijd voorgesteld als een boom met het huidige moment als wortel en het vertakt naar de toekomst. Temporele logica heeft dus een dynamisch aspect waardoor de waarheid van een formule afhangt van de tijd waarin het model zich bevindt. We zullen twee logica’s bestuderen: 1. Lineair-time Temoral Logic (LTL): hier wordt van een lineair-time logica gebruik gemaakt. 2. Computation Tree Logic (CTL): hier wordt van een branching-time logica gebruik gemaakt.

3.1

Lineaire-tijd temporele logica of LTL

LTL is een temporele logica met connectiven die toelaten om naar de toekomst te refereren. Er wordt een opeenvolging van toestanden gemodelleerd die oneindig doorloopt in de toekomst. Deze opeenvolging wordt het pad genoemd. Aangezien de toekomst niet bepaald is worden verschillende paden onderzocht, elk van deze paden stelt een andere toekomst voor. Gelijk welk pad kan later de ’echte’ toekomst blijken te zijn. Er wordt gewerkt met een vaste set atomen (Atoms) of atomaire formules (bv. p, q, r, . . . of p1 , p2 , . . .) welke voor feiten (bv. Printer p3 is bezig, of Proces 5267 is gepauzeerd, ...) staan. In Backus-Naurvorm ziet de syntax van LTL er als volgt uit: φ ::= > | ⊥ | p | (¬φ) | (φ∧φ) | (φ∨φ) | (φ → φ) | (Xφ) | (Fφ) | (Gφ) | (φUφ) | (φWφ) | (φRφ) waarin p een propositioneel atoom is uit Atoms. Opvallend zijn hier X, F, G, U en R welke de temporele connectieven zijn. De betekenis wordt later besproken. Het is belangrijk te weten hoe de prioriteit van de conectieven zijn, daarom spreken we het volgende af. De unaire connectiven (¬, X, F, G) hebben de hoogste prioriteit. Juist daaronder komen U, R en W en daarna komen ∧ en ∨ en op het laatste →. We hebben met andere woorden van hoge naar lage prioriteit: 31

1. ¬, X, F, G 2. U, R, W 3. ∧, ∨ 4. → Wij zullen nu transitietoestandssystemen bestuderen waarbij een systeem door middel van toestanden (een statische structuur) en transities (een dynamische structuur) gemodelleerd wordt. Definitie 22. Een transitietoestandssysteem M = (S, →, L) is een verzameling toestanden S, voorzien van een transitierelatie → zodat elke s ∈ S een s0 ∈ S heeft met s → s0 en een labelende functie L : S → P(Atoms). We noemen deze transitietoestandssystemen nu simpelweg modellen. De relatie → geeft aan hoe het systeem van de ene toestand naar een andere toestand kan gaan. De labelende functie L verbind met iedere toestand een verzameling atomaire proposities L(s) die waar zijn in de gegeven toestand s. Met P(Atoms) wordt de ’power set’ van Atoms bedoeld. Zo is de power set van {p, q} gelijk aan {∅, {p}, {q}, {p, q}}. Een andere manier om naar L te kijken is als een valuatie voor alle propositionele atomen. Enkel hangt deze valuatie nu af van de toestand s waarin het systeem zich bevindt. Van zodra mogelijk worden deze modellen voorgesteld als een gerichte graaf. Als voorbeeld nemen we volgend model M: • S := {s0 , s1 , s2 } • →:= {s0 → s1 , s0 → s2 , s1 → s0 , s1 → s2 , s2 → s2 } • L(s0 ) := {p, q}, L(s1 ) = {q, r}, L(s2 ) = r Deze informatie kan voorgesteld worden door middel van volgende figuur: s0 p, q s1

s2

q, r

r

De definitie van een transitietoestandssysteem stelt dat er nooit toppen mogen zijn waar geen pijl uit vertrekt. In realiteit bestaat zo’n toestand echter wel, het systeem loopt dan vast. Dit wordt gemodelleerd door een extra top toe te voegen waar het enige pad die er uit vertrekt een pad naar zichzelf is. Deze top wordt vaak met sd van ’deadlock’ aangeduidt. Definitie 23. Een pad in een model M = (S, →, L) is een oneindige sequentie van toestanden s1 , s2 , s3 , . . . in S zodat voor elke i ≥ 1, si → si+1 . Een pad wordt genoteerd als s1 → s2 → · · · .

32

Stel dat we een pad π = s1 → s2 → s3 → · · · hebben dan duiden we met π i het pad aan startend in top si waarbij i de locatie is. Dus bv. π 2 in π = s0 → s1 → s2 → · · · is s1 → · · · . We kunnen nu overgaan tot het definieren van de waarheidswaarden van de connectieven. Stel M = (S, →, L) een model en π = s1 → s2 → · · · een pad in M. Dan schrijven we |= als π aan een LTL formule voldoet op volgende manier: 1. π |= > 2. π 6|=⊥ 3. π |= p als en slechts als p ∈ L(s1 ) 4. π |= ¬φ als en slechts als π 6|= φ 5. π |= φ1 ∧ φ2 als en slechts als φ |= φ1 en φ |= φ2 6. π |= φ1 ∨ φ2 als en slechts als φ |= φ1 of φ |= φ2 7. π |= φ1 → φ2 als en slechts als π |= φ2 van zodra π |= φ1 8. π |= Xφ als en slechts als π 2 |= φ 9. π |= Gφ als en slechts als π i |= φ, ∀i ≥ 1 10. π |= Fφ als en slechts als π i |= φ, ∃i ≥ 1 11. π |= φUψ als en slechts als ∃i ≥ 1 : π i |= ψ en ∀j < i : π j |= φ 12. π |= φWψ asa ofwel ∃i ≥ 1 : π i |= ψ en ∀j < i : π j |= φ ofwel ∀k ≥ 1 : π k |= φ 13. π |= φRψ asa ofwel ∃i ≥ 1 : π i |= φ en ∀j ≤ i : π j |= ψ ofwel ∀k ≥ 1 : π k |= ψ De nieuwe temporele connectieven vereisen wat meer uitleg: • neXt: hier wordt gewoon de eerste toestand uit het pad verwijderd en wordt vanaf de tweede toestand naar het pad gekeken. • Future: dit geldt vanaf dat er één begintoestand bestaat waarvoor het pad aan φ voldoet. • Globally: het pad moet aan φ voldoen vertrekkend van gelijk welke toestand. • Until: een formule φ1 Uφ2 houdt steek op een pad zolang φ1 ononderbroken steek houdt tot dat (until) φ2 steek houdt. Het is dus vereist dat op een zeker punt in de toekomst φ2 steek houdt. • Weak until: dit is het zelfde als Until maar er wordt hier niet vereist dat φ2 op een zeker punt in de toekomst steek houdt. • Release: dit is de tegenganger van U, m.a.w φRψ ≡ ¬(¬φU¬ψ). Opdat φRψ zou gelden moet ψ waar zijn tot en met het moment dat φ waar wordt.

33

De connectieven R en W lijken zeer sterk op elkaar ze wisselen de rol van φ en ψ om en ook loopt W maar tot i − 1 terwijl R tot en met i loopt. De toekomst behort hierbij ook tot het heden en omgekeerd in tegenstelling tot de modale logica. Als we dus ’in alle toekomstige toestanden’ zeggen bedoelen we hiermee ook de huidige toestand. Met dit systeem kunnen we dus controleren of paden aan LTL-formules voldoen. Om een systeem te verifiëren moeten we kunnen bepalen of een volledig model M aan een LTL formule voldoet. We zeggen dat dit het geval is indien elk mogelijk uitvoeringspad van het model aan de LTL formule voldoet. Definitie 24. Stel M = (S, →, L) een model, s ∈ S en φ een LTL formule. We schrijven nu M, s |= φ als voor elk uitvoeringspad π van M startend met s geldt dat π |= φ. s0 p, q s1

s2

q, r

r

Als voorbeeld doen we enkele model checks op bovenstaande afbeelding: • M, s0 |= p ∧ q houdt steek omdat p en q in s0 zelf zitten, dus s0 : π |= p ∧ q voor elk pad π beginnend bij s0 . • M, s0 |= ¬r houdt steek omdat r niet in s0 zit. • M, > houdt wegens de definitie steek. • M, s0 |= Xr houdt steek omdat alle paden van s0 ofwel s1 ofwel s2 hebben als volgende toestand en elk van deze twee toestanden bevat r. • M, s0 |= X(q ∧ r) houdt geen steek omdat het pad met als volgende knoop s2 geen q bevat. • M, s0 |= G¬(p∧r) houdt steek omdat er in geen enkel pad beginnend in s0 een toestand zit waar p ∧ r geldt. • M, s2 |= Gr houdt steek omdat alle toestanden die bereikbaar zijn vanaf s2 en ook zichzelf r bevatten. • Voor gelijk welke toestand s van M geldt M, s |= F(¬q ∧ r) → FGr. Dit zegt dat gelijk welk pad π beginnend bij s dat leidt tot een toestand waarin (¬q ∧ r) geldig is, dat dit pad π dan ook aan FGr voldoet. Dit is hier het geval omdat als het pad een toestand heeft waarin (¬q ∧ r) die toestand s2 moet zijn waarin inderdaad FGr geldt. Dit laatste zegt gewoon dat er uiteindelijk een toestand moet zijn waar r continu geldt. • De formule GFp drukt uit dat p oneindig veel voorkomt in het pad. Dus hoelang je het pad ook volgt (G) je zal steeds een p hebben die voorop ligt (F). Zo voldoet het pad s0 → s1 → s0 → s1 → · · · hieraan maar het pad s0 → s2 → s2 → s2 → · · · niet. 34

• Als in het model een pad startend van s0 oneindig veel p’s bevat moet dit het pad s0 → s1 → s0 → s1 → · · · zijn. In dat geval bevat het ook oneindig veel r’en waardoor M, s0 |= GFp → GFr geldt. Andersom geldt M, s0 |= GFr → GF niet omdat er een pad beginnend bij s0 gevonden kan worden dat oneindig veel r’en bevat maar slechts één p. Praktisch gezien wordt LTL gebruikt voor atomaire beschrijvingen zoals busy en accepted. Echter zijn er beperkingen aan wat met LTL uitgedrukt kan worden, er kan niets gezegt worden over het bestaan van een pad. Zo is het niet mogelijk na te gaan of het mogelijk is om van gelijk welke toestand te ’herstarten’, of na te gaan of het mogelijk is dat ’de lift stil blijft staan op de derde verdieping met gesloten deuren’, ... Definitie 25. We zeggen dat twee LTL formules φ en ψ semantisch equivalent, of equivalent zijn (φ ≡ ψ), als voor alle modellen M en alle paden π in M geldt dat π |= φ als π |= ψ. Equivalentie tussen twee formules φ en ψ betekent dat φ en ψ semantisch verwisselbaar zijn, op deze manier kunnen we rekenregels opstellen: • Rekenregels betreffende dualiteit: – – – – –

¬Gφ ≡ F¬φ ¬Fφ ≡ G¬φ ¬Xφ ≡ X¬φ ¬(φUψ) ≡ ¬φR¬ψ ¬(φRψ) ≡ ¬φU¬ψ

• Rekenregels betreffende distributiviteit: – F(φ ∨ ψ) ≡ Fφ ∨ Fψ – G(φ ∧ ψ) ≡ Gφ ∧ Gψ Het geldt zeker niet dat F distributief is over ∧ of dat G distributief is over ∨. • Bijkomende rekenregels: – – – – – – –

Fφ ≡ >Uφ Gφ ≡⊥ Rφ φUψ ≡ φWψ ∧ Fψ φWψ ≡ φUψ ∨ Gφ φWψ ≡ ψR(φ ∨ ψ) φRψ ≡ ψW(φ ∨ ψ) φUψ ≡ ¬(¬ψU(¬φ ∧ ¬ψ)) ∧ ¬ψ)) ∧ Fψ

Een adequate set van connectieven in propositielogica is {⊥, ∧, ¬} omdat hiermee alle andere connectieven ∨, →, >, . . . gevormd kunnen worden. Ook in LTL bestaan er zo’n adequate verzamelingen van connectieven. Hierbij moeten volgende dingen in acht genomen worden: • X kan niet worden afgeleid uit een combinatie van de andere LTL connectieven. • De verzamelingen {U, X}, {R, X}, {W, X} zijn adequaat. De afleidingsregels staan in ’Logic in Computer Science - second edition’ op pagina’s 186-187. 35

3.2

Computational Tree Logic of CTL

In tegenstelling tot LTL is dit een Branching-time logica. CTL heeft de mogelijkheid om kwantoren te mixen wat niet kon bij LTL omdat voor de formule steeds impliciet een universele quantor stond. CTL kan daarom gezien worden als een uitbreiding van LTL met kwantoren: • A: voor alle paden of onvermijdbaar • E: er bestaat een pad of mogelijk In CTL komen deze extra symbolen steeds samen voor met sommige LTL connectieven waardoor CTL uit volgende onderdelen bestaat: • atomen: p, q, r, . . . of p1 , p2 , p3 , . . . • logische connectieven: ⊥, >, ¬, ∧, ∨, → • temporele connectieven: AX, EX, AF, EF ,AG, EG , AU, EU In Backus-Naurvorm ziet de syntax van CTL er als volgt uit: φ ::= ⊥ | > | p | (¬φ) | (φ∧φ) | (φ∨φ) | (φ → φ) | AXφ | EXφ | AFφ | EFφ | AGφ | EGφ | A[φUφ] | E[φUφ] De prioriteit van de connectieven zijn gelijkaardig aan die van LTL en van hoge prioriteit naar lage prioriteit hebben we: 1. ¬, AX, EX, AF, EF, AG, EG 2. ∧, ∨ 3. →, AU, EU Als we A of E gebruiken bij U noteren we dit steeds met vierkante haakjes. Dit verhoogt de leesbaarheid van de formule en sommige model checking programmas/methodes vereisen dit. Formules zoals A[(rUq) ∧ (pUr)] zijn niet goed gevormd omdat er geen logische connectieven binnen A[] of E[] mogen staan. Ook CTL formules worden over een transitiesysteem M = (S, →, L) ge¨ınterpreteerd. We kunnen nu dus overgaan tot het definieren van de waarheidswaarden of geldigheid van een CTL formule φ in een toestand s ∈ S van een model. Deze geldigheid wordt informeel gedefiniëerd als: • Als φ atomair is bepaalt de labelende functie L de waarheidswaarde. • Als het meest prioritaire connectief van φ een logisch connectief is dan wordt de waarheidswaarde door de waarheidstabel ervan bepaald samen met verdere recursie. • Als het meest prioritaire connectief van φ een operator beginnend met A is, dan is het waar als alle paden startend bij s voldoen aan de ’LTL formule’ verkregen zonder de A kwantor. • Als het meest prioritaire connectief van φ ene operator beginnend met E is, dan is het waar als er een pad startend bij s voldoet aan de ’LTL formule’ verkregen zonder de E kwantor. 36

Meer formeel worden de waarheidswaardes als volgt gedefiniëerd. Stel M = (S, →, L) een model voor CTL, s ∈ S en φ een CTL formule. De relatie M, s |= φ is op volgende manier recursief op φ gedefiniëerd: 1. M, s |= > en M, s 6|=⊥ 2. M, s |= p als p ∈ L(S) 3. M, s |= ¬φ als M, s 6|= φ 4. M, s |= φ1 ∧ φ2 als M, s |= φ1 en M, s |= φ2 5. M, s |= φ1 ∨ φ2 als M, s |= φ1 of M, s |= φ2 6. M, s |= φ1 → φ2 als M, s 6|= φ1 of M, s |= φ2 7. M, s |= AXφ als ∀s1 : s → s1 ⇒ M, s1 |= φ. Dus AX zegt ’in elke volgende toestand’ 8. M, s |= EXφ als ∃s1 : s → s1 ⇒ M, s1 |= φ. Dus EX zegt ’in een volgende toestand’ 9. M, s |= AGφ als ∀ paden s = s1 → s2 → s3 → · · · en ∀i ≥ 1 geldt dat M, si |= φ. Dus AG zegt dat langs alle paden beginnend in s de eigenschap φ overal geldig moet zijn. 10. M, s |= EGφ als ∃ een pad s = s1 → s2 → s3 → · · · en ∀i ≥ 1 geldt dat M, si |= φ. Dus EG zegt dat er een pad moet zijn beginnend in s waarlangs de eigenschap φ overal geldig moet zijn. 11. M, s |= AFφ als er ∀ paden s = s1 → s2 → s3 → · · · een i ≥ 1 bestaat : M, si |= φ. Dus AF zegt dat dat voor alle paden beginnend in s er een toekomstige toestand moet zijn waar φ geldt. 12. M, s |= EFφ als er ∃ een pad s = s1 → s2 → s3 → · · · een i ≥ 1 bestaat : M, si |= φ. Dus EF zegt dat er een pad moet zijn beginnend in s waarop er een toekomstige toestand moet zjn waar φ geldt. 13. M, s |= A[φ1 Uφ2 ] als er ∀ paden s = s1 → s2 → s3 → · · · een i ≥ 1 bestaat : M, si |= φ2 en er ∀j < i : M, sj |= φ1 . Dus AU zegt dat alle paden beginnend in s voldoen aan φ1 todat aan φ2 voldaan wordt. 14. M, s |= E[φ1 Uφ2 ] als er voor een pad s = s1 → s2 → s3 → · · · een i ≥ 1 bestaat : M, si |= φ2 en er ∀j < i : M, sj |= φ1 . Dus EU zegt dat er een pad bestaat beginnend in s dat voldoet aan φ1 todat aan φ2 voldaan wordt. Als voorbeeld stellen we een model M = (S, →, L) met volgende componenten: • S = {1, 2, 3, 4, 5, 6, 7, 8} • L(1) = {IA , IB }

• L(5) = {IA , PB }

• L(2) = {PA , IB }

• L(6) = {RA , PB }

• L(3) = {RA , IB }

• L(7) = {RA , RB }

• L(4) = {IA , RB }

• L(8) = {PA , RB } 37

Dit model kunnen we voorstellen zoals in onderstaande tekening: 1

2

3

6

4

7

5

8

Dit model kan zinvol ge¨ınterpreteerd worden op volgende manier: • IX proces X zit in start op (Initialize) • PX proces X verwerkt (Process) • RX proces X vraag aan (Request) We testen nu of enkele practische voorbeelden aan dit model voldoen: • M, 1 |= IA omdat IA geldt in toestand 1. • M, 2 6|= IA omdat IA niet geldt in toestand 2. • M, 1 |= AX(RA ∨ RB ) omdat in elke toestand volgend op 1 ofwel RA ofwel RB geldt. • M, 3 6|= AXPA omdat in toestand 7 PA niet geldt. • M, 1 6|= EXPB omdat er geen toestanden volgend op 1 zijn waarin PB geldt. • M, 3 |= EXPA omdat er een toestand (2) volgend op 3 is waarin PA geldt. • M, 1 |= AF(RA ∨ RB ) omdat voor elk pad vertrekkend uit 1 er een toestand is waarvoor RA of RB geldig zijn. • M, 5 6|= AFRB omdat er een pad vertrekkend uit 5 bestaat waarop RB nooit geldig wordt. • M, 1 |= EF(RA ∧ RB ) omdat er een pad bestaat vertrekkend uit 1 waarop zowel RA als RB geldig worden. • M, 5 6|= EF(PA ∧ PB ) omdat er geen pad bestaat vanuit 5 waarop zowel PA als PB geldig worden. • M, 1 |= AG(RA → EFPA ) omdat voor alle paden beginnend bij 1 het in alle toestanden zo is dat als RA geldt dat er dan een pad bestaat waarop in de toekomst PA zal gelden.

38

• M, 1 6|= AG(RA → AFPA ) omdat het niet zo is dat voor alle paden beginnend bij 1 en alle toestanden op die paden, dat indien RA geldt er dan op gelijk welk pad in de toekomst een toestand zal zijn waar PA zal gelden. • M, 2 |= EG(¬PA → RB ) omdat er een pad vertrekkend uit 2 bestaat waarvoor het in alle toestanden zo is dat indien PA niet geldt dat dan RB geldt. • M, 2 6|= EGPA omdat er geen pad bestaat vertrekkend uit 2 waarop in alle toestanden PA geldt. • M, 1 |= ¬A[RA UPA ] omdat niet op alle paden vertrekkend vanuit 1 geldt dat RA geldt tot dat PA geldt. • M, 7 6|= A[PA URA ] omdat niet op alle paden vertrekkend vanuit 7 geldt dat PA geldt tot dat RA geldt. • M, 1 |= EXE[RA UPA ] omdat er een opvolger van 1 bestaat waarvoor er een pad bestaat dat vertrekt uit deze opvolger waarop RA geldt totdat PA geldt. • M, 7 6|= E[(PA ∧ PB )U(IA ∨ IB )] omdat er geen pad beginnend uit 7 bestaat waarvoor (PA ∧ PB ) geldt totdat (IA ∨ IB ) geldt. Definitie 26. Twee CTL formules φ en ψ zijn semantisch equivalent (φ ≡ ψ) als voor alle modellen M = (S, →, L) en alle toestanden s ∈ S geldt dat M, s |= φ ⇔ M, s |= ψ. Net zoals in LTL bestaan er in CTL enkele belangrijke equivalenties: • Rekenregels betreffende de Morgan: – ¬AFφ ≡ EG¬φ – ¬EFφ ≡ AG¬φ – ¬AXφ ≡ EX¬φ • Bijkomende rekenregels – AFφ ≡ A[>Uφ] – EFφ ≡ E[>Uφ] – A[φUψ] ≡ ¬(E[¬ψU(¬φ ∧ ¬ψ)] ∨ EG¬ψ) Het is echter niet mogelijk om ook E[φUψ] met behulp van andere connectieven uit te drukken. We bewijzen nu de laatste equivalentie. Stel M = (S, →, L) een model en s ∈ S: • Geval A: Stel M, s |= A[φUψ] (*) en M, s 6|= ¬(E[¬ψU(¬φ ∧ ¬ψ)] ∨ EG¬ψ), dan zijn er twee gevallen: 1. Er bestaat een pad π = s1 → s2 → · · · met s1 = s zodat er een k bestaat met M, sk |= ¬φ ∧ ¬ψ en M, sj |= ¬ψ voor alle j < k. Uit (*) volgt dan dat er een l bestaat met M, sl |= ψ en M, sj |= φ voor alle j < l. Vergelijken we echter l met k dan zien we dat als l ≤ k dat er een tegenspraak is met M, l 6|= ¬ψ. Als l > k dan geldt M, sk |= φ wat strijdig is met M, sk |= ¬φ ∧ ¬ψ.

39

2. Er bestaat een pad π = s1 → s2 → · · · zodat M, sk |= ¬ψ voor alle k. In dit geval kan (*) niet gelden. • Geval B: Stel nu M, s 6|= A[φUψ]. Er bestaat dan een pad π = s1 → s2 → · · · met s = s1 zodat M, sk |= ¬ψ voor alle k. Of er bestaat voor alle k met M, sk |= ψ een l < k met M, sl |= ¬φ. Als M, sk |= ¬ψ voor alle k dan volgt EG¬ψ daaruit en dus geldt de ontkenning van de rechter kant in M, s. Stel nu dat M, sk |= ¬ψ niet voor alle k geldt, dan bestaat er een minimale k waarvoor M, sk |= ψ. Voor deze k vinden we dan een l < k met M, sl |= ¬φ. Dan geldt M, sl |= ¬φ ∧ ¬ψ en voor alle j < l geldt dan M, sl |= ¬ψ waardoor de ontkenning van de rechterkant geldig is in M, s. Net zoals in propositionele logica en LTL kunnen sommige connectieven geschreven worden in vorm van andere connectieven en er is dus redundantie tussen de connectieven. Een adequate set connectieven is een verzameling connectieven die het mogelijk maken om alle connectieven uit te drukken. Theorema 3. Een verzameling van temporele connectieven in CTL is adequaat als en slechts als deze verzameling:   tenminste één element van {AX, EX} bevat. tenminste één element van {EG, AF, AU} bevat.  zeker {EU} bevat. We bewijzen dit in verschillende stappen en tonen eerst het adequaat zijn aan: 1. AXφ ≡ ¬EX¬φ 2. EXφ ≡ ¬AX¬φ 3. EFφ ≡ E[>Uφ] 4. AGφ ≡ ¬EF¬φ 5. A[φUψ] ≡ ¬(E[¬ψU(¬φ ∧ ¬ψ)] ∨ [EG¬ψ]) 6. AFφ ≡ A[>Uφ] 7. EGφ ≡ ¬AF¬φ We bewijzen nu dat een adequate verzameling tenminste één element uit {AX, EX} moet bevatten. Stel hiervoor volgend CTL model M: 0

1

2 p

Er geldt nu dat M, 0 6|= EXp en M, 1 |= EXp. Door middel van inductie bewijzen op de lengte van φ we nu dat voor alle CTL formules die nog EX, nog AX bevatten geldt dat M, 0 |= φ als en slechts als M, 1 |= φ.

40

• Inductiebasis: Als φ gelijk is aan ⊥, > of p dan klopt de bewering omdat toppen 0 en 1 dezelfde atomen waar maken. • Inductiehypothese: M, 0 |= φ als en slechts als M, 1 |= φ voor een φ van lengte n. • Inductiestap: We maken onderscheid tussen de verschillende connectieven: – Als φ een ontkenning, conjuctie, disjunctie of implicatie van twee CTL formules is dan volgt de bewerking meteen uit de inductiehypothese. – Als φ = EGψ dan geldt M, 0 |= φ als en slechts dan als M, i |= ψ voor i = 0, 1, 2 en M, 1 |= φ als en slechts dan als M, i |= ψ voor i = 1, 2. Uit de inductiehypothese volgt dan dat M, 0 |= ψ als en slechts dan als M, 1 |= ψ, dus M, 0 |= φ als en slechts dan als M, 1 |= φ. – Als φ = E[ψUψ 0 ] dan geldt M, 0 |= φ als en slechts dan als er een i ≥ 0 bestaat waarvoor geldt dat M, i |= ψ 0 en M, j |= ψ voor alle j < i. Uit de inductiehypothese volgt dan dat M, 0 |= ψ als en slechts dan als M, 1 |= ψ en ook dat M, 0 |= ψ 0 als en slechts dan als M, 1 |= ψ 0 . ∗ Stel nu dat M, 0 |= φ, dan bestaat er een i ≥ 0 zodat M, i |= ψ 0 en M, j |= ψ voor alle j < i geldt. Als i = 0, 1 dan geldt M, 1 |= ψ 0 en dus M, 1 |= φ. Als i = 2 dan geldt M, i |= ψ 0 en M, 1 |= ψ en dus M, 1 |= φ. ∗ Stel dat M, 1 |= φ, dan bestaat er een i ≥ 1 zodat M, i |= ψ 0 en M, j |= ψ voor alle 1 ≤ j < i. Als i = 1 dan geldt M, 0 |= ψ 0 en dus M, 0 |= φ. Als i = 2 dan geldt M, 1 |= ψ en M, 0 |= ψ en dus M, 0 |= φ. De andere gevallen kan men reduceren tot de zojuist behandelde gevallen. We bewijzen nu dat een adequate verzameling tenminste één element van {EG, AF, AU} bevat. Stel hiervoor volgend CTL model M: 3

2

1

··· 0 p 3’

2’

1’

···

Dan geldt M, i |= AFp voor alle i ≥ 0 en M, i0 6|= AFp voor alle i > 0. Voor alle CTL formules φ die geen EG, AF of AU bevatten bestaat er een nφ > 0 zodat voor alle i, j ≥ nφ geldt: M, j |= φ ⇔ M, i |= φ ⇔ M, i0 |= φ We bewijzen dit met behulp van inductie over de lengte van φ: • Inductiebasis: Als φ een atoom is dan is de bewering duidelijk. • Inductiehypothese: Er bestaat een nφ > 0 zodat voor alle i, j ≥ nφ geldt dat M, j |= φ ⇔ M, i |= φ ⇔ M, i0 |= φ voor een φ van lengte n. 41

• Inductiestap: We maken onderscheid tussen de verschillende connectieven: – Als φ een ontkenning, conjunctie, disjunctie of implicatie van twee CTL-formules is, dan volgt de bewering rechtstreeks uit de inductiehypothese. – Als φ = EXψ dan stellen we nφ := nψ + 1 waardoor voor alle i ≥ nφ geldt dat i − 1 ≥ nψ . Wegens de inductiehypothese geldt nu ook dat M, i |= φ ⇔ M, i − 1 |= ψ ⇔ M, j − 1 |= ψ ⇔ M, j |= φ Verder geldt dat M, i |= φ ⇔ M, i − 1 |= ψ ⇔ M, (i − 1)0 |= ψ ⇔ M, i0 |= φ – Als φ = E[ψUψ 0 ] dan stellen we nφ := max{nψ , nψ0 }. Voor alle i ≥ nφ geldt dan dat i ≥ nψ en i ≥ nψ0 . ∗ Stel nu M, i |= φ, dan bestaat er een k ≤ i met M, k |= ψ 0 en voor alle k < l ≤ i geldt dan dat M, l |= ψ. Als M, i |= ψ 0 dan volgt daaruit met behulp van de inductiehypothese dat M, j |= ψ 0 en M, j |= φ. Verder geldt wegens de inductiehypothse dat M, i0 |= ψ 0 en M, i0 |= φ. ∗ Stel nu M, i 6|= ψ 0 , dan geldt wegens de inductiehypothse dat M, j 6|= ψ 0 voor alle j ≥ nψ0 en M, i0 6|= ψ 0 . Uit M, i |= φ volgt dan dat M, i |= ψ waardoor wegens de inductiehypothese geldt dat M, j |= ψ voor alle j ≥ nψ en M, i0 |= ψ. Wegens M, i |= φ en M, j 6|= ψ 0 voor alle j ≥ nψ0 geldt dat M, nφ − 1 |= φ. Deze vaststelling, samen met de structuur van het model zorgen ervoor dat M, j |= φ voor alle j ≥ nφ en M, i0 |= φ. Omgekeerd stel M, i0 |= φ, dan volgt analoog M, i |= φ en daarmee dus M, j |= φ. Als laatste bewijzen we dat een adequate verzameling zeker EU moet bevatten, we beschouwen hiervoor volgend model M:

···

3 p

2 p

1 p 0 q

···

˜2 p

˜1 p

˜0

Dan geldt M, i |= E[pUq] voor alle i ≥ 0 en M, i0 6|= E[pUq] voor alle i > 0. Verder bestaat er voor alle CTL formules φ die geen EU bevatten, een nφ > 0 zodat voor alle i ≥ nφ geldt: M, i |= φ ⇔ M, i0 |= φ 42

We bewijzen dit met behulp van inductie over de lengte van φ: • Inductiebasis: Als φ een atoom is stellen we nφ := 1. De bewering geldt dan omdat in toestand i en i0 dezelfde atomen gelden voor i > 0. • Inductiehypothese: Voor alle CTL formules φ die geen EU bevatten, bestaat er een een nφ > 0 zodat voor alle i ≥ nφ geldt dat M, i |= φ ⇔ M, i0 |= φ. • Inductiestap: We maken onderscheid tussen de verschillende connectieven: – Als φ een ontkenning, conjuctie, disjunctie of implicatie van twee CTL formules is dan volgt de bewerking meteen uit de inductiehypothese. – Stel φ = EXψ en nφ := nψ + 1: ∗ Stel dat M, i |= φ, dan geldt M, i |= ψ of M, i − 1 |= ψ of M, (i − 1)0 |= ψ. Uit de inductiehypothese volgt dan dat M, i0 |= ψ of M, (i − 1)0 |= ψ waaruit volgt dat M, i0 |= φ. Het geval M, i0 = φ wordt analoog behandeld. – Stel φ = EFψ en nφ := nψ . ∗ Stel dat M, i |= φ, dan bestaat er een toestand j die bereikbaar is vanuit i met M, j |= ψ. Deze toestand is ook vanuit i0 bereikbaar zodat M, i0 |= φ. Het geval M, i0 |= φ wordt analoog behandeld. – Stel φ = A[ψUχ] en nφ := nψ ∗ Stel dat M, i |= φ, dan volgt daaruit dat M, i |= χ waaruit met de inductiehypothese volgt dat M, i0 |= χ en dus M, i0 |= φ. Het geval M, i0 |= φ wordt analoog behandeld.

3.3

Algoritmes voor model checking

Een mens zal het model ontbinden tot een oneindige parseboom en zo elk pad controleren. Om een model te checken heeft een computer uiteraard een eindige datastructuur nodig. We zoeken dus een efficiënt algoritme waarmee, gegeven een model M, s ∈ S en formule φ, gecontroleerd kan worden of M, s |= φ steek houdt. Zo’n algoritme moet teruggeven of de formule steek houdt of niet, indient niet moet het pad teruggegeven worden dat een tegenvoorbeeld vormt. Er zijn twee mogelijke manieren waarop men dit zou kunnen doen: 1. Aan het algoritme wordt een model M, een formule φ en een toestand s0 gegeven. Het algoritme zou dan moeten antwoorde ’ja’ (M, s0 |= φ houdt steek), of ’nee’ (M, s0 |= φ houdt geen steek). 2. Aan het algoritme wordt enkel een model M en een formule φ gegeven. Het algoritme geeft dan alle s ∈ S terug waarvoor M, s |= φ steek houdt. We stellen nu een model voor die op de tweede manier CTL formules kan checken, het labelling algoritme. Dit algoritme moet niet alle CTL connectieven kunnen behandelen omdat de connectieven {⊥, ¬, ∧} adequaat zijn voor de propositionele delen van de CTL formule en de connectieven {AF, EU, EX} adequaat zjn voor de temporele delen van de CTL formule. Voordat een CTL formule φ aan het model gegeven wordt, moet φ dus herschreven worden 43

zodat φ enkel maar connectieven uit bovenstaande adequate verzamelingen bevat. We geven nu het algoritme: • INPUT: een model M = (S, →, L) en een CTL formule λ. • OUTPUT: de verzameling van toestanden van M die aan λ voldoen (s ∈ S : M, s |= λ). Veronderstellend dat de formule gepreprocessed is zodat er enkel connectieven uit bovenstaande adequate verzamelingen in zitten moeten we de toestanden van M nu labelen. We labelen de toestanden met de deelformules vanλ die in die toestand geldig zijn. We beginnen met de kleinste deelformules en werken verder tot we aan λ zelf komen. Stel dat ψ een deelformule is van λ en dat alle toestanden die voldoen aan de onmiddelijke deelformules van ψ al gelabeld zijn. Door middel van een gevallenonderzoek bepalen we nu welke toestanden we met ψ moeten labellen. Als ψ gelijk is aan: • ⊥: dan moeten geen toestanden gemarkeerd worden. • >: iedere toestand moet met > gelabeld worden. • p: toestand s moet gelabeld worden met p als en slechts als L(s) = p. • ¬φ: toestand s moet met ¬φ gelabeld worden als en slechts dan als s niet met φ werd gelabeld. • φ ∧ χ: toestand s moet met φ ∧ χ gelabeld worden als het al met φ en χ werd gelabeld. • φ ∨ χ: toestand s moet met φ ∨ χ gelabeld worden als het al met φ of χ werd gelabeld. • φ → χ: toestand s moet met φ → χ gelabeld worden als het niet met φ werd gelabeld of als het met χ werd gelabeld. • EXφ: toestand s moet met EXφ gelabeld worden als een van zijn opvolgers met φ gelabeld is. • AXφ: toestand s moet met AXφ gelabeld worden als al zijn opvolgers met φ gelabeld zijn. • EFφ: 1. Als er een toestand s gelabeld is met φ, label hem dan met EFφ. 2. Label elke toestand s met AFφ als er een opvolger van s met EFφ gelabeld is. 3. Herhaal stap 2 tot er niets meer veranderd. • AFφ: 1. Als er een toestand s gelabeld is met φ, label hem dan met AFφ. 2. Label elke toestand s met AFφ als alle opvolgers van s met AFφ gelabeld zijn. 3. Herhaal stap 2 tot er niets meer veranderd. • E[φUχ]: 44

1. Als er een toestand s gelabeld is met χ, label hem dan met E[φUχ]. 2. Label elke toestand s met E[φUχ] als s met φ gelabeld is en er een opvolger van s met E[φUχ] werd gelabeld. 3. Herhaal stap 2 tot er niets meer veranderd. • A[φUχ]: 1. Als er een toestand s gelabeld is met χ, label hem dan met A[φUχ]. 2. Label elke toestand s met A[φUχ] als s met φ gelabeld is en alle opvolgers van s met A[φUχ] werden gelabeld. 3. Herhaal stap 2 tot er niets meer veranderd. • EGφ: 1. Als er een toestand s gelabeld is met φ, label hem dan met EGφ. 2. Verwijder het label EGφ van s als geen enkele opvolger van s met EGφ werd gemarkeerd. 3. Herhaal stap 2 tot er niets meer veranderd. • AGφ: 1. Als er een toestand s gelabeld is met φ, label hem dan met AGφ. 2. Verwijder het label AGφ van s als er een opvolger van s niet met AGφ werd gemarkeerd. 3. Herhaal stap 2 tot er niets meer veranderd. Na het uitvoeren van dit algoritme moeten alle toestanden s die met λ gelabeld zijn terug. Een voorbeeld is te vinden in het boek ’Logic in Computer Science - second edition’ op pagina’s 225-226 en de handouts van A. Weiermann (FOLO2012hfstk8handout.pdf - pagina’s 36-62). Dit algoritme is lineair over de lengte van de formule en kwadratisch over de grootte van het model. Meer precies, stel f het aantal connectieven en in de formule, V het aantal toestanden en E het aantal transities, dan is de complexiteit gelijk aan O(f · V · (V + E)). We kunnen het algoritme nu iets efficiënter maken door EGφ anders aan te pakken: 1. We beperken de graaf van het model tot de toestanden waar φ geldt, we vergeten dus even alle andere toestanden en bijbehorende toestandsovervangen en bekomen zo: • S 0 := {s ∈ S : M, s |= φ} • →0 := {(s, t); s → t en s, t ∈ S 0 } 2. Zoek de maximaal sterk samenhangende componenten of Strongly Connected Components (SCC’s) van (S 0 , →0 ). Dit zijn de plaatsen in de graaf waarin elke toestand gelinked is (= heeft een eindig pad naar) elke andere toestand in die graaf. 3. Markeer alle toestanden in deze SCC’s met EGφ. 4. Markeer alle toestanden in (S 0 , →0 ) van waaruit een SCC bereikbaar is met EGφ. 45

Hierdoor wordt de complexiteit van het algoritme gelijk aan O(f · (V + E)) of met andere woorden lineair voor zowel de lengte van de formule als de grootte van het model. We bekijken nu een hele andere aanpak van model checking omwille van volgende redenen • Een model kan een niet realistisch of nooit voorkomend gedrag vertonen. • Sommige gedrag is niet in CTL uit te drukken. Zo kunnen we niet uitdrukken dat dat iets binnen een eindige tijd uit een bepaalde toestand zal geraken. Deze problemen lossen we op door fairnessvoorwaarden te veronderstellen en het model checking algoritme enkel naar faire paden te laten kijken. Definitie 27. Een pad s1 → s2 → · · · heet fair tegenover een verzameling C = {ψ1 , ψ2 , . . . , ψn } van fairnessvoorwaarden als sj |= ψi

∀i voor oneindig vele j

We schrijven nu ook AC en EC om aan te duiden dat respectievelijk A en E zich beperken tot de faire paden opgelegd door de fairnessvoorwaarden C. Op deze manier kunnen we volgende equivalenties aantonen: • EC [φUψ] ≡ E[φU(ψ ∧ EC G>)] • EC Xφ ≡ EX(φ ∧ EC G>) We kunnen, indien er fairnessvoorwaarden C beschikbaar zijn, de efficiënte aanpak voor EC Gφ herschrijven: 1. Beperk de graaf tot alle toestanden waarin φ geldt. 2. Bereken de niet triviale SCC’s. 3. Verwijder SCC S als er een voorwaarde ψ ∈ C bestaat waarvoor ∀s ∈ S : s 6|= ψ. 4. Label alle toestanden in de resulterende SCC’s (de faire SCC’s). 5. Bereken en label alle toestanden van waaruit een faire SCC kan worden bereikt. Fairness gaat enkel op voor CTL, in LTL is het mogelijk om deze voorwaarden meteen in de formule zelf uit te drukken.

3.4

Karakterisering van CTL via vaste punten

We noteren vanaf nu JφK voor alle toestanden s ∈ S van M = (S, →, L) waarvoor geldt dat M, s |= φ. Er wordt een volledige bewijstheorie voor het labelend algoritme opgesteld welke te uitgebreid is om in deze cursus te beschrijven. Meer informatie staat in ’Logic in Computer Science - second edition’ pagina’s 239-245.

46

3.5

CTL* en de vergelijking met CTL en LTL

Voor verschillende formules zijn verschillende formuleringen noodzakelijk. Zo kan de LTL formule Fp → Fq, elk pad met een p heeft ook een q, niet in CTL worden uitgedrukt. Omgekeerd kunnen ook heel wat CTL formules niet in LTL worden uitgedrukt. Daarom werdt CTL* ingevoerd die de expressieve kracht van zowel CTL als LTL combineert. Eigenlijk is CTL* gelijk aan CTL maar dan zonder de voorwaarde dat bij elk connectief een A of E moet staan. De syntax wordt nu door twee soorten formules gevormd: • Toestandsformules: φ ::= > | p | (¬φ) | (φ ∧ φ) | A[α] | E[α] waarbij p een atomaire formule is en α gelijk welke padformule • Padformules: α ::= φ | (¬α) | (α ∧ α) | (αUα) | (Gα) | (Fα) | (Xα) waarbij φ gelijk welke toestandsformule is. De prioriteitsregels zijn net dezelfde als voor CTL en/of LTL. Het is gemakkelijk in te zien dat CTL ⊆ CTL* en LTL ⊆ CTL* en dus alles wat in CTL/LTL kan worden uitgedrukt kan ook in CTL* worden uitgedrukt. Voor CTL is dit letterlijk het zelfde. Voor een LTL formule φ kunnen we echter stellen dat A[φ] dezelfde formule is maar dan in CTL* uitgedrukt. Er zijn verschillende voorbeelden te vinden in ’Logic in Computer Science - second edition’ pagina’s 219-220.

4

Modale logica en agenten

In de modale logica kan een formule enkel waar of vals zijn en niets anders. In modale logica worden echter verschillende waarheismodes mogelijk zoals ’dat moet waar zijn’, ’het wordt waar geacht’, ... We kunnen de temporele logica (LTL, CTL) dus zien als een speciaal geval van modale logica omdat we kunnen specifiëren in welke toekomst iets al dan niet waar is.

4.1

Begrippen en notaties van basis modale logica

De syntax van de modale logica is gelijk aan die van de propositionele logica met twee extra connectieven en ♦. Dit zijn net zoals de negatie unaire connectieven. De syntax van basis modale logica is dus te volgende: φ ::=⊥ | > | p | (¬φ) | (φ ∧ φ) | (φ ∨ φ) | (φ → φ) | (φ ↔ φ) | (φ) | (♦φ) waarin p een atomaire formule is. De precedentieregels zijn de volgende: 1. ¬, , ♦ 2. ∧, ∨ 3. →, ↔ 47

Het propositielogica-model waarbij we aan elke atomaire formule een waarheidswaarde toekennen is ontoerijkend voor modale logica omdat we verschillende modes van waarheid moeten kunnen weergeven. Daarom voeren we Kripke modellen in, zo’n model M wordt gespecifieerd door: 1. Een verzameling W van werelden. 2. Een toegankelijkheidsrelatie R ⊆ W × W . 3. Een labelfunctie L → (P )(Atoms). We moeten hierbij w, w0 ∈ W lezen als w en w0 zijn werelden en R(w, w0 ) wil zeggen dat w0 bereikbaar is vanuit w. We geven nu een grafische voorstelling van bijvoorbeeld volgend Kripke model M: • W = {w1 , w2 , w3 , w4 , w5 , w6 } • R = {(w1 , w2 ), (w1 , w3 ), (w2 , w2 ), (w2 , w3 ), (w3 , w2 ), (w4 , w5 ), (w5 , w4 ), (w5 , w6 )} • L = {(w1 , {q}), (w2 , {p, q}), (w3 , {p}), (w4 , {q}), (w5 , ∅), (w6 , {p})} De grafische voorstelling voor bovenstaand model wordt nu weergegeven in figuur 2. Stel w2 p, q

w4

w1

w3

q

p w5

q

w6 p

Figuur 2: Een grafische voorstelling voor M nu M = (W, R, L) een model en x ∈ W een wereld. Als φ een formule is dan wordt de waarheidswaarde van φ in x als volgt met structurele inductie (=inductie op de parsetree) voorgestelt: • x > • x 6 ⊥ • x p als p ∈ L(x) • x ¬φ als x 6 φ • x φ ∧ ψ als x φ en x ψ • x φ ∨ ψ als x φ of x ψ 48

• x φ → ψ als x ψ van zodra x φ • x φ ↔ ψ als x φ als en slechts als x ψ • x φ als ∀y ∈ W waarvoor R(x, y) geldt dat y φ • x ♦φ als ∃y ∈ W waarvoor R(x, y) geldt dat y φ Met de uitspraak ’x φ houdt steek’ bedoelen we dus dat φ waar ix in wereld x. We kunnen M, x φ schrijven om te benadrukken over welk model het gaat. Meer specifiek kunnen we de en ♦ operatoren als volgt interpreteren: • φ: dit is waar als φ waar is in alle werelden die we kunnen bereiken vanuit wereld x. We merken op dat x ⊥ enkel waar is als er geen toegankelijke werelden zijn vanuit x. • ♦φ: dit is waar als φ waar is in een wereld die we kunnen bereiken vanuit wereld x. We merken op dat x ♦> enkel waar is als er tenminste één toegankelijke wereld is vanuit x. We kunnen de interpretatie van en ♦ met die van AX en EX uit CTL vergelijken. We bekijken nu enkele voorbeelden op het model voorgesteld in figuur 2: • w1 q omdat q ∈ L(w1 ). • w1 ♦q omdat er een wereld waarin q waar is toegangkelijk is vanuit w1 , namelijk w2 . Meer wiskundig is het waar omdat R(w1 , w2 ) en w2 q. • w1 6 q omdat niet alle werelden die bereikbaar zijn vanuit w1 (dus wereld w2 en w3 ), q bevatten. • w5 6 p en w5 6 q en w5 6 p ∨ q maar wel w5 (p ∨ q). Dit omdat vanuit w5 de toegankelijke werelden w4 en w6 zijn. Aangezien w4 6 p volgt dat w5 6 p en aangezien w6 6 q volgt dat w5 6 q. Deze twee argumenten samen geven meteen dat w5 6 p∨q. Maar w5 (p∨q) geldt wel omdat we p of q in alle bereikbare werelden vinden. • De werelden die voldoen aan p → p zijn w2 , w3 , w4 , w5 , w6 . Voor w2 , w3 en w6 is dit het geval omdat ze zelf aan p voldoen. Voor w4 is dit juist omdat deze wereld niet aan p voldoet (er geldt R(w4 , w5 ) en w5 voldoet niet aan p). De redenering voor w5 is analoog. Wereld w1 voldoet niet aan de uitspraak p → p omdat de wereld aan p voldoet maar zelf geen p bevat. Definitie 28. Een formuleschema is een algemene vorm van een formule. We zeggen dat een wereld en/of model aan een formuleschema voldoet als alle instanties van dat schema aan het model voldoen. Een instatie bekomt men door voor elke φ een geldige formule in te vullen. Een voorbeeld van een formuleschema is φ → ♦p waarvan p → ♦q een instantie is. Deze instantiatie wil zeggen dat als p waar is, dan in elke mogelijke wereld y die vanuit p bereikbaar is, moet gelden dat ♦q. Dit wil dan weer zeggen dat vanuit elke mogelijke wereld y er een z moet zijn, bereikbaar vanuit y, waarin q waar wordt.

49

Definitie 29. We zeggen dat een verzameling formules Γ een semantisch gevolg is van de formule ψ als geldt dat in elke wereld w van gelijk welk Kripke model M = (W, R, L) geldt dat w ψ van zodra w φ, ∀φ ∈ Γ. We noteren dit met Γ |= ψ We zeggen dat twee formules φ en ψ semantisch equivalent zijn (φ ≡ ψ) als φ ψ en ψ φ. Het is belangrijk te weten dat elke equivalentie in de propositionele logica ook een equivalentie is in de modale logica. Dit geldt ook indien men een substitutie uitvoert. Stel bijvoorbeeld de equivalente formules p → ¬q en ¬(p ∧ q) en voer volgende substitutie uit: p 7→ p ∧ (q → p) q 7→ r → ♦(q ∨ p) Met als resultaat p ∧ (q → p) → ¬(r → ♦(q ∨ p)) ¬((p ∧ (q → p)) ∧ (r → ♦(q ∨ p))) welke in de modale logica ook equivalent zijn. Zo gelden ook volgende wetten voor en ♦: • De wetten van de Morgan: – ¬φ ≡ ♦¬φ – ¬♦φ ≡ ¬φ • De distributiviteitswetten: – (φ ∧ ψ) ≡ φ ∧ ψ – ♦(φ ∨ ψ) ≡ ♦φ ∨ ♦ψ • Overige wetten: – > ≡ > 6≡ ♦T – ♦ ⊥≡⊥6≡ ⊥ – ♦> ≡ p → ♦p Definitie 30. Een formule φ is valide of geldig als ze waar is in elke wereld van elk model. We noteren dit met |= φ. Hieruit volgt, met de substitutieregels, dat elke propositionele tautologie een geldige formule is. We bewijzen nu dat volgende formuleschema’s geldig zijn: • ¬φ ↔ ♦¬φ • (φ ∧ ψ) ↔ φ ∧ ψ • ♦(φ ∨ ψ) ↔ ♦φ ∨ ♦ψ K (φ → ψ) ∧ φ → ψ ≡ (φ → ψ) → (φ → ψ) Bewijs voor formule 1: stel x een model M = (W, R, L), we moeten nu aantonen dat x ¬φ ↔ ♦¬φ en dus dat x ¬φ als x ♦¬φ. We krijgen nu dat x ¬φ: 50

als het niet het geval is dat x φ. ⇔ als het niet het geval is dat ∀y waarvoor R(x, y) en y φ gelden. ⇔ als ∃y waarvoor R(x, y) en ¬y φ gelden. ⇔ als ∃y waarvoor R(x, y) en y ¬φ gelden. ⇔ als x ♦¬φ Waarmee het gestelde bewezen is. De bewijzen voor de andere twee formules zijn analoog. De laatste formule wordt meestal met K aangeduidt (afkomstig van Kripke). Om aan te tonen dat K geldt stellen we weer een wereld x in een model M = (W, R, L). We nemen aan dat x (φ → ψ) ∧ φ en bewijzen dat x ψ. x (φ → ψ) ∧ φ als x (φ → ψ) en x φ ⇔ als ∀y met R(x, y) geldt dat y φ → ψ en y φ impliceert dat ∀y met R(x, y) er geldt dat y ψ ⇔ x ψ Alle andere formules kunnen afgeleid worden uit de voorgaande en dit is dus een soort van volledigheidsresultaat.

4.2

Logische engineering en correspondentietheorie

Met logische engineering of logisch knutselen wordt het ontwerpen van logica om in nieuwe applicaties te gebruiken. Dit is echter heel breed en we beperken ons hier tot het betekenis geven van modale logica. We weten dat ¬¬ equivalent is met ♦ en we kunnen dus volgende betekenissen aan beide operatoren geven: φ Het is zeker waar dat φ Het zal altijd waar zijn dat φ Het moet waar zijn dat φ Agent Q gelooft dat φ Agent Q weet dat φ Na elke uitvoering van programma P , geldt φ

♦φ Het is mogelijks waar dat φ Ergens in de toekomst is waar dat φ Het is toegestaan waar te zijn dat φ φ is consistent met wat agent Q gelooft. Met alles dat Q weet, geldt φ Na enkele uitvoeringen van programma P , geldt φ

Naarmate en ♦ op een andere manier ge¨ınterpreteerd worden zullen er ook andere formules geldig zijn. In de wereld op figuur 2 was p → p bijvoorbeeld niet geldig. Als we echter als een ’noodzaak’ gaan interpreteren wordt die uitspraak per definitie waar. Want p → p wil dan zeggen ’Uit p is noodzakelijk waar volgt dat p waar is’ wat uiteraard altijd klopt. We moeten dus afspraken maken over hoe we de dingen gaan interpreteren. In het boek ’Logic in Computer Science - second edition’ wordt hier op pagina’s 318-322 dieper op ingegaan. Definitie 31. Een frame F = (W, R) is een model zonder de labelfunctie. Een frame voldoet aan een formule als voor elke mogelijke labelfunctie L : W → P(Atoms) en voor elke mogelijke wereld w ∈ W , het zo gevormde model aan die formule voldoet. 51

We kunnen nu aantonen dat als een frame F aan een formule voldoet, dat het frame dan ook aan elke substitutie-instantie van die formule voldoet. Met andere woorden kan een frame aan een formuleschema voldoen en op deze manier worden de twee abstracties samengebracht. w5

w5

w5

Figuur 3: Een grafische voorstelling van een frame We geven nu enkele voorbeelden omtrent het frame in figuur 3 • F voldoet aan de formule p → p. Dit is juist omwille van volgende redenering. Stel w gelijk welke wereld en stel dat x p, we moeten nu aantonen dat x p. We weten dat R(w, w) omdat w bereikbaar is vanuit zichzelf in de figuur. Dus volgt het te bewijzen meteen uit de defintie van . • Het frame voldoet nu aan elke vorm van deze formule en dus aan het formuleschema φ → φ. • Het frame voldoet niet aan de formule p → p. Een tegenvoorbeeld wordt gegeven in figuur 4 waar w4 p maar w4 6 p. w5

w5

w5

p

p

p

Figuur 4: Een model gebaseerd op het frame uit figuur 3 Stelling 5. Stel F = (W, R) een frame, dan zijn de volgende stellingen equivalent: 1.

• R is reflexief • F voldoet aan φ → φ • F voldoet aan p → p

2.

• R is transitief • F voldoet aan φ → φ • F voldoet aan p → p

We bewijzen deel 1 en twee appart en het bewijs van elk van de delen bestaat uit 3 dingen: (a) Indien R de eigenschap bezit dan moet voldoet het frame aan het formule schema. (b) Indien het frame aan het formuleschema voldoet, voldoet het aan een instantie ervan. 52

(c) Indien het frame aan een formule-instantie voldoet heeft R de eigenschap. Bewijs: 1. (a) Stel dat R reflexief is en dat L een labelende functie is, dan is M = (W, R, L) een model voor basis modale logica. We moeten aantonen dat M |= φ → φ en dus dat w φ → φ, ∀w ∈ W . We kiezen nu gelijk welke w en veronderstellen dat w φ. Aangezien R(x, x) volgt uit de regel voor meteen dat w p en dus geldt w φ → φ. (b) We stellen φ gelijk aan p. (c) Stel dat het frame aan p → p voldoet. We tonen nu aan dat voor een willekeurige wereld w, R(w, w) geldt. Veronderstel een labelende functie L zodat p 6∈ L(w) en p ∈ L(y) voor alle werelden y behalve w. We bewijzen met contradictie. Stel dat er geen zo’n R(w, w) bestaat, dan geldt w p aangezien alle werelden die bereikbaar zijn vanuit w aan p voldoen (dit is omdat alle werelden behalve w aan p voldoen). Aangezien F echter aan p → p voldoet volgt dat x |= p → p en dus verkrijgen we uit x p en x p → p samen dat x p. Dit is tegenstrijdig met het feit dat we geen R(x, x) hebben omdat we gezegd hadden dat p 6∈ L(x) is. Hieruit volgt dat R(x, x) in het frame moet zitten. 2. (a) Stel dat R transitief is en dat L een labelende functie is, dan is M = (W, R, L) een model voor basis modale logica.We moeten aantonen dat M φ → φ en du moeten we aantonen dat voor gelijk welke w ∈ W geldt dat w φ → φ. Stel nu dat w φ, dan moeten we nog aantonen dat x φ. Uit de regel voor volgt dan dat gelijk welke y waarvoor R(w, y) geldt aan φ moet voldoen. Er moet dus gelden dat voor gelijk welke w, z met R(w, y) en R(y, z) er moet gelden dat z φ. Veronderstel nu dat er zo’n y, z met R(w, y) en R(y, z) bestaan. Wegens het feit dat R transitief is verkrijgen we R(w, z). We veronderstelden echter dat x φ en we verkrijgen, wegens de betekenis van , dat z φ en dus is het gestelde bewezen. (b) We stellen φ gelijk aan p. (c) Stel dat het frame aan p → p voldoet. Neem nu een willekeurige x, y, z met R(x, y) en R(y, z), we tonen dan aan dat R(x, z) geldt. Definieer een labelende functie L zodanig dat p 6∈ L(z) en p ∈ L(w) foor alle werelden w uitgezonderd z. Stel dat er geen R(x, z) bestaat, dan x p aangezien w p voor alle w 6= z. Uit het axioma p → p volgt dan dat x p. Dus y |= p aangezien R(x, y) bestaat. Dit laatste resultaat en R(y, z) maken van z p een contradictie en dus moet R(x, z) bestaan. De correspondentie in de correspondentietheorie duidt dus op het feit dat een formuleschema en een eigenschap van de toegangkelijkheidsrelatie met elkaar corresponderen. Het basisidee is dus hat het eisen dat bepaalde formules/formuleschema’s waar zijn gelijk staat met het eisen dat een toegangkelijkheidsrelatie een bepaalde eigenschap heeft. Een overzicht wordt in volgende tabel weergegeven:

53

naam T B D 4 5

formuleschema φ → φ φ → ♦φ φ → ♦φ φ → φ ♦φ → ♦φ φ ↔ ♦φ (φ ∧ φ → ψ) ∨ (ψ ∧ ψ → φ)

eigenschap van R reflexiviteit symmetrie serialiteit transitiviteit Euclidiciteit functionaliteit voorwaartse lineairiteit

In wat volgt zullen we enkele soorten modale logica bespreken, deze worden gedefinieerd door een set L van formuleschema’s te kiezen. Definitie 32. Stel L een verzameling van formuleschema’s en Γ ∪ {ψ} een verzameling formules, dan: 1. De verzameling Γ is gesloten onder de substitutieinstanties. Van zodra φ ∈ Γ zit ook elke substitutieinstantie van φ in Γ. 2. We schrijven Lc voor de kleinste verzameling die alle instanties van alle formuleschema’s van L bevat. 3. Γ voldoet semantisch aan ψ in L als in elk model waar alle formules van Γ en Lc voldaan zijn, ook aan de formule ψ voldaan is. We noteren met: Γ |=L ψ We merken op dat zeggen dat alle formules van Lc voldaan zijn, het zelfde is als zeggen dat we ons beperken tot die modellen waar de relatie R aan de overeenkomstige eigenschappen voldoet. Volgende zijn voorbeelden van enkel modale logica’s: • De modale logica K: dit is de zwakste modale logica en en heeft geen gekozen formuleschemas en dus L = ∅. Er worden dus geen bijkomende eisen aan R opgelegd. Deze modale logica voldoet dus aan alle instanties van de formule K. Modale logica’s die deze eigenschap bezitten worden normaal genoemd. Alle logica’s die we bespreken zijn normaal. • De modale logica KT45: ook wel S5 genaamd. Hier is L = {T, 4, 5} met T, 4, 5 de formules uit bovenstaande tabel. We eisen hiermee dat R een equivalentierelatie is. Deze logica wordt gebruikt om over kennis te redeneren en dus betekend φ hier dat ’agent Q weet dat φ’. We verkrijgen dus: – Waarheid: agent Q weet enkel ware dingen. – Positieve introspectie: als agent Q iets weet, dan weet agent Q dat hij het weet. – Negatieve introspectie: als agent Q iets niet weet, dan weet agent Q dat hij het niet weet. • De modale logica KT4: ook wel S4 genaamd. Hier is L = {T, 4}. We eisen hiermee dat R reflexief en transitief is. Deze logica is vooral handig bij het redeneren over partiële evaluatie van code.

54

4.3

Natuurlijke deductie

Het rechtstreeks bewijzen van Γ |=L ψ vanuit de semantiek is zeer lastig. Daarom voeren we een geschikt systeem van natuurlijke deductie of bewijsleer in. Dit is een uitbreiding van de bewijsleer voor propositielogica. We voren een nieuwe soort bewijsbox in, aangeduidt met gestippelde lijnen. Daarin redeneren we in een willekeurig toegangkelijke wereld. We voeren ook twee nieuwe bewijsregels in, namelijk i en e. Bewijsbaarheid in K noteren we met `K en we stellen vast dat dit systeem sterk genoeg is om alle stellingen uit K te bewijzen. De nieuwe bewijsregels zijn de volgende: .. . φ φ

φ

i

.. . φ .. .

e

De gewone bewijsboxen en gestippelde bewijsboxen mogen genest voorkomen. Er zijn geen expliciete regels voor ♦ welke we dus als ¬¬ moeten noteren. Voor KT45 modale logica komen hier enkele uitbreidingen bij. Deze komen overeen met de regels T, 4 en 5: φ φ

T

φ φ

4

¬φ ¬φ

5

In het boek ’Logic in Computer Science - second edition’ staan op pagina’s 330-331 enkele uitgewerkte voorbeelden.

4.4

Redeneren over kennis in een multi-agentensysteem

Een een multi-agentensysteem hebben verschillende agenten verschillende kennis over de wereld. Als men over kennis redeneert, redeneert men niet alleen over de feiten in de wereld, maar ook over de kennis van andere agenten in de groep. Indien men enkele voorbeelden bekijkt dan ziet men dat er nood is aan meerdere modaliteiten. In plaats van één te hebben, maken we er nu veel, namelijk éénper agent i. Definitie 33. Gegeven een verzameling A = {1, 2, . . . , n} van agenten, we noteren met Ki met i ∈ A dat agent i weet dat φ waar is (de K duidt aan dat het om kennis gaat). Stel nu G = {i1 , . . . , im } een deelverzameling van A, dan zijn er volgende connectoren: • Ki φ: agent i weet dat φ • EG φ: alle agenten uit de verzameling G weten dat φ, en dus equivalent met Ki1 φ ∧ · · · ∧ Kim φ. • CG φ: alle agenten uit de verzameling G weten dat φ en ze weten dat ze dat weten, .... Dit is equivalent met de oneindige conjunctie EG φ∧EG EG φ∧· · · (Common knowledge). • DG φ: de kennis van φ kan afgeleid worden wanneer de agenten uit G hun kennis samenleggen. (Distributed knowledge) 55

Deze logica noemen we KT45n . Wat betreft de precedentieregels kunnen we de extra connectieven allemaal dezelfde prioriteit geven als . Als we dus A als een verzameling van agenten zien en G ⊆ A en i ∈ A dan voldoet een goed-gevormde KT45n formule aan volgende grammatica: φ ::=⊥ | > | p | (¬φ) | (φ ∧ φ) | (φ ∨ φ) | (φ → φ) | (φ ↔ φ) | (Ki φ) | EG φ) | (CG φ) | (DG φ) We schrijven E voor EA , C voor CA en D voor DA . Definitie 34. Een model M = (W, (Ri )i∈A , L) van de multimodale logica KT45n met een verzameling A van n agenten wordt vastgelegd door 3 dingen: 1. Een verzameling W van werelden. 2. ∀i ∈ A een equivalentierelatie Ri over W (Ri ⊆ W × W ). Dus een verzameling van toegankelijkheidsrelaties. 3. een labelende functie L : W → P(Atoms) De grafische voorstelling lijkt goed op die voor basis modale logica. Echter zijn alle links symmetrisch en dus worden geen pijlen meer getekend. Ook worden de voorstellingen voor 1 agent gemaakt, dus verschillende voorstellingen voor KT451 , KT452 , ... Dit is zo omdat elke relatie een equivalentierelatie is daar we kennis willen modelleren. Stel een model M = (W, (Ri )i∈A , L) van KT45n en een wereld x ∈ W . Wanneer φ waar is in x wordt via een voldoeningsrelatie x φ via inductie op φ gedefinierd: • x p als p ∈ L(x) • x ¬φ als x 6 φ • x φ ∧ ψ als x φ en x ψ • x φ ∨ ψ als x φ of x ψ • x φ → ψ als x ψ van zodra x φ • x Ki ψ als ∀y ∈ W waarvoor Ri (x, y) bestaat geldt y ψ • x EG ψ als ∀i ∈ G geldt dat x Ki ψ k ψ. Hierbij betekent E k E E . . . E k keer • x CG ψ als ∀k ∈ N ≥ 1 geldt dat x EG G G G G na elkaar

• x DG ψ als ∀y ∈ W waarvoor Ri (x, y), ∀i ∈ G geldt dat y ψ. Elke Ki gedraagt zich dus als een met betrekking tot Ri . Er zijn geen equivalenties met ♦, maar je kan deze bekomen door ¬Ki ¬ uit te drukken. Samenvattend is een frame F voor KT45n (W, (Ri )i∈A ) een verzameling W van werelden met voor elk van die werelden een equivalentierelatie Ri over W . Er wordt gezegt dat een frame F aan φ voldoet als voor elke labelende functie L : W → P(Atoms) en elke wereld w ∈ W geldt dat M, w φ steek houdt. We zeggen dan dat F |= φ steek houdt.

56

Stelling 6. Er geldt dat: k φ als voor alle y die in k stappen G-bereikbaar zijn, voldoen aan y φ. 1. x EG

2. x CG φ als voor alle y die G-bereikbaar zijn, voldoen aan y φ We zeggen dat y G-bereikbaar is in k stappen van x als er een w1 , w2 , . . . , wk−1 ∈ W zijn en een i1 , i2 , . . . , ik ∈ G zodat xRi1 w1 Ri2 w2 · · · Rik−1 wk−1 Rik y waarmee Ri1 (x, w1 ), Ri2 (w1 , w2 ), . . . , Rik (wk , y) mee wordt bedoeld. We bewijzen nu de stelling: Stel dat y φ∀y G-bereikbaar vanaf x in k stappen. We bewijk φ steek houdt. Het volstaat aan te tonen dat x K , K , . . . , K φ voor zen nu dat x EG i1 i2 ik gelijk welke i1 , i2 , . . . , ik ∈ G. Neem nu een willekeurige i1 , i2 , . . . , ik ∈ G en een willekeurige w1 , w2 , . . . , wk−1 en willekeurige y zodat er een pad van de vorm xRi1 w1 Ri2 w2 · · · Rik−1 wk−1 Rik y bestaat. Aangezien y G-bereikbaar is vanuit x in k stappen geldt dat y φ wegens onze aanname en dus geldt x Ki1 , Ki2 , . . . , Kik φ zoals nodig was. k φ en dat y G-bereikbaar is vanuit x in k stappen. We Tegenovergesteld, veronderstel x EG j φ moeten dan aantonen dat y φ steek houdt. Neem i1 , i2 , . . . , ik ∈ G, aangezien x EG geldt volgt dat x Ki1 , Ki2 , . . . , Kik φ en dus dat y φ. Het bewijs voor deel 2 is analoog. We lijsten nu nog enkele geldige formules voor KT45n logica op. De formule K houdt steek voor de connectieven Ki , EG , CG en DG waardoor we dus volgende formuleschema’s verkrijgen: • Ki φ ∧ Ki (φ → ψ) → Ki ψ • EG φ ∧ EG (φ → ψ) → EG ψ • CG φ ∧ CG (φ → ψ) → CG ψ • DG φ ∧ DG (φ → ψ) → DG ψ Deze formules betekenen dat verschillende niveau’s van kennis gesloten zijn onder logisch gevolg. Als bepaalde feiten bijvoorbeeld ’common knowledge’ zijn en andere feiten volgen hier letterlijk uit, dan zijn die andere feiten ook common knowledge. We merken ook op dat E, C en D zich als een gedragen omdat ze universeel over verschillende toegankelijkheidsrelaties handelen. We kunnen hierdoor de relaties REG , RDG en RCG in termen van de relaties Ri invoeren: • REG (x, y) als Ri (x, y) voor sommige i ∈ G • RDG (x, y) als Ri (x, y) voor alle i ∈ G k (x, y) voor elke k ≥ 1 • RCG (x, y) als RE G

Aangezien Ri de equivalentirelaties zijn in multi-modale logica, blijven ook volgende regels van kracht: • Ki φ → Ki Ki φ: positieve introspectie

57

• ¬Ki φ → Ki ¬Ki φ: negatieve introspectie • Ki φ → φ: waarheid Deze formules gelden ook voor DG en CG aangezien RDG en RCG equivelantierelaties zijn. Dit is echter niet het geval voor EG omdat REG niet noodzakelijk een equivalentierelatie is. Maar REG is wel reflexief, dus de formule EG φ → φ is geldig op voorwaarde dat G 6= ∅. Deze laatste vereiste is ook nodig opdat CG φ → φ zou gelden omdat deze formules anders altijd waar zouden zijn.

4.5

Natuurlijke deductie

De regels voor KT45n zijn een kleine uitbreiding van de regels voor KT45. Ze zijn analoog met volgende toevoegingen: • Er zijn verschillende soorten gestippelde kaders voor de verschillende soorten modale connectieven. De modaliteit wordt links bovenaan in een hoek van de gestippelde box aangegeven. • De axioma’s T, 4 en 5 kunnen voor elke Ki gebruikt worden. Axioma’s 4 en 5 kunnen ook voor CG gebruikt worden maar niet voor EG . De bewijsregels voor KT45n worden als volgt samengevat: Ki

EG

.. . φ Ki φ

Ki φ Ki

Ki i

EG

CG φ i j ∈ G K i1 · · · K ik φ

KT

EG i

EG φ

.. . φ .. .

Ki φ voor elke i ∈ G EG φ

.. . φ

EG φ

Ki e

Ki φ φ

CG

.. . φ

KE

CK

CG φ

EG e

.. . φ .. .

CG φ CG CG φ Ki φ Ki Ki φ

K4

C4

CG e

.. . φ .. .

CG

EG φ i ∈ G Ki φ

CG i

CG φ

CG φ EG · · · EG φ

EKi

¬CG φ CG ¬CG φ ¬Ki φ Ki ¬Ki φ

CE

C5

K5

Een intu¨ıtieve manier om over de gestippelde boxen te denken is de volgende, als je zo’n box Ki opent, dan redeneer je over wat agent i weet. Een gewone formule φ kan dus niet zomaar 58

in zo’n box gebracht worden omdat je niet weet of agent i die kent. Zo kan men de regel ¬i niet gebruiken als een van de premissen van de regel buiten de box is waarin je werkt. In het boek ’Logic in Computer Science - second edition’ op pagina’s 341-350 staan twee uitgebreide voorbeelden.

5

Binaire beslissingsdiagramma’s

5.1

Voorstellen van booleanse functies

Booleaanse functies zijn heel belangrijk om hard- en softwaresystemen te beschrijven en er moet dus een goede manier gevonden worden om ze voor te stellen. Definitie 35. Een booleaanse variabele x is een variabele die de waarden 0 en 1 kan aannemen. We noteren ze met x1 , x2 , . . . en x, y, z, . . .. We geven de volgende functies aan de verzameling {0, 1}: def

def

• (complement) x = 1 en 1 = 0 def

def

• (product) x · y = 1 als x en y waarde 1 hebben, anders x · y = 0 def

def

• (som) x + y = 0 als x en y waarde 0 hebben, anders x + y = 1 def

• (xor of exclusieve of ) x ⊕ y = 1 als x of y maar niet beide 1 zijn. Definitie 36. Een booleaanse functie f met n argumenten is een functie van {0, 1}n naar {0, 1}. We schrijven f (x1 , x2 , . . . , xn ) of f (V ) om aan te duiden dat een syntactische voorstelling van f enkel op de booleaanse variabelen in V duiden. Propositionele formules en waarheidstabellen zijn beide verschillende representaties van booleaanse functies. In propositionele formules gelden dan volgende ’mappings’: • ∧ 7→ ·

• > 7→ 1

• ∨ 7→ +

• ⊥7→ 0

• ¬ 7→ x

• (φ ∧ ¬ψ) ∨ (¬φ ∧ ψ) 7→ φ ⊕ ψ

Booleaanse functies worden op de meest logische manier in waarheidstabellen weergegeven. Onderstaand heb je de voorstelling voor φ = ¬(p ∨ q) of dus f (x, y) = (x + y): x 1 0 1 0

y 1 1 0 0

f (x, y) 0 0 0 1

p T F T F

q T T F F

φ F F F T

Definitie 37. Een disjunctieve normaalvorm is een disjunctie van conjuncties van literalen

59

We kunnen dus verschillende voorstellingen maken van booleaanse functies, in waarheidstabellen, in propositionele formules, in conjunctieve normaalvorm, in disjunctieve normaalvorm. Echter hebben vele van deze voorstellingen grote nadelen, of ze zijn heel lang, of ze zijn niet te controleren op vervulbaarheid. Daarom voeren we gereduceerde OBDD’s of gereduceerde Ordered Binary Decision Diagrams in. Volgende tabel geeft een overzicht over welke voor- en nadelen een bepaalde representatie heeft:

Representatie Propositionele formules Formules in DNV Formules in CNV Geordende waarheidstabellen Gereduceerde OBDD’s

compact? vaak

testen op vervulbaarheid geldigheid moeilijk moeilijk

booleaanse operaties · + x makkelijk makkelijk makkelijk

soms soms nooit

makkelijk moeilijk moeilijk

moeilijk makkelijk moeilijk

moeilijk makkelijk moeilijk

makkelijk moeilijk moeilijk

moeilijk moeilijk moeilijk

vaak

makkelijk

makkelijk

gemiddeld

gemiddeld

makkelijk

Binaire beslissingsdiagrammen (BDD’s) zijn een andere manier om booleaanse functies voor te stellen. Ze zijn gebaseerd op binaire beslissingsbomen, dit zijn binaire bomen waarvoor de toppen gelabeld zijn met een booleaanse variabele x, y, z, . . . en de bladeren zijn met 0 of 1 gelabeled. Elke top heeft dus twee kinderen, één met een gestippelde lijn en een andere met een volle lijn. Definitie 38. Stel T een eindige binaire beslissingsboom, dan stelt T een unieke booleaanse functie f voor met als argumenten de variabelen in de toppen van de boom. Als men aan de variabelen een 0 en een 1 toewijst, dan starten we in de wortel van de boom en: • We nemen een gestippelde lijn als de waarde van de variabele 0 is. • We nemen een volle lijn als de waarde van de variabele 1 is. De waarde van de functie f is dan de waarde van het blad waarin we uitkomen. Een binaire beslissingsboom is echter even groot als een waarheidstabel en bieden dus niet echt een compactere manier van voorstellen. Echter is het duidelijk dat er heel wat redundancy in die bomen zit. In een blad kan enkel 0 of 1 staan en dus volstaat het de bomen met 2 bladeren te tekenen. Deze optimalisatie wordt weergegeven in de linker figuur op figuur 5. We hebben nu minder bladeren maar nog steeds evenveel takken. Een tweede optimalisatie x y 1

x y

y

0

1

0

Figuur 5: Twee optimalisaties voor binaire beslissingsbomen

60

bestaat er in om onnodige beslissingspunten uit de boom te verwijderen. In de linkerboom op figuur 5 is de rechter y overbodig omdat die zeker tot 0 leidt. Daarom kan deze worden weggelaten en we bekomen dan de rechterboom. Dit soort structuren worden binaire beslissingsdiagrammen genoemd en zijn duidelijk geen bomen meer, maar veel algemenere grafen. Een derde en laatste optimalisatie bestaat er in om deelBDD’s te delen, stel de bdd in figuur 6. De twee binnenste y-toppen in de boom op figuur 6 hebben de zelfde functie omdat de z

x

x

y

y

y

0

y

1

Figuur 6: een BDD met dubbele deelBDD’s ´ en van de twee kunnen dan verwijderd worden met deelBDD’s die er onder hangen gelijk zijn. E´ als resultaat de linkerboom in figuur 7. Nu zien we dat de meest linkse y-top samengenomen kan worden met de middelste. De x-top boven hen beide wordt dan redundant en kan worden verwijderd. Zo bekomen we de optimale BDD welke rechts staat op figuur 7. z

z

x x

x

y

y

0

y

y

0

1

y

1

Figuur 7: Het twee keer uitvoeren van de derde optimalisatie. We hebben dus 3 optimalisaties: C1: Het verwijderen van dubbele bladeren. C2: Het verwijderen van dubbele beslissingspunten. C3: Het verwijderen van dubbele deelBDD’s. 61

Definitie 39. De majoriteitsfunctie wordt als volgt gedefinieerd: 1 als het meertal van x, y, z1 is. f (x, y, z) = 0 anders Definitie 40. Een binair beslissingsdiagramma of BDD is een eindige gerichte acyclische graaf met een unieke top (de wortel), enkel bladeren gelabeld met 0 of 1 en waarvan alle interne toppen met een booleaanse variabele gelabeled zijn. Elke interne top heeft exact twee én boog is met 0 gelabeled en de andere met 1 en bogen van die top naar een andere top. E´ we stellen deze met een gestippelde en een volle lijn voor. Een BDD noemt gereduceerd als er geen van de voorgaande drie optimalisaties (C1, C2, C3) op kunnen worden uitgevoerd. Ze leggen booleanse variabelen vast net zoals binaire beslissingsbomen dat doen. Het testen gaat nu als volgt: • Vervulbaarheid testen: de BDD stelt een vervulbaare functie voor als er ten minste 1 consistent pad is die naar een 1-blad loopt. Met een consistent pad wordt een pad uit enkel gestreepte of enkel volle lijnen bedoelt per variabele. Dit komt er dus op neer dat we aan een variabele maar é’en waarde kunnen bedelen. • Geldigheid testen: een BDD stelt een geldige functie voor als er geen 0-bladeren bereikbaar zijn vanuit een consistent pad. • De · operatie uitvoeren: stel twee BDD’s Bf en Bg , een BDD die f · g voorstelt wordt verkregen door de BDD voor f te nemen en alle 1-bladeren door Bg te vervangen. • De + operatie uitvoeren: stel twee BDD’s Bf en Bg , een BDD die f + g voorstelt wordt verkregen door de BDD voor f te nemen en alle 0-bladeren door Bg te vervangen. • De inverse BDD zoeken: alle 1-bladeren worden 0-bladeren en omgekeerd De + en · operaties zullen op deze manier BDD’s met meerdere voorkomens van variabelen genereren, later bespreken we een meer geoptimaliseerde manier. Zelfs met de bovenstaande optimalisaties kunnen er nog dubbele voorkomens zijn van variabelen in de boom. Dit lijkt niet echt efficiënt, daarbovenop is er nog geen goede manier om equivalentie te testen. De oplossing bestaat erin om een ordening van de variabelen die voorkomen op een pad in te voeren. We blijven die ordening dan gebruiken voor alle BDD’s die we opstellen/gebruiken. Definitie 41. Stel [x1 , . . . , xn ] = x1 < · · · , xn een ge¨ ordende lijst van variabelen zonder duplicaten en stel B een BDD die al deze variabelen bevat. We zeggen dat B de ordening [x1 , . . . , xn ] = x1 < · · · , xn heeft als alle variabelen voorkomen in B en als voor elk voorkomen van xi gevolgd door xj in gelijk welk pad van B geldt dat i < j, of dus dat xi boven de variabele xj staat. Een geordende BDD of OBDD is dus een BDD welke een ordening heeft voor een lijst van variabelen. Enkele voorbeelden van OBDD’s staan in het boek ’Logic in Computer Science - second edition’ op pagina’s 367-368. Als we nu bewerkingen gaan uitvoeren op OBDD’s dan vereisen we meestal dat ze compatibele variabelenordeningen hebben. Dit is het geval als er geen variabelen x en y bestaan waarvoor x > y in B1 en y > x in B2 . Dus twee compatibele 62

ordeningen zijn bijvoorbeeld [x, y, z] en [x, u, y, z]. Deze voorwaarden zorgen ervoor dat gereduceerde OBDD’s unieke representaties zijn van booleaanse functies. De reducties C1 , C2 en C3 bewaren hierbij de ordening. Stelling 7. Als twee OBDD’s, stel B1 en B2 een compatibele variabelenordening hebben en ze zijn gereduceert, dan zijn ze uniek als en slechts als ze dezelfde booleaanse functie representeren. Het testen van vervulbaarheid, geldigheid en equivalentie wordt op deze manier triviaal voor gereduceerde OBDD’s. De grootte van een OBDD hangt in het algemeen sterk af van de gekozen variabele-ordening, een voorbeeld staat in het boek ’Logic in Computer Science second edition’ op pagina’s 370-371. De optimale ordening vinden is een complex probleem waarvoor heuristieken gebruikt worden. De significantie van de unieke voorstelling (’canonical representation’) van de OBDD’s moet sterk worden benadrukt omdat het toelaat om volgende testen gemakkelijk uit te voeren: • Afwezigheid van redundante variabelen: als de waarde van de booleaanse functie f (x1 , x2 , . . . , xn ) niet afhangt van de waarde van xi dan zal geen enkele gereduceerde OBDD die deze funcite voorstelt een xi -top bevatten. • Test voor semantische equivalentie: als twee functies f (x1 , x2 , . . . , xn ) en g(x1 , x2 , . . . , xn ) voorgesteld worden door OBDD’s Bf en Bg met een compatibele variabelen-ordening, dan kan gemakkelijk beslist worden of beide functies semantisch equivalent zijn. We reducren indien nodig Bf en Bg en controleren of ze een identieke structuur hebben, indien dit zo is zijn beide functies semantisch equivalent. • Test voor geldigheid: een functie f (x1 , x2 , . . . , xn ) is geldig als hij altijd 1 uitkomt. Als we de gereduceerde OBDD voor f opstellen dan is f geldig als deze OBDD’ één blad heeft met waarde 1. • Test voor implicatie: om te testen of een functie f een functie g impliceert, of dus waneer f = 1 dat dan ook g = 1 geldt,moeten we de gereduceerde OBDD voor f · g berekenen. Dit is de constante 0-boom als de implicatie geldt. • Test voor vervulbaarheid: om te controleren of een functie f vervulbaar is, of dus dat er ten minste 1 bedeling bestaat waarvoor f = 1, moet er een gereduceerde OBDD bestaan die niet de constante 0-boom is.

5.2

Algoritmen voor gereduceerde OBDD’s

De reductieregels C1, C2, C3 zijn heel belangrijk om een gereduceerde (O)BDD te berekenen. We beschrijven nu het reduce algoritme wat dit op een efficiënte manier doet. Als de ordening van B gelijk is aan [x1 , x2 , . . . , xl ] dan heeft B maximium l + 1 niveau’s. Het reduce algoritme gaat nu in een bottom-up manier door de boom en kent labels id(n) toe aan elke top in de boom B. De labels worden zo toegekend zodat deelOBDD’s met worteltoppen n en m die de zelfde booleanse functie voorstellen de zelfde labels id(n)=id(m) krijgen.

63

Het algoritme gaat nu als volgt, waarin we lo(n) als kind kind via de gestippelde lijn en hi(n) het kind via de volle lijn bedoelen: 1. Ken #0 toe aan alle bladeren met label 0. 2. Ken #1 toe aan alle bladeren met label 1. 3. In een interne top n met variabele x: (a) als id(lo(n))==id(hi(n)) dan id(n)=id(lo(n)) (b) als er een top m 6= n met dezelfde variabele x bestaat en id(m) en er geldt dat id(lo(n))=id(lo(m)) en id(hi(n))=id(hi(m)), dan stellen we id(n) gelijk aan id(m). (c) anders stellen we id(n) gelijk aan het volgend nog niet gebruikt getal Het algoritme eindig met de reducties C1, C2, C3 toe te passen op een bottom-up manier, dit is een efficiënte operatie. Een andere procedure is het apply algoritme wat wordt gebruikt om operaties op booleanse functies zoals ·, +, ⊕ en complement berekenen (via f ⊕ 1) uit te voeren. Als de OBDD’s Bf en Bg voor booleaanse functies f en g gegeven zijn berekent apply(op, Bf , Bg ) de gereduceerde OBDD van de booleaanse formule ’f op g’. Hierbij is op uiteraard een functie van {0, 1} × {1, 0} 7→ {0, 1}. Het algoritme apply werkt recursief op de structuur van twee OBDD’s: • Stel v de variabele die het eerst voorkomt in de ordening en in zowel Bf als in Bg voorkomt. • Splits het probleem in twee deelproblemen, namelijk voor v = 0 en voor v = 1 en ga zo verder op een recursieve manier. • Indien men in de bladeren komt, pas de booleaanse operatie meteen toe. Het resultaat zal achteraf nog gereduceerd moeten worden om een OBDD te verkrijgen. Definitie 42. Stel f een booleaanse formule en x een variabele, dan: 1. We noteren met f [0/x] de booleaanse formule die wordt verkregen door alle voorkomens van x in f te vervangen door 0. Analoog noteren we met f [1/x] de booleaanse formule die wordt verkregen door alle voorkomens van x in f te vervangen door 1. De uitdrukkingen f [0/x] en f [1/x] worden restricties van f genoemd. 2. We zeggen dat twee booleaanse functies f en g semantisch equivalent zijn als ze dezelfde booleaanse functie voorstellen, we schrijven dan f ≡ g. Het zijn deze restricties die het mogelijk maken om apply recursief te definiëren. Stel namelijk dat x een variabele in de functie f is dan geldt f ≡ x · f [0/x] + x · f [1/x]. Dit resultaat is beter bekend als de Shannon expansie. Lemma 7. (Shannon expansie) Voor alle booleaanse functies f en alle booleaanse variabelen x (zelfs als ze niet in f ) voorkomen geldt: f ≡ x · f [0/x] + x · f [1/x] 64

De apply functie is als volgt op de Shannon expansie voor f op g gebaseerd: f op g = xi · (f [0/xi ] op g[0/xi ]) + xi · (f [1/xi ] op g[1/xi ]) Dit wordt gebruikt als een controlestructuur van apply welke vanaf de wortels van Bf en Bg naar beneden gaat om zo de toppen van de OBDD Bf op g te construeren. Stel rf de wortel van Bf en rg de wortel van Bg : 1. Als zowel rf als rg bladeren zijn met labels lf en lg , waarbij deze labels dus 0 of 1 moeten zijn, dan berekenen we de waarde lf op lg en we noemen de resulterende OBDD B0 als de waarde 0 is en B1 als de waarde 1 is. 2. In de overige gevallen is ten minste één van de toppen geen blad. We hebben nu 3 mogelijkheden: (a) Beide nodes zijn interne toppen xi . We maken nu een xi -top n met een gestippelde lijn naar apply(op, lo(rf ), lo(rg )) en een volle lijn naar apply(op, hi(rf ), hi(rg )). We roepen met andere woorden apply recursief op. (b) Als rf een interne xi -top is en rg een blad of een xj -top met j > i, dan weten we dat er geen xi -top in Bg bestaat. Dit omdat de twee OBDD’s een compatibele ordening van booleaanse variabelen hebben. Er volgt dus dat g onafhankelijk is van xi (g ≡ g[0/xi ] ≡ g[1/xi ]). We maken dus een xi -top n aan met een gestippelde lijn naar apply(op, lo(rf ),rg ) en een volle lijn naar apply(op, hi(rf ), rg ) (c) Als rg een interne xi -top is en rf een blad of een xj -top met j > i, dan weten we dat er geen xi -top in Bf bestaat. Er volgt dus dat f onafhankelijk is van xi (f ≡ f [0/xi ] ≡ f [1/xi ]). We maken dus een xi -top n aan met een gestippelde lijn naar apply(op,rf ,lo(rg )) en een volle lijn naar apply(op, rf , hi(rg )) Het resultaat van de apply procedure is niet noodzakelijk gereduceerd en dus moet op het einde nogmaals de reduce procedure opgeroepen worden. In het boek ’Logic in Computer Science - second edition’ wordt op pagina’s 375-376 een visueel voorbeeld van de apply procedure gegeven. In de handouts van hoofdstuk 7 staat vanaf slide 36 een uitwerkt voorbeeld. Het restrict algoritme opgeroepen als restrict(0, x, Bf ) berekend de gereduceerde OBDD welke f [0/x] voorstelt met dezelfde variabele ordening als Bf . Het algoritme voor restrict(i, x, Bf ) gaat als volgt: 1. Herleid voor alle toppen n die met x gelabeled zijn de inkomende bogen naar: • lo(n) als i = 0 • hi(n) als i = 1 2. Verwijder top n 3. Reduceer het resulterende OBDD Als laatste bespreken we de exists procedure. We kunnen een booleaanse functie zien als een beperking op zijn variabelen. Stel bijvoorbeeld de functie f = x + (y · z), deze is 1 enkel als x = 1, of als y = 0 en z = 1, dit zijn dus beperkingen op x, y, z. We schrijven nu ∃x.f

65

voor f [0/x] + f [1/x] wat wil zeggen dat ∃x.f waar is als f waar gemaakt kan worden door x te vervangen door 0 of 1. Het exists algoritme kan nu worden uitgedrukt in termen van het apply en restrict algoritme: apply(+, restrict(0, x, Bf ), restrict(1, x, Bf )) We kunnen op een gelijkaardige manier een forall functie definiëren aangezien geldt dat def ∀x.f = f [0/x] · f [1/x] en we verkrijgen dus: apply(·, restrict(0, x, Bf ), restrict(1, x, Bf )) In het boek ’Logic in Computer Science - second edition’ worden op pagina’s 378-379 enkele voorbeelden visueel voorgesteld. We kunnen nu een overzicht geven over hoe we booleaanse functies f naar OBDD’s Bf kunnen omzetten indien een ordening gegeven is: Booleaanse fomule f

Methode om OBDD Bf te verkrijgen

0

B0

1

B1

x

Bx

f

verwissel de 0- en 1-toppen in Bf

f +g

apply(+, Bf , Bg )

f ·g

apply(·, Bf , Bg )

f ⊕g

apply(⊕, Bf , Bg )

f [1/g]

restrict(1, x, Bf )

f [0/g]

restrict(0, x, Bf )

∃x.f

apply(+, Bf [0/x] , Bf [1/x] )

∀x.f

apply(·, Bf [0/x] , Bf [1/x] )

Niet alle functies hebben een compact OBDD, op de slides van hoofdstuk 7 vanaf slide 42 staat de Hidden Weighted Bit function gedefinieerd. Ieder gereduceerd OBDD van HW Bn heeft een grootte die exponentieel is in n. Er bestaan echter wel BDD’s die beter zijn.

5.3

Symbolic model checking

Symbolic model checking is het controleren van een model met een (O)BDD. We bespreken een implementatie van het CTL model checking algoritme gegeven op pagina 44, maar dan met OBDD’s als datastructuur. Dit algoritme heeft een CTL formule φ als input en geeft een verzameling toestanden terug die aan φ voldoen. Intern werkt het algoritme ook steeds met een verzameling van overgangsrelaties. We bekijken dus volgende onderdelen: • Hoe stellen we een CTL model voor als OBDD • Hoe kunnen we de overgangsrelaties opslaan als OBDD • Hoe kunnen we het CTL model checking algoritme herschrijven zodat het de operaties apply, restrict, ... gebruikt. 66

We bekijken eerst hoe we deelverzamelingen van een verzameling toestanden kunnen vooerstellen. Stel hiervoor S een eindige verzameling van gelijk wat. Om een deelverzameling van S als OBDD voor te stellen moeten we dus de elementen van S als booleaanse waarde voorstellen. Dit gebeurt in volgende stappen: 1. Geef aan elk element s ∈ S een unieke rij van booleaanse waarden (v1 , v2 , . . . , vn ). 2. We stellen nu een deelverzameling T voor als de booleaanse functie fT welke (v1 , v2 , . . . , vn ) op 1 afbeeldt als s ∈ T en anders op 0. Er zijn precies 2n booleanse vectoren (v1 , v2 , . . . , vn ) van lengte n en dus moet de lengte zodanig gekozen worden zodat 2n−1 < |S| ≤ 2n met |S| het aantal elementen in S. Definitie 43. De karakteristieke functie fT : {0, 1}n → {0, 1} zegt ons ∀s ∈ S, voorgesteld door (v1 , v2 , . . . , vn ) of s ∈ T ⊆ S, en dus: 1 :s∈T fT (binaire voorstelling s) = 0 : s 6∈ T In het geval dat s een verzameling van toestanden in een overgangssysteem M = (S, →, L) is, bestaat er een natuurlijke manier om de booleanse voorstelling van een element te kiezen. De voortelling wordt namelijk gegeven door de labelende functie L : S → P(Atoms). Hierbij veronderstellen we een vaste ordening op de verzameling Atoms, stel x1 , x2 , . . . , xn . We stellen s ∈ S nu voor met de vector (v1 , v2 , . . . , vn ) waar voor elke i, vi gelijk is aan 1 als xi ∈ L(s), anders is vi = 0. We moeten nu nog garanderen dat deze voorstelling voor elke s ∈ S uniek is. Daarom eisen we dat ∀s1 , s2 ∈ S, L(s1 ) = L(s2 ) ⇒ s1 = s2 . Indien dit niet het geval is, bijvoorbeeld omdat 2|Atoms| < |S|, dan kunnen we extra atomaire proposities toevoegen totdat we genoeg onderscheidingen kunnen maken. Een toestand wordt nu voorgesteld als een OBDD van de booleaanse functie l1 · l2 · · · · · ln waarin xi als xi ∈ L(s) fT (binaire voorstelling s) = xi als xi 6∈ L(s) De verzameling van toestanden wordt nu voorgesteld door de OBDD van de functie: (l11 · l12 · · · · · l1n ) + (l21 · l22 · · · · · l2n ) + · · · + (lm1 · lm2 · · · · · lmn ) waarin li1 · l12 · l1n de toestand si voorstelt. We nemen het voorbeeld uit figuur 8 en lijsten de deelverzamelingen van de toestanden van het model op:

67

x1

x2

Figuur 8: Een simpel CTL model verzameling standen ∅ {s0 } {s1 } {s2 } {s0 , s1 } {s0 , s2 } {s1 , s2 } S

van

toe-

voorstelling door booleaanse variabelen (1, 0) (0, 1) (0, 0) (1, 0), (1, 0), (0, 1), (1, 0),

(0, 1) (0, 0) (0, 0) (0, 1), (0, 0)

voorstelling door booleaanse functie 0 x1 · x2 x1 · x2 x1 · x2 x1 · x2 + x1 · x2 x1 · x2 + x1 · x2 x1 · x2 + x1 · x2 x1 · x2 + x1 · x2 + x1 · x2

Het interessante aan de OBDD voortelling is dat hij heel klein kan zijn. Het CTL model dat in figuur 8 wordt weergegeven is het volgende: def

• S = {s0 , s1 , s2 } def

• → = {(s0 , s1 ), (s1 , s2 ), (s2 , s0 ), (s2 , s2 )} def

def

def

• L(s0 ) = {x1 }, L(s1 ) = {x2 }, L(s2 ) = ∅ We zien meteen dat aan de eis dat voor alle toestanden s1 , s2 moet gelden dat als L(s1 ) = L(s2 ) ⇒ s1 = s2 voldaan is. We kunnen de verzameling toestanden dus ordenen met de volgorde [x1 , x2 ] zoals dit in bovenstaande tabel is gebeurt. Het valt op dat de vector (1, 1) en de bijbehorende functie 1, 1 niet gebruikt zijn en we zijn dus vrij om te kiezen of we het in een representatie van een deelverzameling van S weergeven of niet. We kunnen hiervoor kiezen om de grootte van de OBDD te optimaliseren. De deelverzameling {s0 , s1 } kan dus x1

x1

x2

0

1

x2

x2

0

1

Figuur 9: Twee OBDD voorstellingen voor de verzameling {s0 , s1 } beter voorgesteld worden door de booleaanse functie x1 , x2 aangeziende bijbehorende OBDD kleiner is dan die voor x1 · x2 + x1 · x2 zoals te zien is op figuur 9. We gaan nu na of alle 68

operaties die het CTL model checking algoritme gebruikt uitgevoerd kunnen worden op deze voorstelling: • Doorsnede, Unie en Complement van deelverzamelingen: Deze worden letterlijk vertaald met ·, + en x en maken dus gebruik van het apply algoritme. • De functies: – pre∃ (X) = {s ∈ S | ∃s0 , (s → s0 ∧ s0 ∈ X)} – pre∀ (X) = {s ∈ S | ∀s0 , (s → s0 → s0 ∈ X)} De functie pre∃ neemt een deelverzameling X van toestanden en geeft de verzameling van toestanden die een overgang naar X kunnen maken terug. De functie pre∀ neemt een deelverzameling X van toestanden en geeft de verzameling van toestanden die enkel en alleen maar een transitie naar X kunnen maken terug. We beschrijven nu hoe we overgangsrelaties met OBDD’s kunnen weergeven. Een overgangsrelatie → van van een model M = (S, →, L) is een deelverzameling van S × S. Deelverzamelingen van een eindige verzamelingen worden via de karakteristieke functie van een binaire encoding als OBDD’s weergegeven. Net zoals bij deelverzamelingen zal ook hier de labelende functie de binaire encoding aangeven. Aangezien → een een deelverzameling is van S × S hebben we twee kopiën nodig van de booleaanse vectoren. De overgangsrelatie s → s0 wordt dus weergegeven door het paar bitvectoren ((v1 , v2 , . . . , vn ), (v10 , v20 , . . . , vn0 )) waar vi = 1 als pi ∈ L(s) en vi = 0 in de andere gevallen. Analoog is vi0 = 1 als pi ∈ L(s0 ) en 0 in de andere gevallen. In een OBDD wordt de overgangsrelatie nu weergegeven als een OBDD van de functie: (l1 · l2 · · · · · ln ) · (l10 · l20 · · · · · ln0 ) en een verzameling van overgangsrelaties, dus →, is het OBDD van de som van alle links. Als voorbeeld berekenen we de OBDD voor de transitierelatie op figuur 8 welke dus gegeven wordt door: def → = {(s0 , s1 ), (s1 , s2 ), (s2 , s0 ), (s2 , s2 )} We tonen deze relatie eerst als een waarheidstabel in tabel 1. Elke 1 in de laatste kolom duid aan dat er een link in de transitierelatie zit en elke 0 toont de afwezigheid van een link aan. De booleaanse functie die de transitierelatie weergeeft wordt nu gevonden door de disjunctie van de rijen die 1 hebben in de laatste kolom te nemen en wordt dus gegeven door: def

f → = x1 · x2 · x01 · x02 + x1 · x2 · x01 · x02 + x1 · x2 · x01 · x02 + x1 · x2 · x01 · x02 Meestal is het zo dat men best variabelen met en zonder accent door elkaar zet in de ordening, dus beter [x1 , x01 , x2 , x02 ] dan [x1 , x2 , x01 , x02 ]. De resulterende OBDD wordt nu gegeven op figuur 10. Het volstaat nu om aan te tonen dat de functies pre∃ en pre∀ met een OBDD berekend kunnen worden. Stel de OBDD’s BX voor X en B→ voor de transitierelatie →. We merken op dat pre∀ uitgedrukt kan worden in termen van complementen en pre∃ en wel op de volgende manier: 69

x1 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1

x2 0 0 0 0 1 1 1 1 0 0 0 0 1 1 1 1

x01 0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1

x02 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1

→ 1 0 1 0 1 0 0 0 0 1 0 0 0 0 0 0

x1 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1

x01 0 0 0 0 1 1 1 1 0 0 0 0 1 1 1 1

x2 0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1

x02 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1

→ 1 0 1 0 1 0 0 0 0 1 0 0 0 0 0 0

Tabel 1: De waarheidstabel voor de overgangsrelatie, de twee tabellen tonen elk een andere ordening. x1

x01

x01

x2

x2

x02

x02

0

1

Figuur 10: Een OBDD voor de transitierelatie uit het voorbeeld pre∀ = S−pre∃ (S − X) waarin we S − Y noteren voor de verzameling van alle s ∈ S die niet in Y zitten. We moeten dus enkel uitleggen hoe we de OBDD voor pre∃ (X) moeten berekenen in termen van BX en B→ .

70

Dit gaat als volgt: 1. Plaats bij alle variabelen in BX een accent en noem de resulterende OBDD BX 0 . 2. Bereken de OBDD voor exists(ˆ x0 , apply(·, B→ , BX 0 )). In de handouts van hoofdstuk 9 staat een uitgewerkt voorbeeld vanaf slide 10/20.

6

Algebra¨ısche normaalvorm en resolutie

6.1

Adequate verzamelingen

Definitie 44. Een verzameling X van booleaanse functies wordt adequaat of functioneel volledig genoemd als elke booleaanse functie uit die verzameling uitgedrukt kan worden door een samenstelling van functies uit X en projectiefuncties. Een projectiefunctie is een functie van de vorm πin met xi = πin (x1 , . . . , xn ). Zo zijn bijvoorbeeld {¬, ∧}, {¬, ∨} adequate verzamelingen en {∧, ∨, →} is dat niet. Intu¨ıtief is een verzameling van adequate connectieven een verzameling connectieven die het mogelijk maken alle mogelijke connectieven uit te drukken. Voeren we bijvoorbeeld volgende connectieven in: • x ↑ y := ¬(x ∧ y) • ite(x, y, z) = (x → y) ∧ (¬x → z) dan zijn {↑} en {ite, >, ⊥} adequate verzamelingen omdat we ze in termen van andere adequate verzamelingen kunnen schrijven: • {↑}: – ¬x ≡ x ↑ x – x ∧ y ≡ (x ↑ y) ↑ (x ↑ y) • {ite, >, ⊥}: – ¬x ≡ ite(x, ⊥, >) – x ∧ y ≡ ite(x, y, ⊥)

6.2

Algebra¨ısche normaalvorm

We voeren nu de algebra¨ısche normaalvorm in naast de disjunctieve en conjunctieve normaalvorm. We maken hiervoor volgende mappings: • T 7→ 1 • F 7→ 0 • x + y = x ⊕ y = (x ∧ ¬y) ∨ (¬x ∧ y) • x·y =x∧y

71

De operaties op F2 zijn associatief en dus kan men de haakjes bij opeenvolgende optredens van ⊕ en · schrappen. We stellen dat lege sommen de waarde 0 hebben en lege producten de waarde 1. Voor veeltermfuncties over F2 geldt dat k 2 = k, maar de als veelterm is X 2 wel verschillend van X. Stelling 8. Iedere booleaanse functie f : {0, 1}n → {0, 1} kan uniek worden herschreven als veeltermfunctie Y M cA · xi f (x1 , . . . , xn ) = A⊆{1,...,n}

i∈A

met c∅ , . . . , c{1,...,n} ∈ {0, 1}. We bewijzen dit met behulp van inductie: • Basisstap: als n = 0 of n = 1 dan volgt de bewerking gemakkelijk door opsomming van de mogelijke gevallen. • Inductiestap: stel nu dat n > 1. Het bestaan van een normaalvorm volgt met inductie uit f (x1 , . . . , xn ) = f (0, x2 , . . . , xn ) ⊕ x1 (f (0, x2 , . . . , xn ) ⊕ f (1, x2 , . . . , xn )). Het uniek zijn van deze normaalvorm volgt uit de lineaire algebra voor eindige velden. Het is n namelijk zo dat de ring F2 [x1 , . . . , xn ]/(x21 ⊕x1 , . . . , x2n ⊕xn ) 22 elementen heeft. Omdat n er precies 22 booleaanse functies met n variabelen bestaan is dus normaalvorm dus uniek. Men kan ook elementair inductief argumenteren dat de nulfunctie door een unieke keuze van coëfficienten beschreven wordt: Stel dat M Y f (x1 , . . . , xn ) = cA · xi = 0 A⊆{1,...,n}

i∈A

voor alle keuzes van xi . Zij g(x2 , . . . , xn ) =

M A⊆{2,...,n}

cA ·

Y

xi

i∈A

Dan geldt g(x2 , . . . , xn ) = f (0, x2 , . . . , xn ) = 0 voor alle keuzes van xi . Na de inductiehypothese geldt dus dat cA = 0, ∀A ⊆ {1, . . . , n} met 1 ∈ A. Dus cA = 0 voor alle keuzes van A. Het algemene geval van een niet-nulfunctie kan men behandelen door het bekijken van het verschil tussen twee veeltermfuncties. De stelling van Post geeft ons nu de meer formele voorwaarden om na te gaan waneer een verzameling van booleaanse functies adequaat is. Echter moeten we daarvoor eerst volgende begrippen invoeren. Definitie 45. Een booleaanse functie is false-bewarend als f (0, . . . , 0) = 0 en true-bewarend als f (1, . . . , 1) = 1). Definitie 46. Een booleaanse functie is monotoon als uit xi ≤ yi , ∀i ≤ n volgt dat f (x1 , . . . , xn ) ≤ f (y1 , . . . , yn ). Definitie 47. Een booleaanse functie f is zelf duaal als f (x1 , . . . , xn ) = f (x1 , . . . , xn ), ∀xi .

72

Definitie 48. Een booleaanse functie f is affien als f (x1 , . . . , xn ) = c0 ⊕ c1 x1 ⊕ . . . ⊕ cn xn voor zekere selectie van ci ∈ {0, 1}. Uit stelling 8 volgt dat een booleaanse functie fM niet affienY is als er een A ⊆ {1, . . . , n} bestaat zodat |A| ≥ 2 en cA = 1 en f (x1 , . . . , xn ) = cA · xi A⊆{1,...,n}

i∈A

Stelling 9. (Stelling van Post) Een verzameling X van booleaanse functies is adequaat als en slechts als aan volgende voorwaarden is voldaan: • ∃f ∈ X zodat f niet false-bewarend is. • ∃f ∈ X zodat f niet true-bewarend is. • ∃f ∈ X zodat f niet monotoon is. • ∃f ∈ X zodat f niet zelf-duaal is. • ∃f ∈ X zodat f niet affien is. We geven nu een bewijs: • Men ziet gemakkelijk in dat composities van false-bewarende, true-bewarende, monotone, zelf-duale en affiene functies weer false-bewarende, true-bewarende, monotone, zelf-dulel en affiene functies zijn. Als dus alle functies uit X één van deze eigenschappen hebben kan een samenstelling ervan nooit een functie zijn die deze eigenschap niet heeft. • Voor de andere bewijsrichting definiëren we eerst 0, 1, x. Stel daarvoor g(x) = f1 (x, x, . . . , x) en h(x) = f2 (x, x, . . . , x). Dan geldt g(x) = 1 of g(x) = x en h(x) = 0 of h(x) = x omdat f1 niet false-bewarend is en f2 niet true-bewarend is. We hebben dan vier mogelijke gevallen: 1. g(x) = 1 en h(x) = x . Dan geldt h(g(x)) = 0. 2. g(x) = x en h(x) = 0. Dan geldt g(h(x)) = 1. 3. g(x) = 1 en h(x) = 0. Kies een niet monotone f3 ∈ X. Dan bestaat er een i ∈ {1, . . . , m} en bestaan er a1 , . . . , ai−1 , ai+1 , . . . , am ∈ {0, 1} met f3 (a1 , . . . , ai−1 , x, ai+1 , . . . , am ) = x Dan geldt voor j 6= dat aj = g(x) of aj = h(x) dus kan x worden gedefinieerd met behulp van f3 , g, h. 4. g(x) = x en h(x) = x. Kies een niet zelf-duale f4 ∈ X. Dan bestaan er b1 , . . . , bn ∈ {0, 1} zodat f4 (b1 , . . . , bn ) = f4 (b1 , . . . , bn ). Neem i(x) = f4 (x ⊕ b1 , . . . , x ⊕ bk ) dan geldt i(0) = i(1) en dus i(x) = 1 of i(x) = 0. Dus g(i(x)) = 0 of g(i(x)) = 1. Verder geldt x ⊕ bj = x of x ⊕ bj = x = g(x) en dus kan i(x) worden gedefinieerd met behulp van f4 , g. 73

We hebben nu 0, 1, x gedefinieerd door middel van f1 , f2 , f3 , f4 . We definiëren nu x · y met hulp van f1 , f2 , f3 , f4 , f5 . Er bestaan g1 , g2 , g3 , g4 zodat (zonder de algemeenheid te schaden): f5 (x1 , . . . , xl ) = x1 · x2 · g1 (x3 , . . . , xl ) ⊕ x1 · g2 (x3 , . . . , xl ) ⊕ x2 · g3 (x3 , . . . , xl ) ⊕ g4 (x3 , . . . , xl ) met g1 (x3 , . . . , xl ) 6= 0 vanwege de algebra¨ısche normaalvormstelling. Er bestaan nu c3 , . . . , cl ∈ {0, 1} zodat g1 (c3 , . . . , cl ) = 1, stel nu: – c = g2 (c3 , . . . , cl ) – d = g3 (c3 , . . . , cl ) – e = g4 (c3 , . . . , cl ) Dan geldt f5 (x1 , x2 , c3 , . . . , cl ) = x1 · x2 ⊕ x1 c ⊕ x2 d ⊕ e. Definieer nu h(x, y) = f5 (x ⊕ d, y ⊕ c, c3 , . . . , cl ) ⊕ cd ⊕ e dan geldt h(x, y) = (x ⊕ d)(y ⊕ c) ⊕ (x ⊕ d)c ⊕ (y ⊕ c)d ⊕ e ⊕ cd ⊕ e = xy ⊕ xc ⊕ dy ⊕ dc ⊕ xc ⊕ dc ⊕ yd ⊕ cd ⊕ e ⊕ cd ⊕ e = xy Definitie 49. Een clausule is een verzameling {l1 , . . . , ln } van literalen die staat voor de formule f ({l1 , . . . , ln }) = l1 ∨ . . . ∨ ln . Definitie 50. Een clausulevorm is een verzameling van clausules {C1 , . . . , Cm } die staat voor de formule g({C1 , . . . , Cm }) = f (C1 ) ∧ . . . ∧ f (Cm ). staat voor de lege clausule en die is niet vervulbaar. Een clausulevorm die bevat is dus per definitie niet vervulbaar. ER bestaat dus voor iedere formule φ een clausulevorm ψ zodat φ ≡ g(ψ) Bijvoorbeeld: Conjunctieve normaalvorm ¬p ∧ (¬q ∨ ¬p) ∧ (¬p ∨ ¬r)) (¬p ∨ q) ∧ (q ∨ ¬r) ∧ (p ∨ q ∨ ¬r)) (¬p ∨ ¬p) ∧ (q ∨ r) ∧ (r ∨ q)

Clausule vorm {{¬p}, {¬q, ¬p}, {¬p, ¬r}} {{¬p, q}, {q, ¬r}, {p, q, ¬r}} {{¬p}, {q, r}}

Definitie 51. Twee( literalen l1 en l2 zijn complementair als l1 = ¬l2 of ¬l1 = l2 . Als l een ¬p als l = p literaal is dan lc = p als l = ¬p Definitie 52. We definiëren: • Twee clausules C1 en C2 clashen als er een literaal l bestaat met l ∈ C1 en lc ∈ C2 . • Een resolvent van twee clashende clausules C1 en C2 is een clausule (C1 \{l})∪(C2 \{lc }). C1 en C2 worden dan ouder-clausules van de resolvent genoemd. 74

• Als S een verzameling van clausules is dan is Res(S) = S ∪ {R : R is resolvent van twee clausules in S} Definitie 53. (Resolutie) We definiëren: • Res0 (S) = S • Resn+1 (S) = Res(Resn (S)) S n • Res∗ (S) = ∞ n=0 Res (S) We merken op dat er altijd een n bestaat met Res∗ (S) = Resn (S) omdat de machtverzameling van de machtverzameling van een verzameling met een eindig aantal atomen opnieuw eindig is. We voeren nu volgende procedure in om een resolutie te vinden: repeat T = S; S = Res(S); until ( ∈ S) or (T = S); if ∈ S then S is niet vervulbaar else S is vervulbaar Definitie 54. Een deductie van vanuit een clausulevorm S is een reeks C1 , C2 , . . . , Cm van clausules zodat Cm = en ∀i, i = 1, . . . , m geldt: Ci ∈ S of Ci is resolvent van twee clausules Cj , Ck met j, k < i. Lemma 8. ∈ Res∗ (S) als en slechts als er een deductie bestaat van uit S. Dit kan bewezen worden met inductie over de lengte van de afleiding. Hierdoor met men dus niet alle clausules van Res∗ (S) opschrijven om ∈ Res∗ (S) aan te tonen. Het volstaat om een deductie van uit S te vinden. Lemma 9. Als Γ een clausulevorm is en R resolvent van twee clausules uit Γ dan zijn Γ en Γ ∪ {R} equivalent. We bewijzen nu dit lemma. Stel dat v een bedeling is met v(Γ ∪ {R}) = T , dan geldt zeker ook datl v(Γ) = T . Omgekeerd, als v(Γ) = T en R resolventen zijn van twee clausules C1 , C2 met R = C1 \{l} ∪ C2 \{lc } met l ∈ C1 en lc ∈ C2 dan bestaan er twee opties: 1. v(l) = T : v(C2 ) = T levert dan v(C2 \{lc }) = T dus v(R) = T . 2. v(l) = F : v(C1 ) = T levert dan v(C1 \{l}) = T dus v(R) = T . in totaal dus v(Γ ∪ {R}) = T .

Stelling 10. Als uit een clausulevorm u de lege clausule kan worden afgeleid dan is u niet vervulbaar. 75

Bewijs. Stel ∈ Res∗ (u) en zij ∈ Resn (u) voor een zekere n. De lege clausule kan men alleen verkrijgen door resolutie van twee clausules C1 en C2 met C1 = {l} en C2 = {lc }. Het resolutielemma toont aan dat u ≡ Res1 (u) ≡ Res2 (u) ≡ · · · ≡ Resn (u) waarbij C1 , C2 ∈ Resn (u). Omdat {C1 , C2 } niet vervulbaar is, is Resn (u) niet vervulbaar en daardoor is u ook niet vervulbaar. Stelling 11. Voor het aantonen van niet-vervulbaarheid van clausulevormen volstaat resolutie. Zij u een niet-vervulbare clausule vorm. dan kan met met resolutiestappen uit u, afleiden. Bewijs. Zij u een niet-vervulbare verzameling van clausules. Zij p1 , . . . , pn een volledige lijst van optredende atomen. Met inductie op n tonen wij ∈ Res∗ (u) aan: • Als n = 0 dan u = {} en ∈ u ∈ Res∗ (u). • Stel voor de inductiestap dat u atomen p1 , . . . , pn+1 bevat. Construeer u0 uit u door weghalen van alle optredens van pn+1 in clausules en door verwijderen van alle clausules waar ¬pn+1 optreedt. Construeer analoog u” uit u door weghalen van alle optredens van ¬pn+1 en door verwijderen van alle clausules waar pn+1 optreedt. u0 en u” zijn niet vervulbaar: – Stel anders dat er een bedeling v bestaat die zeg maar aan u0 de waarde T toekent. Zij v 0 (pi ) = v(pi ) voor i < n + 1 en v 0 (pn+1 ) = F . Dan is v 0 een bedeling met v 0 (u) = T . Een tegenspraak. – Een analoog argument geldt voor u”. De inductie hypothese geeft ∈ Res∗ (u0 ) en ∈ Res∗ (u”). Voor u0 betekent dat, dat 0 bestaan met C 0 = en voor i = 1, . . . , m geldt C 0 ∈ u0 of C 0 er clausules C10 , . . . , Cm m i i is resolvent van twee clausules Ca0 , Cb0 met a, b < i. Voor u betekent dat (via inductie op i ≤ m) dat er clausules C1 , . . . , Ci bestaan met Ci ⊆ Ci0 ∪ {pn+1 } en voor i = 1, . . . , m geldt Ci ∈ u of Ci is resolvent van twee clausules Ca , Cb met a, b < i. We werken nu de inductie uit en merken eerst op dat geldt: – Als R0 resolvent van twee ouderclausules C10 , C20 is en p 6∈ C10 ∪ C20 en C1 ⊂ C10 ∪ {p} en C2 ⊂ C20 ∪ {p} dan bestaat resolvent R van C1 , C2 met R ⊆ R0 ∪ {p}. Neem nu door de inductiehypothese aan dat C0 , . . . Ci−1 zoals gewenst geconstrueerd zijn en bekijk Ci0 . Indien Ci0 ∈ u0 dan bestaat naar constructie Ci ∈ u met Ci ⊆ Ci0 ∪ {pn+1 } en C0 , . . . , Ci−1 , Ci is zoals gewenst. Anders is Ci0 resolvent van twee ouderclausules Ca0 , Cb0 met a, b < i. Uit de inductiehypothse volgt het bestaan van D0 , . . . , Da en E0 , . . . , Eb zoals gewenst met Da ⊆ Ca0 ∪{pn+1 } en Eb ⊆ Cb0 ∪ {pn+1 }. Dan bestaat wegens de opmerking een resolvent ci van Da en Eb met Ci ⊂ Ci0 ∪ {pn+1 }. De gewenste reeks is dan D0 , . . . , Da , E0 , . . . , Eb , Ci . Vanwege Cm ⊆ {pn+1 } volgt ∈ Res∗ (u) of {pn+1 } ∈ Res∗ (u). Analoog ziet men ∈ Res∗ (u) of {¬pn+1 } ∈ Res∗ (u). Indien ∈ Res∗ (u) dan zijn we al klaar. Anders verkrijgen we uit {pn+1 } en {¬pn+1 } met een resolutiestap ook en dus ∈ Res∗ (u).

76

Theorie Formele logica

Recommend Documents