Clausules en Unificatie

Achtergrond

Het zou handig zijn als we logica zouden kunnen automatiseren, want dan kunnen we een computer vragen of een formule A uit een verzameling aannames G volgt. Voor de propositielogica kan dat: de propositielogica is beslisbaar, bijvoorbeeld met behulp van waarheidstabellen, maar de complexiteit hiervan is wel exponentieel (in het aantal propositionele variabelen). Predicatenlogica is onbeslisbaar zoals we later in het college nog in iets meer detail zullen zien. (De verzameling afleidbare formules is recursief opsombaar.) Desalniettemin zou er voor predicatenlogica (of voor een fragment van de predicatenlogica) natuurlijk nog best een algoritme kunnen zijn dat in veel gevallen goed werkt.

In dit college bekijken we zo'n algoritme dat gebaseerd is op de resolutie regel. Resolutie werkt met zogenaamde clausules, formules van de vorm L1 \/ L2 \/ ... \/ Lk waarbij iedere Li een literal (atoom of negatie van een atoom) is. De variabelen in de Li vatten we op als universeel gequantificeerd. Om resolutie toe te passen hebben we unificatie nodig: het vinden van een (zo algemeen mogelijke) substitutie s die twee formules A en B 'aan elkaar gelijk maakt' (door een substitutie van de vrije variablen volgens s).

Leerdoel

Na het voltooien van deze taak kunt u

• onderstaande kernbegrippen (zie 'Instructie') hanteren;
• uitleggen wat het basisprincipe van resolutie is
• resolutieafleidingen in de propositie logica maken
• van termen de mgu (most general unifier) bepalen

Instructie

1. Lees de slides en p. 243-252 van "Logica voor Informatici (3de editie)", dwz de secties 16.1 (inleiding), 16.2 (kennisrepresentatie met logische programma's), 16.3 (bewijzen als programmaverwerking), 16.4 (propositionele resolutie), 16.5 (unificatie en resolutie) alleen het stuk over unificatie.
   Deze informatie is ook te vinden in Ch7 van Reeves and Clarke. Kernbegrippen:
   • Clausule, Horn Clausule, Programma Clausule, Feit, Doel,
   • resolutie regel voor de propositielogica
   • weerlegging(sboom)
   • antwoordsubstitutie, unificatie, unificeerbaar
   • unificatie algoritme, most general unifier
2. Voer de opdrachten in de bijlage uit.
3. Waarom mogen we niet twee verschillende atomen tegelijk verwijderen?
   Dus, waarom niet: uit p,q← en ←p,q concluderen we ←.

Product

• Bij 2: voor het speciale geval een formele logische afleiding en voor het algemene geval een logisch gefundeerde redenering dat het klopt.
• Bij 3: resolutieafleidingen
• Bij 4: een uitwerking van hoe je aan de mgu (of "fail") komt

Reflectie

• Welke formules in 3 zijn clausules, welke programma clausules, welke zijn Horn clausules, welke zijn doelen, welke zijn `feiten'?
• Hebt u in 3 de resolutieregel goed toegepast? Kunt u de resolvent aanwijzen?
• Heeft u bij 4 duidelijk het unificatie algoritme stapsgewijs toegepast? Kunt u bij iedere stap aanwijzen welk geval van het unificatie algoritme u gebruikt?