Sammanfattning vecka 3, lektion och övning

Repetition av modellteorin för prolog.

Lite repetition om bevisteorin för logikprogrammering, sökträd, bevisträd, bevis. SLD-resolution.

sundhet (allt man kan bevisa är sant) och fullständighet (allt sant kan bevisas) hos SLD-resolution.

Vad händer om SLD-trädet är oändligt? Svar: vi tappar fullständigheten i normalfallet, dvs det kan finnas lösningar som vi inte hittar pga att prologinterpretatorn loopar i en annan gren.

Programmering med träd och listor.

spegelpredikatet mirror(T1,T2) där T2 är en spegelbild av T1 och omvänt.

ATt implementera ett "dictionary" med hjälp av ett partiellt instanterat binärt träd.

append(L1,L2,L), olika användningar, sätta samman listor, ta isär listor, flera lösningar möjliga.

Hitta sista elementet i en lista, last(L,E).

Ta bort duplikat ur en lista.

Sortering av listor med (not so) quicksort.

Exempel med hur man använder listor för att representera mängder.

Invarianter:

- listan är unik, dvs. inget element förekommer mer än en gång,

- listan är sorterad.

Att slå ihop två sorterade listor så att resultatet fortsatt är sorterat, predikatet merge(L1,L2,L).

Skapa predikatet union för mängder representerade av unika och sorterade listor.

Räkneövningen fortsätter att excersera med listor och träd.