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
Product
Reflectie