Sammanfattning vecka 2 av lektion och övning:

Jag gick igenom hur unifieringsalgoritmen som sköter likhetsteorin fungerar och vad program "betyder" deklarativt ("modellteorin").

Prolog arbetar med bevisregeln Modus Ponens, dvs att använda implikation i ett bevis och unifiering av logiska variabler. Tillsammans kallas denna metod för bevisföring för SLD-resolution.

Unifieringsalgoritmen genererar likheter som behövs för att det man frågar efter skall kunna bevisas.

När man beskriver detta tala man om "substitutioner", en avbildning av variabler till deras värden.

Detta kallas också "bindningsomgivning" och är de "värden" som man får vid en exekvering.

OBS att substitutioner är ett sätt att beskriva vad programmet gör, och inte hanteras explicit i program.

Exempel på program togs upp där unifiering är särskilt viktigt:

- familjerelationer med strukturerad information om individerna.

- Zebraproblemet

Lägg gärna in era frågor om övningsuppgifter i denna tråd, så ser fler som kanske har samma funderingar vpr diskussion. Det går också bra att skicka epost till mig så svarar jag så fort jag hinner.

- Thomas