diff --git a/logic_programming/5_SLD.ipynb b/logic_programming/5_SLD.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..2f8f70264001303f9d1f465b308a5344f5eb9c93
--- /dev/null
+++ b/logic_programming/5_SLD.ipynb
@@ -0,0 +1,574 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "id": "9eb5530a",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "source": [
+ "# Linear Resolution and SLD Resolution\n",
+ "\n",
+ "```Horn clauses``` are clauses (i.e., disjunctions of literals) with at most one positive literal.\n",
+ "A ```query``` or denial is a Horn clause without positive literal.\n",
+ "A ```fact``` is a Horn clause consisting of one positive literal and no negative literals.\n",
+ "\n",
+ "Note that the CNF of our knights and knaves puzzle, contains one query, no facts and\n",
+ " two non-Horn clauses ```B ∨ A``` and ```C ∨ A```:\n",
+ "```\n",
+ "{¬A ∨ ¬B ∨ ¬C, B ∨ A, C ∨ A, ¬B ∨ A, ¬A ∨ B}\n",
+ "```\n",
+ "\n",
+ "Note that Prolog programs are automatically Horn clauses in CNF.\n",
+ "For example, the Prolog clause\n",
+ "```\n",
+ "wet :- rains, outside.\n",
+ "```\n",
+ "\n",
+ "corresponds to the Horn clause:\n",
+ "\n",
+ "```\n",
+ "wet ∨ ¬rains ∨ ¬outside\n",
+ "```\n",
+ "\n",
+ "The head of a Prolog clause is a positive literal. The calls in the body correspond to negative literals.\n",
+ "\n",
+ "Querys are not Prolog program clauses but stem from the Prolog console."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "1eb3920b",
+ "metadata": {},
+ "source": [
+ "Let us now encode a simple Prolog program using the representation from the previous notebook:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "id": "964ebd52",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ ":- discontiguous program/3.\n",
+ ":- dynamic program/3.\n",
+ "program(1,'weather',\n",
+ " [ [pos(wet),neg(rains),neg(outside)],\n",
+ " [pos(rains)],\n",
+ " [pos(outside)] ]).\n",
+ "negate(pos(A),neg(A)).\n",
+ "negate(neg(A),pos(A))."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "a4dc903e",
+ "metadata": {},
+ "source": [
+ "For simplicity we will assume that the positive literal is always the first literal in a clause.\n",
+ "\n",
+ "Let us now perform resolution with a negative literal:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "id": "26e0221b",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ "resolve_literal(neg(Prop),Clauses,Resolvent) :-\n",
+ " member([pos(Prop)|Body],Clauses), % find a clause with a corresponding positive literal\n",
+ " Resolvent=Body."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "fc6823ad",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "source": [
+ "This can be used like this:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "id": "152289b6",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mP = [[pos(wet),neg(rains),neg(outside)],[pos(rains)],[pos(outside)]],\n",
+ "Resolvent = [neg(rains),neg(outside)]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- program(1,_,P),resolve_literal(neg(wet),P,Resolvent)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "68fd6059",
+ "metadata": {},
+ "source": [
+ "Here we find a contradiction:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "id": "2c3dd1bf",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mP = [[pos(wet),neg(rains),neg(outside)],[pos(rains)],[pos(outside)]],\n",
+ "Resolvent = []"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- program(1,_,P),resolve_literal(neg(rains),P,Resolvent)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "07785e91",
+ "metadata": {},
+ "source": [
+ "We can extend this code to work with a complete denial, rather than single negative literal:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "id": "33fc6271",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ "resolve_query(Query,Clauses,Resolvent) :-\n",
+ " selection_rule(Query,SelectedLiteral,RestQuery),\n",
+ " resolve_literal(SelectedLiteral,Clauses,Body),\n",
+ " append(Body,RestQuery,Resolvent).\n",
+ "\n",
+ "selection_rule([LeftmostLiteral|Rest],LeftmostLiteral,Rest)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "1d426bb1",
+ "metadata": {},
+ "source": [
+ "The above predicate uses the predicate ```select/3``` from ```library(lists)```, which can be used to select an element from a list and returns a modified list with the element removed:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "id": "f2a8b4a4",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mP = [[pos(wet),neg(rains),neg(outside)],[pos(rains)],[pos(outside)]],\n",
+ "Resolvent = [neg(rains),neg(outside)]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- program(1,_,P),resolve_query([neg(wet)],P,Resolvent)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "cba18c66",
+ "metadata": {},
+ "source": [
+ "As you can see, the resolvent is again a query consisting only of negative literals.\n",
+ "We can apply resolution again:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "id": "06aa608c",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mP = [[pos(wet),neg(rains),neg(outside)],[pos(rains)],[pos(outside)]],\n",
+ "Resolvent = [neg(outside)]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- program(1,_,P),resolve_query([neg(rains),neg(outside)],P,Resolvent)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "4c71d8af",
+ "metadata": {},
+ "source": [
+ "As you can see, the resolvent is again a query consisting only of negative literals.\n",
+ "We can apply resolution again:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "id": "a76d8b5d",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mP = [[pos(wet),neg(rains),neg(outside)],[pos(rains)],[pos(outside)]],\n",
+ "Resolvent = []"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- program(1,_,P),resolve_query([neg(outside)],P,Resolvent)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "4d9ecefc",
+ "metadata": {},
+ "source": [
+ "We have now reached the empty clause, i.e., a contradiction.\n",
+ "This means that the original proposition wet is a logical consequence of our logic program."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "e67981b4",
+ "metadata": {},
+ "source": [
+ "We can now try to encode the search for a contradiction systematically as follows:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "id": "d7a0cc62",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ "prove(Proposition,Clauses) :-\n",
+ " find_contradiction([neg(Proposition)],Clauses).\n",
+ "\n",
+ "find_contradiction([],_). % empty clause found\n",
+ "find_contradiction(Query,Clauses) :-\n",
+ " resolve_query(Query,Clauses,NewQuery),\n",
+ " find_contradiction(NewQuery,Clauses)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "2b2ea192",
+ "metadata": {},
+ "source": [
+ "Let us now check whether wet is a logical consequence of program 1:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "id": "78163b60",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mClauses = [[pos(wet),neg(rains),neg(outside)],[pos(rains)],[pos(outside)]]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- program(1,_,Clauses), prove(wet,Clauses)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "a70dbafb",
+ "metadata": {},
+ "source": [
+ "There are a few important observations:\n",
+ "- negative literals always come from the query\n",
+ "- positive literals always come from the program clauses\n",
+ "- the resolve_literal predicate can have multiple solutions\n",
+ "- the clauses in the logic program (```Clauses``` above) are never changed. \n",
+ "The last point means that there is no exponential growth of the number of clauses during execution and it means we can precompile the logic program to find clauses for the given positive literals.\n",
+ "\n",
+ "This procedure is called linear resolution, as the pool of clauses remains of constant size\n",
+ "and we \"forget\" earlier denials, except for backtracking when no contradiction is found.\n",
+ "\n",
+ "The above code also contains a so-called selection rule/function ```selection_rule```.\n",
+ "This one selects the next literal chosen for resolution in the query.\n",
+ "- it is a function: no backtracking is needed\n",
+ "- there is an important property, called \"independence of the selection function\" which stipulates that it is correct to not backtrack\n",
+ "- Prolog's execution engine uses the leftmost literal by default; we have done the same above\n",
+ "\n",
+ "The procedure we have implemente is called SLD-resolution:\n",
+ "- Selection rule driven\n",
+ "- Linear resolution for\n",
+ "- Definite clauses\n",
+ "\n",
+ "(Definite clauses are clauses without using Prolog's negation operator. We will return to this later.)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "4759110b",
+ "metadata": {},
+ "source": [
+ "Let us augment the above procedure with a few print statements:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 25,
+ "id": "9d3fbd1a",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ "trace_prove(Prop,Clauses) :- trace_find_contradiction([neg(Prop)],Clauses,1).\n",
+ "trace_find_contradiction([],_,Nr) :- format(' ~w: [] (contradiction)~n',[Nr]). % empty clause found\n",
+ "trace_find_contradiction(Query,Clauses,Nr) :-\n",
+ " format(' ~w: ~w~n',[Nr,Query]), N1 is Nr+1,\n",
+ " resolve_query(Query,Clauses,NewQuery),\n",
+ " trace_find_contradiction(NewQuery,Clauses,N1)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 26,
+ "id": "a8ba5814",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ " 1: [neg(wet)]\n",
+ " 2: [neg(rains),neg(outside)]\n",
+ " 3: [neg(outside)]\n",
+ " 4: [] (contradiction)"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mClauses = [[pos(wet),neg(rains),neg(outside)],[pos(rains)],[pos(outside)]]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- program(1,_,Clauses), trace_prove(wet,Clauses)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "6cdeade5",
+ "metadata": {},
+ "source": [
+ "The above sequence of denials is also called an ```SLD-derivation```.\n",
+ "An SLD-derivation which ends in a contradiction is called an ```SLD-refutation```."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "d32921c9",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "source": [
+ "Let us examine a more complicated example corresponding to the Prolog program\n",
+ "\n",
+ "```\n",
+ "p :- q,r.\n",
+ "q :- t.\n",
+ "q :- s.\n",
+ "r.\n",
+ "s.\n",
+ "```"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 23,
+ "id": "26924712",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ "program(2,'Backtracking',[\n",
+ " [pos(p),neg(q),neg(r)],\n",
+ " [pos(q),neg(t)],\n",
+ " [pos(q),neg(s)],\n",
+ " [pos(r)],\n",
+ " [pos(s)]\n",
+ " ]) :- true."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "17dd1525",
+ "metadata": {},
+ "source": [
+ "If we now try to prove that ```p``` is a logical consequence of program 2 we will see that backtracking is required:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 28,
+ "id": "7d90c4ad",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ " 1: [neg(p)]\n",
+ " 2: [neg(q),neg(r)]\n",
+ " 3: [neg(t),neg(r)]\n",
+ " 3: [neg(s),neg(r)]\n",
+ " 4: [neg(r)]\n",
+ " 5: [] (contradiction)"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mClauses = [[pos(p),neg(q),neg(r)],[pos(q),neg(t)],[pos(q),neg(s)],[pos(r)],[pos(s)]]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- program(2,_,Clauses), trace_prove(p,Clauses)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "b4b28da4",
+ "metadata": {},
+ "source": [
+ "By putting the above queries into a tree we obtain a so-called ```SLD-tree``` for the program and top-level query under consideration."
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "Prolog",
+ "language": "prolog",
+ "name": "prolog_kernel"
+ },
+ "language_info": {
+ "codemirror_mode": "prolog",
+ "file_extension": ".pl",
+ "mimetype": "text/x-prolog",
+ "name": "Prolog"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}