Overzicht colleges Logica en Modelleren najaar 2011

Deze pagina wordt elke maandag en woensdag na het college bijgewerkt en vermeldt dan welke stof is behandeld. Voor de rest is het niet meer dan een prognose die nog zo nu en dan zal worden bijgesteld.

Hoorcollege 5 september:

• Opfrissen propositielogica (zelf doen!):
  • formules
  • begrippen tautologie (valid formula), contradictie, contingentie
  • Semantische implicatie en semantische equivalentie
       Slides over semantische implicatie: [LG]

    NB: Dit zijn bekende begrippen: kennis van de propositielogica uit het college Logische Structuren wordt bekend verondersteld!

• Natuurlijke deductie voor de propositielogica,
  Hoofdstuk 1 tot aan paragraaf 1.2.4, pagina 29
     NB: Nog niet behandeld: regel voor disjunctie eliminatie, LEM en PBC.
     Slides over natuurlijke deductie: [ND]
  

Hoorcollege 7 september:

• Natuurlijke deductie voor de propositielogica, vervolg
  • Eliminatie van disjunctie
  • LEM en PBC
  • Afgeleide regels
• Correctheids- en volledigheidsstellingen voor de propositielogica:
  

  φ₁, ... ,φ_n |− ψ   ⇔   φ₁, ... ,φ_n |= ψ

• Correctheid van natuurlijke deductie (soundness, theorem 1.35), (Par. 1.4.3, nog zonder bewijzen)
• Volledigheidsstelling (Par. 1.4.4, zonder bewijzen)

Hoorcollege 12 september:

• Natuurlijke deductie met ProofWeb
  Na een korte klassikale kennismaking met ProofWeb in M-607 gaan we aan de slag in de computerzalen S-329 (groep A), S-345 (groep B) en S-353 (overloop)
  NB: Meld je aan voor het practicum door een mailtje aan tcs@cs.vu.nl met subject "proofweb" en in de tekst alleen je voor- en achternaam en vu-id. Doe het nu!

Hoorcollege 14 september:

• Syntax van de predikatenlogica: termen, formules, parse trees
• Bereik (scope) van een kwantor
• Gebonden en vrije variabelen
• Substitutie
• Natuurlijke deductie predikatenlogica
  De regels ∀e, ∃i en ∀i zijn behandeld; de regel ∃e nog niet.

Hoorcollege 19 september:

• Vervolg natuurlijke deductie predikatenlogica
  Slides natuurlijke deductie predikatenlogica (onder constructie): [ND-pred]
  
• Predikatenlogica in ProofWeb

Hoorcollege 21 september:

• Semantiek predikatenlogica
• Model, waarheid, geldigheid
• Geldigheid van semantische implicatie testen
  [voorbeeldslides modellen] [voorbeeldslide ongeldige gevolgtrekking] [voorbeeldslide geldige gevolgtrekking]

Hoorcollege 26 september:

• Eigenschappen van relaties
• Speciale modellen: getalstructuren
• Consistentie (vervulbaarheid, satisfiability)
  [Aantekeningen over consistentie]
• Kappersparadox
• Gelijkheid (=) in de predikatenlogica
• Uitdrukken van aantallen met behulp van =
• Vertalen met gelijkheid

Hoorcollege 28 september

• Betekenis van formules met en zonder vrije variabelen
• Eigenschappen uitgedrukt door formules met vrije variablen
• Vertalen voor gevorderden
• Gelijkheidsregels voor natuurlijke deductie (H&R, p. 107-109)
• Vooruitblik voortentamen

Hoorcollege 3 oktober:

• Modale logica: Hoofdstuk 5 tot en met par. 5.3.1

Hoorcollege 5 oktober:

• Modale logica: frames, geldigheid op frames
• Correspondentie tussen modale formules en frame-eigenschappen
• Weergave van modale eigenschappen in de predikatenlogica

Hoorcollege 10 oktober:

• Volledigheid en correctheid [slide Volledig- en Correctheidsstelling] (H&R, p. 136, (2.10))
• Consistentie (satisfiability, vervulbaarheid) versus syntactische consistentie [slide Consistentiestelling]
  

  NB: Een verzameling formules Γ heet "syntactisch consistent" als niet: Γ ⊢ ⊥
  Dus i.h.b. geldt dat {φ₁, ..., φ_n} syntactisch consistent als niet: φ₁, ..., φ_n ⊢ ⊥

• Compactheidstelling [slide Compactheidstelling] (H&R, p. 137, Thm. 2.24)
• Definieerbaarheid en ondefinieerbaarheid (H&R, Sectie 2.6)
• Ondefinieerbaarheid van het begrip eindig [slide 1] [slide 2] [aantekeningen]
• Bereikbaarheid via een binaire relatie R niet uitdrukbaar in de predikatenlogica [slide 1] [slide 2] (H&R, Thm. 2.27)

Hoorcollege 12 oktober:

• Post Correspondence Problem (PCP)
• Onbeslisbaarheid van de predikatenlogica
  [slides PCP] (Huth & Ryan Sectie 2.5)
  
  
• Programmaspecificatie met Hoare triples
• Toestanden (states) als look-up functies
• Totale en partiële correctheid
  (Huth & Ryan Hoofdstuk 4, tot aan Sectie 4.3)

Hoorcollege 17 oktober:

Een dergelijke tabel kunnen we op twee manieren zien als onderdeel van een model van de predikatenlogica:

• Relatiemodel
  De tabel representeert in dit voorbeeld een 5-plaatsige relatie Persons, er geldt bijvoorbeeld Persons(1, Hansen, Ola, Timoteivn 10, Sandnes), en zo voor elk van de drie rijen.

  Een query die vraagt naar de voornamen van personen die in Sandnes wonen, kunnen we dan formuleren als een formule in de predikatenlogica met één vrije variabele x:

  ∃y₁∃y₂∃y₃ Persons(y₁, y₂, x, y₃, Sandnes)

• Tuple-model
  De tabel kun je ook zien als een verzameling 5-tuples, zoals bijvoorbeeld <1, Hansen, Ola, Timoteivn 10, Sandnes>. Die verzameling geven we ook aan met het nu 1-plaatsige predikaat Persons. Voor elke kolom is er dan een corresponderende projectiefunctie, hier zijn dat P_Id, LastName, Firstname, Adress, City. De query wordt nu een formule met functiesymbolen (en natuurlijk nog steeds x als enige vrije variabele):

  ∃y (Persons(y) ∧ FirstName(y) = x ∧ City(y) = Sandnes)

• ∀z (∃y₁∃y₂∃y₃∃y₄ Persons(y₁, y₂, z, y₃, y₄) → ∃y₁∃y₂ (Chats(y₁, y₂, x, z) ∨ Chats(y₁, y₂, z, x)))
• ∀z (∃y (Persons(y) ∧ FirstName(y) = z) → ∃y (Chats(y) ∧ ((FirstName_1(y) = x ∧ FirstName_2(y) = z) ∨ (FirstName_1(y) = z ∧ FirstName_2(y) = x))))

Het resultaat van een query kan ook zelf weer een relatie zijn. We willen bijvoorbeeld weten welke personen x en y die in dezelfde stad wonen met elkaar gechat hebben. (We zijn weer alleen geïnteresseerd in de voornamen.) In respectievelijk het relatie- en het tuple-model kan dat met de volgende queries:

• ∃z (∃x₁∃x₂∃x₃ Persons(x₁, x₂, x, x₃, z) ∧ ∃y₁∃y₂∃y₃ Persons(y₁, y₂, y, y₃, z) ∧ ∃w₁∃w₂ Chats(w₁, w₂, x, y))
• ∃z (∃v₁ (Persons(v₁) ∧ FirstName(v₁) = x ∧ City(v₁) = z) ∧ (∃v₂ (Persons(v₂) ∧ FirstName(v₂) = y ∧ City(v₂) = z) ∧ (∃v₃ (Chats(v₃) ∧ FirstName_1(v₃) = x ∧ FirstName_2(v₃) = y)

Om verder te oefenen:

• Opgave 6 van het tentamen van 27 oktober 2010
• Dezelfde opgave, nu in het tuple-model

Hoorcollege 19 oktober:

• Onvolledigheidsstellingen (Gödel)
  
  
• Overzicht van de stof van het college
• Tentamenvoorbereiding
• Uitwerkingen van het tentamen van 27 oktober 2010