SLD-resolutie en Herbrandmodellen

Achtergrond

In het vorige college hebben we algemene resolutie behandeld voor clausules en we hebben gezien dat iedere predicaatlogische formule "herschreven" kan worden naar een conjunctie van clausules, waarbij inconsistentie bewaard blijft. Resolutie heeft nog erg veel keuze momenten (welke literals van welke clausules moeten we met elkaar unificeren om een resolutiestap te doen?) waardoor het in de praktijk niet erg bruikbaar is. Daarom beperkt men zich meestal tot logische programma's (bestaande uit een rij logische clausules) waar dan 1 doel bij gestopt wordt om inconsistentie te bewijzen.
Deze vorm van resolutie heet logisch programmeren en computer systemen als Prolog zijn ervoor gemaakt om hiermee te werken. Bij logisch programmeren zijn er nog steeds keuzes te maken. SLD resolutie is een vorm van resolutie die de keuzes op een vaste manier voorschrijft, volgens een rekenregel en een zoekregel.

In dit college bestuderen we SLD resolutie: hoe het algoritmisch werkt en de keuzes die ermee gemoeid zijn. Een belangrijk begrip is de SLD boom, die op een samenhangende manier alle mogelijke SLD resoluties beschrijft (gegeven een zoekregel). Daarnaast bekijken we Herbrand modellen van logische programma's. Deze modellen worden gebruikt om de volledigheid van SLD resolutie aan te tonen: "Als S u {~A} inconsistent is, dan is er een succesvolle SLD afleiding van S u{~A}". (De correctheid van resolutie hebben we al in een eerder college bewezen.)

Leerdoel

Na het voltooien van deze taak kunt u

• onderstaande kernbegrippen (zie 'Instructie') hanteren
• SLD resolutie, zoekregel, rekenregel en SLD afleiding
• SLD boom, succes tak, faal tak en oneindige tak
• Herbrand universum en Herbrand model
• Minimaal Herbrand model

Instructie

1. Lees de stukken van hoofdstuk 16 van "Logica voor Informatici (3de editie)" over SLD resolutie en Herbrand modellen. Lees ook het aanvullende collegedictaat.
   (Optioneel: de slides van Ramakrishnan geven een alternatieve presentatie en een methode om het kleinste Herbrand model uit te rekenen). Kernbegrippen:
   • SLD resolutie
   • SLD boom
   • Herbrand model
2. Maak de bijgeleverde opgaven

Product

• SLD afleidingen en een gestructureerde SLD boom met bij iedere succestak de bijbehorende antwoordsubstituties.
• Beschrijving van de minimale Herbrand modellen in opgave 3 dmv een plaatje + verantwoording dat dit de minimale Herbrand modellen zijn.
• Bij de modellen en de interpretaties in opgave 4 duidelijke uitleg dat het een model van S is (in 4.3) en dat A in M geldt (in 4.4).

Reflectie

• Zijn uw SLD afleiding en SLD boom overzichtelijk. Is uw SLD boom volledig? Wordt de juiste rekenregel toegepast? Wat zijn de antwoordsubstituties?
• Zijn uw minimale Herbrand modellen echt minimaal? Zijn het wel modellen van S?