Leertaak 11

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 de rest van hoofdstuk 16 van "Logica voor Informatici (3de editie)", behalve 16.6, 16.7 en 16.8 t/m Stelling 16.2 Lees ook het stuk over "prenex vormen" (blz 125). Kernbegrippen:
  2. Maak de opgaven in de bijlage.

Product

Reflectie