Les Formele Logica
05 - 03 - 2004
Benjamin De Leeuw Departement Zuivere Wiskunde en Computer Algebra Galglaan 2, B-9000 Gent
[email protected] Gent University, Belgium
March 9, 2004
1
Doelstelling 1. De Computer als logische Rekenmachine 2. Oefeningen op Semantische Tableau’s 3. Oefeningen op Deductiecalculus PROPC 4. FLIPO : Formele Logica in Prologomgeving 5. Oefeningen op het Gebruik van FLIPO 6. Eerste Project
2
De Computer als logische Rekenmachine • De computer wordt gebruikt als rekenmachine. • Voor elk berekenbaar probleem, kan er een programma opgesteld worden dat de oplossing uitrekent op een rekenmachine. Een programma is een opeenvolging van commando’s voor de rekenmachine. • Berekenbaar komt theoretisch overeen met Turing Berekenbaar. • Een probleem is Turing berekenbaar indien er een Turing Machine kan worden opgesteld die het probleem oplost. (Zie Datastructuren en Algoritmen II, Formele Logica hfdst 4 en 5, Formele Talen en Automaten). • Het opstellen van een tabel of tableau, en het construeren van een tegenvoorbeeld, voor een formule in PROPA , is een berekenbaar probleem. (Het bewijs hiervan staat in de cursus Formele Logica, pp. 23-24).
1
• Het opstellen van een model voor een formule in PROPA is een berekenbaar probleem. • Het nakijken van een met de hand gemaakte deductie voor een logische formule in PROPC , is een berekenbaar probleem. • Het zoeken naar een deductie voor een logische formule in PROPC , is een berekenbaar probleem. • Het zoeken naar een deductie voor een logische formule in PREDΣ , is een onbeslisbaar probleem. • Het nakijken van een met de hand gemaakte deductie voor een logische formule in PREDΣ , is een berekenbaar probleem. • Het berekenbaar of onbeslisbaar zijn van een logica heeft alles te maken met de uitdrukkingskracht van die logica. • De uitdrukkingskracht bepaalt wat men kan zeggen in een logica, welke en hoeveel informatie (over de werkelijkheid) men kan bevatten in een logica. De uitdrukkingskracht van PROPC is kleiner dan die van PREDΣ . • Alle logica’s met minstens de uitdrukkingskracht van eerste orde logica, zijn onbeslisbaar. • Omdat rekenen op papier met de deductiecalculus van bvb PROPC onderworpen is aan (schrijf)fouten, willen we de pc als ondersteuning gebruiken. De pc maakt geen (schrijf)fouten in een deductie. Het is de bedoeling van de lessen in de pc-zalen om de studenten vertrouwd te maken met de pc als logische rekenmachine. Volgende programma’s zullen aan bod komen in de lessen: • FLOBES : Formeel LOgisch BEwijsvoeringSysteem, een programma dat bewijzen nakijkt, ter ondersteuning van een deductiecalculus • OPA : Open Source Prooving Assistant, een programma dat deducties in PROPC zoekt • PAPA : Pieter’s Automated Prooving Assistant, een programma dat deducties in PROPC zoekt • FLIPO : Formele Logica in Prolog Omgeving, FLOBES + OPA • NPPV : New Paltz Program Verifier, een programma ter ondersteuning van deductie in de Hoare-calculus (zie cursus Formele Logica, hfdst 4) • PROLOG : een logische programmeertaal • PVS : Prototype Verification System1 , een programma dat modelspecificaties2 nakijkt op correctheid en consistentie 1 2
We zullen PVS enkel bekijken indien er tijd en interesse voor is. Dit is geen examenleerstof. ‘Model’ wordt hier verstaan in zijn breedste betekenis, als beeld voor een stuk van de werkelijkheid.
2
3
Oefeningen op Semantische Tableau’s
We vatten aan met enkele bruikbare definities en eigenschappen. Definitie 1 We defini¨eren twee nieuwe symbolen in PROPA : p→q p∨q
≡ ≡
¬(p ∧ ¬q) ¬(¬p ∧ ¬q)
We gaan nu de overeenkomstige tableau-reductieregels afleiden: L, p → q . R | L, ¬(p ∧ ¬q) . R | L . p ∧ ¬q, R /\ L . p, R L . ¬q, R | L, q . R en voor het andere lid:
L . p → q, R | L . ¬(p ∧ ¬q), R | L, p ∧ ¬q . R | L, p, ¬q . R | L, p . q, R
Voor het andere symbool verkrijgen we: L, p ∨ q . R | L, ¬(¬p ∧ ¬q) . R | L . ¬p ∧ ¬q, R /\ L . ¬p, R L . ¬q, R | | L, p . R L, q . R
3
en voor het andere lid tenslotte: L . p ∨ q, R | L . ¬(¬p ∧ ¬q), R | L, ¬p ∧ ¬q . R | L, ¬p, ¬q . R | L . p, q, R Samenvattend hebben we dus vier nieuwe reductieregels ge¨ıntroduceerd. Reductieregels 2 We hebben vier nieuwe reductieregels afgeleid in PROPA , twee voor elk nieuw symbool uit definitie 1: →L
∨L
L, p → q . R /\ L . p, R L, q . R
→R
L, p ∨ q . R /\ L, p . R L, q . R
∨R
L . p → q, R | L, p . q, R
L . p ∨ q, R | L . p, q, R
Ga nu gebruikmakend van deze nieuwe reductieregels volgende uitdrukkingen na op geldigheid: 1. .p → (p ∨ q) 2. .(p ∨ q) → p 3. p → q . (p ∨ q) → (p ∧ q) 4. p ∨ (q ∧ r) . (p ∨ q) ∧ (p ∨ r) 5. .((p ∧ q) ∧ r) ∨ ((¬p ∧ ¬q) ∧ ¬r) Voorbeeld 1 .p → (p ∨ q) | p.p∨q | p . p, q ⊥
4
Voorbeeld 1 geeft ons een gesloten tableau. Bijgevolg is uitdrukking 1 geldig. Met de adequaatheid van de tableaumethode (L |= α asa er bestaat een gesloten semantisch tableau voor L . α), en door het feit dat L = φ in voorbeeld 1, geldt |= p → (p ∨ q) wat dus betekent dat dit een tautologie is. Voorbeeld 2 .(p ∨ q) → p | p∨q.p /\ p.p q.p ⊥ × Voorbeeld 2 heeft een open tableau. We construeren uit de open tak het tegenvoorbeeld q =1.p=0 Uitdrukking 2 is geen tautologie omdat er geen gesloten tableau voor kan worden opgesteld. Oefening 3,4 en 5 suggereren ons dat deze tableaumethode niet de meest geschikte is voor geldigheidsbewijzen op papier. Ga dit na door de tableau’s op te stellen voor uitdrukkingen 3,4 en 5. De oplossingen kunnen ter controle worden afgegeven. De tableaumethode is echter zeer interessant voor automatische verificatie van geldigheid. Extra opgave: schrijf een javaprogramma dat, gebruikmakend van de tableaumethode, de geldigheid van een uitdrukking in PROPA nagaat, of een tegenvoorbeeld construeert. Men mag ervan uitgaan dat elke uitdrukking die als input dient, een wff is.
4
Oefeningen op Deductiecalculus PROPC
Op het examen wordt meestal de volgende vraag gesteld over PROPC : Ga na of volgende regels betrouwbaar zijn, zo ja geef een deductie of bewijs, zo neen, geef een tegenvoorbeeld. Bij deze vraag horen dan ´e´en of meerdere logische uitdrukkingen. Definitie 3 We noemen een uitdrukking L ` α betrouwbaar als L |= α. Er zijn twee manieren om L |= α vast te stellen: tabelmethode of tableaumethode. Gebruik ´e´en van beide. We geven hiervoor kort de verklaring. We weten dat M |= α geldig is indien we een tabel kunnen opstellen die α waar maakt. En dat M |= L 5
geldig is indien we een tabel kunnen opstellen die alle β ∈ L waar maakt. Indien nu voor elke M geldt dat M |= L → M |= α dan schrijven we L |= α L |= α is daarom af te lezen uit een tabel, over alle elementen β ∈ L en α. Met de adequaatheid van de tableaumethode: L |= α asa er bestaat een gesloten semantisch tableau voor L . α komen we rechtstreeks tot een manier om L |= α aan te tonen. Er wordt gevraagd om eerst de betrouwbaarheid te testen, omdat het logisch is dat we geen deductie zullen vinden voor een uitdrukking die niet betrouwbaar is. Ga de betrouwbaarheid van volgende uitdrukkingen na en geef een deductie of een tegenvoorbeeld: 1. p ↔ q, (¬p ∧ ¬q) → ¬r, r ` q 2. (p ∧ q) → ¬r, ¬(r → s), (q ∨ s) ` ¬p 3. ` ((p → q) → (p → r)) → (p → (q → r)) 4. ` ((p → q) → p) → p 5. p → (q ∨ (r → s)), q → (q → ¬p), ¬(r → ¬p) ` s
6
Oplossing: al deze uitdrukkingen zijn betrouwbaar. We geven enkele deducties: (1) (2) (3) (4) (5) (6) (7) (8) (9) (10) (11) (12) (13) (14)
p`p ¬q ` ¬q p, ¬q ` p ↔ ¬q p ↔ ¬q ` ¬(p ↔ q) p, ¬q ` ¬(p ↔ q) p, (p ↔ q) ` q ¬p ∧ ¬q ` ¬p ∧ ¬q ¬p, ¬q ` ¬p ∧ ¬q ¬q, ¬(¬p ∧ ¬q) ` p (p ↔ q), ¬q, ¬(¬p ∧ ¬q) ` q r, ¬r ` q (p ↔ q), ¬q, (¬p ∧ ¬q) → ¬r, r ` q q`q (p ↔ q), (¬p ∧ ¬q) → ¬r, r ` q
(1) (2) (3) (4) (5) (6) (7) (8) (9) (10) (11)
p∧q `p∧q p, q ` p ∧ q q, ¬(p ∧ q) ` ¬p ¬r, r ` ¬p q, (p ∧ q) → ¬r, r ` ¬p q, (p ∧ q) → ¬r, p ` ¬r ¬r ` (r → s) q, (p ∧ q) → ¬r, p ` (r → s) s ` (r → s) (q ∨ s), (p ∧ q) → ¬r, p ` (r → s) (p ∧ q) → ¬r, ¬(r → s), (q ∨ s) ` ¬p
(1) (2) (3) (4) (5) (6) (7) (8) (9) (10) (11) (12) (13)
(p ∧ ¬r) ∧ p, q ` q (p ∧ ¬r), p, q ` q p, ¬r, p, q ` q p, ¬r, q ` (p → q) p, q, ¬(p → q) ` r ¬(p → q), p ` (q → r) ¬(p → q) ` p → (q → r) r ` (q → r) ¬p, p ` (q → r) (p → r), p ` (q → r) (p → r) ` p → (q → r) (p → q) → (p → r) ` p → (q → r) ` ((p → q) → (p → r)) → (p → (q → r))
7
(A) (A) (EqIC1 (1, 2)) (EqN 3) (SN (3, 4)) (CoP o4 (5)) (A) (AnDc(7)) (CoP o3 (8)) (SN (9, 6)) (XQ1 ) (I(10, 11)) (A) (R(12, 13)) (A) (AnDc(1)) (CoP o1 (2)) (XQ1 ) (I(3, 4)) (CoP o2 (5)) (XQ3 ) (SN (6, 7)) (I2 ) (D(8, 9)) (CoP o1 (10)) (Aex) (AnDc(1)) (AnDc(2)) (I1 (3)) (CoP o3 (4)) (I1 (5)) (I1 (6)) (I2 ) (XQ1 ) (I(9, 8)) (I1 (10)) (I(7, 11)) (I1 (12))
(1) (2) (3) (4) (5) (6) (1) (2) (3) (4) (5) (6) (7) (8) (9) (10) (11) (12) (13) (14)
4.1
p, ¬p ` q ¬p ` (p → q) ¬(p → q) ` p p`p (p → q) → p ` p ` ((p → q) → p) → p
(XQ1 ) (I1 (1)) (CoP o3 (2)) (A) (I(3, 4)) (I1 (5))
q, ¬q ` ¬p r, ¬r ` ¬p s, ¬s ` ¬p (r → s), r, ¬s ` ¬p q ∨ (r → s), r, ¬s, ¬q ` ¬p ¬p ` ¬p p → (q ∨ (r → s)), r, ¬s, ¬q ` ¬p q, ¬p ` ¬p q ∨ (r → s), r, ¬s, ¬p ` ¬p p → (q ∨ (r → s)), r, ¬s, ¬p ` ¬p p → (q ∨ (r → s)), (q → ¬p), r, ¬s, ` ¬p p → (q ∨ (r → s)), q → (q → ¬p), r, ¬s, ` ¬p p → (q ∨ (r → s)), q → (q → ¬p), ¬s, ` (r → ¬p) p → (q ∨ (r → s)), q → (q → ¬p), ¬(r → ¬p), ` s
(XQ1 ) (XQ1 ) (XQ1 ) (I(2, 3)) (D(1, 4)) (A) (I(6, 5)) (Aex) (D(8, 4)) (I(6, 9)) (I(7, 10)) (I(7, 11)) (I1 (12)) (CoP o3 (13))
Opmerking
Zeker in het laatste bewijs kunnen we vaststellen dat de tableaumethode en de deductiecalculus veel met elkaar gemeen hebben. Gebruikmakend van regels (XQ1 ) of (Aex), gevolgd door ´e´en of meerdere applicaties van (AnDc(x)), kunnen we uit de bladeren in een gesloten tableau de juiste assumptieregels opmaken. Door vervolgens de deductieregels (D(x, y),I(x, y),CoP on (x),. . . ), overeenkomstig met de toegepaste tableauregels (in de constructie van de gesloten tableau), toe te passen op deze assumptieregels, verkrijgen we steeds een juiste deductie, hoewel deze niet de kortste hoeft te zijn. Snoeien is meestal aangewezen. Een programma dat zelf deducties opstelt voor PROPC zal gebruikmaken van zulk een techniek. De kwaliteit van de bewijzen is dan afhankelijk van de interne boekhouding van het programma en diens geheugengebruik om de deductieboom (of tableau) bij te houden. We bespreken nu zulk een programma: FLIPO.
5
FLIPO : Formele Logica in Prologomgeving
. . . met dank aan prof. Hoogewijs en Pieter Audenaert.
5.1
Installatie
Haal het bestand flipo-0.2f.zip af van de website van Pieter Audenaert (http://cage. ugent.be/~paudenae). In dit bestand zit zowel de linuxversie als de windowsversie van FLIPO. FLIPO is geschreven in SWI-prolog. 8
Windows : Zet de bestanden flipo.exe, flipo.pl, plterm.dll, libpl.dll en d regels.pl in een directory. Zet eventueel deze directory in de Windows ‘path’-systeemvariabele. Linux : Zet de bestanden flipo.linux, flipo.pl en d regels.pl in een directory. Zet eventueel deze directory in de Linux ‘path’-systeemvariabele. De overige bestanden die worden meegeleverd in de zip-file zijn flipo.txt : een handleiding bij het programma bij FLIPO syntax.txt : een handleiding bij de syntaxisregels van FLIPO dq2q.c : een C-programma om (”) om te zetten naar (’) ggx.pl : een voorbeeldbewijs snede.pl : een voorbeeldbewijs changelog.txt : de versiegeschiedenis van het programma FLIPO
5.2
Gebruik van FLOBES
Start de SWI-prolog-console met het commando flipo.exe flipo.linux
(Windows) (Linux)
Geef vervolgens in dit SWI-prolog-venster het commando flobes(’snede.pl’).
(let op de punt)
Men leest in het SWI-prolog-venster het volgende DIT BEWIJS IS OK! met daaronder een duidelijke ‘Yes’, die het antwoord nog eens bekrachtigt. Het tekstbestand snede.pl kan in het bovenstaande uiteraard vervangen worden door een willekeurig tekstbestand. Dit tekstbestand bevat het te verifi¨eren bewijs. Dit is een deductiebewijs in prolog-syntaxis. Indien FLIPO gedraaid wordt vanuit een directory, waarop men geen schrijfrechten heeft (zoals in de PC-zalen), zal het pad moeten meegegeven worden. Voorbeeld: flobes(’c:/temp/eigenbewijs.pl’). De ondersteunde deductieregels, in prolog-syntaxis, staan in het tekstbestand d regels.pl. Regels kunnen toegevoegd worden door aan deze file te sleutelen. Deze file wordt automatisch ingeladen bij het opstarten van FLIPO. Sluit het SWI-prolog-venster met het commando halt.
(let op de punt)
Het werken met flobes zal dus vnl werken met een teksteditor zijn. Kies zelf een teksteditor. De syntaxis van de FLIPO-tekstbestanden wordt besproken in sectie 5.4. In de PC-zalen is FLIPO beschikbaar op F:/ahoogew/Flipo/ Men heeft geen schrijfrechten op deze directory. 9
5.3
Gebruik van OPA
Start de SWI-prologconsole zoals in sectie 5.2. Geef het commando opa(g(lijst,formule),’voorbeeld.pl’).
(let op de punt)
met lijst : een lijst van premissen, in prolog-syntaxis zoals in sectie 5.4 formule : een conclusieregel, in prolog-syntaxis zoals in sectie 5.4 OPA zoekt dan een bewijs voor lijst ` formule Dit bewijs komt in het bestand voorbeeld.pl te staan. De naam van dit bestand mag uiteraard arbitrair gekozen worden. Om voor de volgende uitdrukking (1) a → (p ∨ q), b → (p → r), a, ¬(b → ((q → r) → r)) ` b → ((q → r) → r) (prem) een deductie te construeren, geeft men het commando opa(g([i(f(a),o(f(p),f(q))),i(f(b),i(f(p),f(r))),f(a),n(i(f(b),i(i(f(q),f(r)),f(r))))], i(f(b),i(i(f(q),f(r)),f(r)),’voorbeeld.pl’). in de SWI-prolog-console. Gebruik ‘copy’ en ‘paste’ uit de file flipo.txt. Gebruik steeds een teksteditor om OPA-commando’s te formuleren. Op deze regel kunnen we (ZeBe(1)) toepassen om te komen tot (2) a → (p ∨ q), b → (p → r), a ` b → ((q → r) → r) (ZeBe(1)) wat de eigenlijke uitdrukking is die we willen bewijzen. Deze regel moet in FLIPOsyntaxis aan de file voorbeeld.pl worden toegevoegd om tot een sluitend bewijs in FLIPO voor (2) te komen. Elke te bewijzen uitdrukking, zal voor OPA zo moeten geconstrueerd worden, zodanig dat manueel de laatste regel (ZeBe) kan worden toegevoegd zoals hierboven. Dit is waarschijnlijk een artefact van de prolog-omgeving, waarin FLIPO geprogrammeerd is. Mits verdere transformatie, kunnen we tot het formaat van een echte deductieregel komen. Voor meer uitleg hierover verwijzen we naar de file flipo.txt. Als OPA argumenten moeten we dus steeds iets van de vorm lijst, ¬formule ` formule construeren. Open en bekijk het aangemaakte tekstbestand voorbeeld.pl. Samen met opmerking 4.1 is men nu in staat om de volgende vrijblijvende extra opdracht uit te voeren: vervolledig het javaprogramma uit sectie 3, om een volledig automatisch bewijsvoeringssysteem voor PROPC te bekomen. Eventueel kan een ‘Tarski’s World’-achtige look gebruikt worden voor de invoer.
10
5.4
Sytaxis van FLIPO-tekstbestanden
Een propositie of lijst van proposities wordt op de volgende manier geschreven: p α L L1
f (p) f (alf a) l(lijst) l(lijst1)
De logische connectieven zijn de volgende: p∧q p∨q p→q p↔q ¬p p, q L, p
a(f (p), f (q)) o(f (p), f (q)) i(f (p), f (q)) e(f (p), f (q)) n(f (p)) [f (p), f (q)] [l(lijst), f (p)]
f (p) & f (q) f (p) v f (q) f (p) − −− > f (q) f (p) < − − − > f (q) ∼ f (p)
α∧β α∨β α→β α↔β ¬α α, β L, α
a(f (alf a), f (beta)) o(f (alf a), f (beta)) i(f (alf a), f (beta)) e(f (alf a), f (beta)) n(f (alf a)) [f (alf a), f (beta)] [l(lijst), f (alf a)]
f (alf a) & f (beta) f (alf a) v f (beta) f (alf a) − −− > f (beta) f (alf a) < − − − > f (beta) ∼ f (alf a)
En met P , Q formules uit de bovenstaande lijst of onderstaande lijst P ∧Q P ∨Q P →Q P ↔Q ¬P
a(P, Q) o(P, Q) i(P, Q) e(P, Q) n(P )
P P P P ∼
&Q vQ − −− > Q <−−−> Q P
Extra opgave: stel de syntaxis van een wff in FLIPO recursief op in BNF notatie. Een regel in een bewijs heeft ´e´en van de volgende vormen: (1) p, q ` r (prem) (3) p ` p (A) (5) p ` q (R(1, 2))
s(1, [f (p), f (q)], f (r), prem). s(3, [f (p)], f (p), regel(0 A0 )). s(5, [f (p)], f (q), regel op(0 R0 , [1, 2])).
Een FLIPO-bewijs is een opeenvolging van regels in een tekstbestand. Bekijk bvb de tekstfile snede.pl. De naamgeving van de regel op regels, is dezelfde als deze van in de cursus. Ze kan ook worden nagegaan in het tekstbestand d regels.pl. Daar kunnen ook regels worden toegevoegd. Pas hiermee op! U kan uw eigen kopij van d regels.pl inconsistent maken, zodanig dat alles bewijsbaar wordt3 . Dit is niet de bedoeling, en is ook zinloos, vermits de gewenste functionaliteit (nagaan van bewijzen in PROPC ) verdwenen is. Voeg dus enkel regels toe die reeds bewezen zijn in PROPC . 3
Ex contradictione sequitur quodlibet, uit een contradictie kan men alles afleiden.
11
6
Oefeningen op het Gebruik van FLIPO
Over FLOBES: 1. Schrijf de bewijzen uit sectie 3 in FLIPO-notatie, in de gekozen teksteditor, en voer ze in FLIPO (FLOBES) in. 2. Zijn er bewijzen incorrect? 3. Zoek de fouten, indien deze er zijn, verbeter en voer opnieuw in FLIPO in. 4. Wat is de complexiteit van het algoritme voor verificatie? Over OPA: 1. Gebruik OPA of het eigen geschreven javaprogramma, om de bewijzen uit sectie 3 te genereren. 2. Bekijk het resultaat. Wat zijn de verschillen? 3. Waardoor ontstaan deze verschillen (als ze er zijn)? 4. Zijn de verschillen belangrijk? 5. Wat is de complexiteit van het algoritme voor een deductie? 6. Bekijk de file flipo.txt. Om een volledig correcte deductieregel uit OPA te verkrijgen moeten we nog een aantal regels toevoegen. Verklaar.
7
Eerste Project • Het eerste project voor Formele Logica is beschikbaar! • Doelstelling : uitdiepen van de betekenis van waarheidstabellen, kennismaken met de uitdrukkingskracht van PROPC en vertrouwd worden met FLIPO-bewijzen. • Op het examen zal ook FLIPO gebruikt worden, maar dan voor PREDΣ bewijzen. • Men maakt zich best nu vertrouwd met FLIPO, nu het nog eenvoudig is. • De opgaven maken enkel gebruik van PROPA en PROPC , en men kan alle opgaven herformuleren naar het opstellen van een model, of het geven van een deductie. • Het project is beschikbaar op http://cage.ugent.be/~svlangen/Academic/Logica/Logica2003-2004/ Project1Prop.pdf. • Vragen kunnen in de les of op het forum van Claroline gesteld worden.
12
