Algemene resolutie en "normalizatie" van formules

Achtergrond

In het vorige college hebben we propositionele resolutie behandeld en unificatie. Dit laatste is belangrijk bij het definieren van de regel voor algemene resolutie die in de predicatenlogica gebruikt wordt. Hierbij worden een aantal negatieve literals in een clause geunificeerd met een aantal positieve literals in een andere clause, door middel van een most general unifier. Een eenvoudig geval hiervan is binaire resolutie waarbij 1 positieve literal met 1 negatieve literal geunificeerd wordt.
In het college hebben we ook de soundness (ook wel correctheid) van de resolutieregel aangetoond: als we met resolutie een tegenspraak afleiden uit S, dan is S ook echt inconsistent. Verder hebben we bekeken hoe algemeen "clausules" zijn als sub-klasse van formules uit de predicatenlogica. Daarbij zijn de begrippen prenex vorm, conjunctieve normaalvorm en Skolemizatie aan de orde gekomen. We hebben gezien dat iedere formule A kan worden herschreven tot een conjunctie van clausules B zodat geldt: A is inconsistent desda B is inconsistent.

Leerdoel

Na het voltooien van deze taak kunt u

Instructie

  1. Lees van "Logica voor Informatici (3de editie)": paragraaf 8.2 en paragrafen 16.5 en 16.9. Kernbegrippen:
  2. Bestaat er een resolutie bewijs voor:
    P(a,b), ∀x,P(x,c)\/~P(x,b), ∀x y z, P(y,z) \/ ~ P(x,y) \/ ~ P(x,z), ∀ x y z, P(z,x) \/ ~ P(x,y) \/ ~ P(y,z)
    Is er ook een oneindige loop? Als er geen bewijs bestaat, waarom niet? Wat nu als we ←P(c,a) toevoegen?
  3. Maak de opgaven in de bijlage.

Product

Reflectie