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

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:
  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

Reflectie