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

• onderstaande kernbegrippen (zie 'Instructie') hanteren
• de methode van algemene resolutie gebruiken
• van formules de conjunctieve normaalvorm en de prenex normaal vorm bepalen.
• formules Skolemizeren
• bewijzen dat Skolemizatie inconsistentie bewaart

Instructie

1. Lees van "Logica voor Informatici (3de editie)": paragraaf 8.2 en paragrafen 16.5 en 16.9. Kernbegrippen:
   • Prenex vorm en conjunctieve normaalvorm (een tool)
   • Skolemizatie
   • Binaire en algemene resolutie
   • Antwoordsubstitutie
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

• Antwoorden op bovenstaande vraag en de vragen uite de bijlage, in het bijzonder:
• Weerleggingsbomen en antwoordsubstituties die verkregen zijn volgens de resolutieregel. Het moet duidelijk zijn hoe uw oplossing stapsgewijs verkregen wordt.
• Universele clausules en het proces dat aangeeft hoe deze uit de oorspronkelijke formules verkregen zijn waarbij duidelijk de stappen Skolemizatie, prenex normaal vorm en conjunctieve normaalvorm onderscheiden zijn.
• Helder gestructureerde bewijzen die blijk geven dat u de definities juist kunt hanteren.

Reflectie

• Zijn uw stapsgewijze beschrijvingen van de oplossingen zo duidelijk dat ze zo op een ander voorbeeld toegepast zouden kunnen worden?
• Vindt u uw eigen bewijzen overtuigend? En uw medestudenten?