Hoorcolleges Inleiding Logica voor CKI

hoorcollege 15 (maandag 31 oktober 2011)

hoorcollege 14 (woensdag 26 oktober 2011)

• geldigheid, vervulbaarheid, strijdigheid
• de voor-alle introductie en eliminatie regels

hoorcollege 13 (maandag 24 oktober 2011)

1. interpretatie van 0-, 1- en meerplaatsige predikaten
2. interpretatie van de variabele
3. recursieve definitie van de interpretatiefunctie
4. voorbeelden

hoorcollege 12 (woensdag 19 oktober 2011)

1. de notie van signatuur
2. de officiële definitie van de taal
3. constructieboom
4. voorkomen
5. bereik van een kwantorvoorkomen
6. binding
7. substitutie

hoorcollege 11 (maandag 17 oktober 2011)

1. bespreking tussentoets; punten staan online.
2. demonstratie van tool (zie practicumpagina) om een eenvoudige wereld te maken en daarop de waarheid van predikaatlogische formules te bepalen;
3. modelleren in/programmeren met predikatenlogica: Prolog. twee voorbeeldprogramma's, voorouder.pl en hanoi.pl en demonstratie in swipl.

hoorcollege 10 (woensdag 12 oktober 2011)

hoorcollege 9 (maandag 10 oktober 2011)

hoorcollege 8 (woensdag 5 oktober 2011)

• voorbeeld van een formule (A of niet A) waarop (mijn) yices weliswaar sat als antwoord geeft, maar geen waarde aan A toekent. Dit is geen bug, maar het betekent dat de waarde die aan A toegekend wordt er niet toe doet (wbt vervulbaarheid).
• Enige voorbeelden van natuurlijke deductie afleidingen (geinspireerd door de equivalenties op blz. 74).
• Heuristiek bij het geven van ND bewijzen: aannames zover mogelijk opsplitsen m.b.v. eliminatie regels, af te leiden conclusie zover mogelijk opsplitsen m.b.v. introductie regels, en deze op elkaar proberen te laten passen (Hoofdstuk 9, zie daar voor meer heuristieken)
  (heuristiek werkt niet altijd, i.h.b. niet indien RAA nodig is).
• Correctheid- en volledigheidsstelling van het natuurlijke deductie bewijssysteem t.o.v. semantisch gevolg (Hoofdstuk 10). Gebruik van deze stelling om vragen over niet afleibaarheid te beantwoorden d.m.v. een tegenmodel, d.w.z. door te laten zien dat de conclusie geen semantisch gevolg is van de aannames.
• Slides.

hoorcollege 7 (maandag 3 oktober 2011)

• Toetsstof: in principe de gehele propositielogica syllabus en inductieve en recursieve definities uit de inductie syllabus. Actief te beheersen: stof waarmee geoefend is. Passief te beheersen: de rest.
  (Nadere specificatie volgt eind deze week.)
• Natuurlijke deductie, afleidingsbomen, afleidbaarheid, introductie- en eliminatieregels, intrekken van 0,1 of meer hypothesen, regelschema's per connectief, en eerste voorbeelden van afleidingen (Hoofdstuk 9).
• Slides.

hoorcollege 6 (woensdag 28 september 2011)

• Bespreking van inleveropgaven, algemene punten:
  • positieve binaire getallen PB als gedefinieerd door clausules (i) 1 in PB; (ii) als p in PB dan p0 in PB; (iii) als p in PB dan p1 in PB. er zijn ook vele alternatieven, b.v. zou clausule (iii) vervangen kunnen worden door (iii)' als p,q in PB dan pq in PB.
    Inductieve definities en recursie vormen de basis voor functioneel programmeren (b.v. Haskell (in het 2de jaar van CKI te volgen)), en ook voor moderne bewijscheckers zoals Coq.
  • voorbeeld van een veel gemaakte fout: V((p en q)) = V((1 en q)) als V(p) = 1. Dit is niet juist: het mengt semantiek (de waarheidswaarde 1) met syntax (de formule (... en q)). Correct is V((p en q)) = min(V(p),V(q)) = min(1,V(q)) = V(q) als V(p) = 1.
  • geef bij de practicumopgaven een goede toelichting. maak daarin expliciet een koppeling tussen de uitvoer van het tool en de opgave. dus zet niet `dus het is een tautologie' onder de tabel, maar zeg iets als `we zien in de nde kolom dat de waarheidstafel van de formule een 1 heeft voor alle mogelijke inputs, dus is de formule een tautologie'.
• Slides.
• Substitutie (syntactische verandering) en substitutiestelling (syntactische verandering heeft geen semantische verandering tot gevolg).: vervanging door een equivalente formule. (Hoofdstuk 7, Sectie 3.4)
• Functionele volledigheid: ieder (waarheidsdefiniet) connectief kan gerepresenteerd worden door een formule, dwz een formule die dezelfde waarheidstafel heeft, door iedere rij waar de waarheidstafel een 1 heeft te beschrijven (mbv een conjunctie van de waarheidswaarden van de propositievariabelen in die rij) en daar de disjunctie van te nemen. (Hoofdstuk 7, Sectie 4.1)
• De formule die het bovenstaande proces oplevert, is een formule in disjunctieve normaalvorm (dnv) (disjunctie van conjuncties van literals, waarbij een literal een propositionele variabele of een negatie daarvan is). (Hoofdstuk 7, Sectie 4.2)
• Equivalenties waarmee je iedere formule naar dnv kunt omschrijven. (Hoofdstuk 7,Stelling 3.12) Dualiteit: equivalenties uitgedrukt alleen m.b.v. conjunctie, disjunctie, negatie (en evt. falsum en verum) blijven behouden onder `op z'n kop zetten.
• Conjunctieve normaalvormen (cnv) vormen de basis voor logisch programmeren in Prolog (later in het 1ste jaar van CKI te volgen); de wereld wordt `beschreven' m.b.v. een conjunctie van clauses, die zelf bestaan uit disjuncties van literals.

hoorcollege 5 (maandag 26 september 2011)

• Slides.
• eerste informele voorbeelden van bewijzen met inductie (komt later nog terug, ook formeler in de nog te plaatsen uitbreiding van de inductie syllabus)
  • bewijs met inductie dat 1+...+n = n(n+1)/2
  • bewijs met inductie dat het aantal haakjes in een formule altijd even is
• semantisch gevolg

hoorcollege 4 (woensdag 21 september 2011)

• Overzicht van stof tot dusverre in een paar Slides.
• Berekening van de waarheidswaarde V(A) van een formule A door stapsgewijs uitrekenen mbv recursieve definitie, b.v. V((p en niet p)) = min(V(P),V(niet p)) = min(V(p),1-V(p)) = 0 (want ofwel V(p) = 0, ofwel V(p) = 1 en dan 1-V(p) = 0) (Hoofdstuk 7, sectie 1).
• Waarheidsdefiniet of niet? (Hoofdstuk 6) Bespreking van `want' en `omdat' (de waarheidswaarde van `ik word nat omdat het regent' als ik binnen ben maar onder de douche sta). (Hoofdstuk 6 sectie 1.7) Bespreking van probleem met analyseren van `ooit regent het' als ooit(het regent) (komt pas terug in Logica voor AI).
• Valuatie V opgevat als wereld(beschrijving). V maakt A waar, notatie V |= A. Bepaald zijn van de waarheidswaarde van formules door de waarheidswaarde van hun propositionele variabelen (Hoofdstuk 7,sectie 2).
• Tautologie, contingent, en tegenspraak/contradictie (Hoofdstuk 7,sectie 3.3).
• Vervulbaarheid (satisfiability, Hoofdstuk 7,sectie 3.1). Het omzetten van de vraag of iets een tautologie is of een tegenspraak naar een vervulbaarheidsprobleem. Coderen van puzzles als vervulbaarheidsprobleem met als voorbeeld sudoku's.

hoorcollege 3 (maandag 19 september 2011)

• Syntax: alfabet, taal, afleidingsbomen
• Van syntax naar semantiek: recursieve functies, uit te rekenen mbv afleidingsboom
• Waarheidstafels
• Slides van het college.

hoorcollege 2 (woensdag 14 september 2011)

• Logistiek: inleveropgaven dienen iedere week op maandag voor het hoorcollege ingeleverd te worden, op papier, in de daarvoor bestemde dozen/mappen bij het hoorcollege.
• Falsum en dan-en-slechts-dan-als, informele uitleg.
• Syntax vs. semantiek. Vorm vs. betekenis.
• Syntax: de verzameling van formules (lees Hoofdstuk 2 van de syllabus voor verzameling notatie)
• Slides van het college.
• Syntax: de inductieve definitie van de verzameling formules (lees Hoofdstuk 4 van de syllabus en de inductie syllabus)

hoorcollege 1 (maandag 12 september 2011)

• Opzet van de cursus, logistiek, organisatie in het algemeen (gereflecteerd in deze site).
• Plaatsing van Inleiding Logica binnen het CKI curriculum.
• Slides van het college.
• Proposities (Hfdstk 3 uit syllabus).
• Formules als opgebouwd mbv logische connectieven: conjunctie (... en... ), disjunctie (... of...), implicatie (als ... dan ...), negatie (niet ...).
  (Vooralsnog informeel, zie alvast Hfdstk 4 uit syllabus).
• Informele bespreking van (geldige) redeneringen, en voorbeeld (zie slides) van het vertalen van een whodunnit (in natuurlijke taal) naar formules (in de taal van propositielogica).
• Illustratie van het oplossen van de whodunnit met behulp van het programma yices.
  Nota bene: yices is een zeer geavanceerd tool en in eerste instantie gericht op het gebruiken van logica, niet op het leren van logica. Het dient voor het moment slechts ter illustratie van de slogan `rekenen met waarheid'.
• Illustratie van het checken van de predikaatlogische redenering socrates met behulp van het programma prover9.
  Nota bene: niet alleen is ook prover9 een geavanceerd tool, maar dit voorbeeld maakt ook gebruik van predikaatlogica, iets dat pas in de tweede helft van de cursus aan bod zal komen. Dus ook dit voorbeeld dient voor het moment slechts ter illustratie van de automatisch redeneer vaardigheden van tools.

collegeweek   1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10