diff --git a/logic_programming/7_Unification.ipynb b/logic_programming/7_Unification.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..5d3c0ac869a02dc1bb8960c1336160558902ae9b
--- /dev/null
+++ b/logic_programming/7_Unification.ipynb
@@ -0,0 +1,657 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "id": "9eb5530a",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "source": [
+ "## Substitutions\n",
+ "\n",
+ "Substitution: mapping from variables to terms\n",
+ "\n",
+ "Notation: {X1/t1, …, Xn/tn}\n",
+ "\n",
+ "Examples: \n",
+ "{X/a} {X/b, Y/s(0)} {Y/Z} {}\n",
+ "\n",
+ "In Prolog we represent this as lists of bindings:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "id": "78764141",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ "is_subst([]).\n",
+ "is_subst([Var/Term|T]) :- variable(Var), term(Term), is_subst(T).\n",
+ "\n",
+ "variable('$VAR'(_)).\n",
+ "variable('X'). % a few artificial variables for easier reading\n",
+ "variable('Y').\n",
+ "variable('Z').\n",
+ "term(_)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "id": "b03ac6e7",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mtrue"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "\n",
+ "?- is_subst(['X'/a])."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "ab0d39bc",
+ "metadata": {},
+ "source": [
+ "Applying a substitution to a term or wff\n",
+ "Instantaneous replacement by right-hand sides\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "id": "f6f156a3",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ "% apply(Term,Subst,NewTerm)\n",
+ "apply(Var,Subst,Res) :- variable(Var), !,\n",
+ " (member(Var/New,Subst) -> Res=New ; Res=Var).\n",
+ "apply(Term,Subst,Res) :- Term =.. [Functor|Args],\n",
+ " l_apply(Args,Subst,NewArgs),\n",
+ " Res =.. [Functor|NewArgs].\n",
+ "\n",
+ "l_apply([],_,[]).\n",
+ "l_apply([Arg1|T],Subst,[NewArg1|NewT]) :- apply(Arg1,Subst,NewArg1),\n",
+ " l_apply(T,Subst,NewT)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "id": "c675dc2a",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mRes = p(a)"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- apply(p('X'),['X'/a],Res)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "id": "9639129f",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mRes = f(a,b,$VAR(2),c,a)"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- apply(f('X',b,'Y',c,'X'),['X'/a],Res)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 19,
+ "id": "a36930e8",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mRes = f(Y,X)"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- apply(f('X','Y'),['X'/'Y','Y'/'X'],Res)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "c2f4b9a9",
+ "metadata": {},
+ "source": [
+ "A substitution s is called a unifier of two terms (or wff’s) A and B iff As = Bs\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 18,
+ "id": "5a3f584e",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mS = [X/a],\n",
+ "Res1 = p(a),\n",
+ "Res2 = p(a)"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- S=['X'/a],\n",
+ " apply(p('X'),S,Res1),\n",
+ " apply(p(a),S,Res2)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 20,
+ "id": "5290b75d",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mS = [X/Z,Y/Z],\n",
+ "Res1 = p(Z,Z),\n",
+ "Res2 = p(Z,Z)"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- S=['X'/'Z', 'Y'/'Z'],\n",
+ " apply(p('X','Y'),S,Res1),\n",
+ " apply(p('Z','Z'),S,Res2)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 23,
+ "id": "347e1997",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mS = [X/s(X)],\n",
+ "Res1 = p(s(X)),\n",
+ "Res2 = p(s(s(X)))"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- S=['X'/s('X')],\n",
+ " apply(p('X'),S,Res1),\n",
+ " apply(p(s('X')),S,Res2)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "96d07660",
+ "metadata": {},
+ "source": [
+ "Composition s1s2 of two substitutions s1 and s2\n",
+ "Defined like composition of functions: A(s1s2) = (As1)s2\n",
+ "Let s1={X1/t1,...},s2={Y1/r1,...}, then s1s2 = {X1/t1s1,...}∪ {Yi/ri| Yi ∉ {X1,...} }\n",
+ "(and delete Xi/tis1 if Xi=tis1)\n",
+ "\n",
+ "In Prolog this gives this (naive) implementation:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 27,
+ "id": "d56c09cb",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ "compose_subst(Sub1,Sub2,Res) :-\n",
+ " apply1(Sub1,Sub2,NewSub1), % apply Sub2 to RHS of Sub1\n",
+ " filter2(Sub2,Sub1,NewSub2), % filter unreachable parts of Sub2\n",
+ " append(NewSub1,NewSub2,Res).\n",
+ "\n",
+ "apply1([],_,[]).\n",
+ "apply1([X1/T1|T],Sub2,Res) :- apply(T1,Sub2,NewT1),\n",
+ " (NewT1=X1 -> apply1(T,Sub2,Res) % X1/NewT1 is useless; remove it\n",
+ " ; Res = [X1/NewT1|ResT], apply1(T,Sub2,ResT)).\n",
+ "\n",
+ "filter2([],_,[]).\n",
+ "filter2([Y1/T1|T],Sub1,Res) :-\n",
+ " (member(Y1/_,Sub1) -> filter2(T,Sub1,Res) % Y1 is in domain of Sub1\n",
+ " ; Res=[Y1/T1|ResT], filter2(T,Sub1,ResT))."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 28,
+ "id": "b1f992d9",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mRes = [X/a,Y/b]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- compose_subst(['X'/a],['Y'/b],Res)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 29,
+ "id": "df25466a",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mRes = [X/b,Y/b]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- compose_subst(['X'/'Y'],['Y'/b],Res)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 30,
+ "id": "c6a79cdf",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mRes = [Y/X]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- compose_subst(['X'/'Y'],['Y'/'X'],Res)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 31,
+ "id": "68a10c4f",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mRes = [X/f(a)]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- compose_subst(['X'/f('X')],['X'/a],Res)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "778e0b71",
+ "metadata": {},
+ "source": [
+ "A (naive) Prolog version of the unification algorithm.\n",
+ "\n",
+ "It does not really compute the disagreement tuple; it traverses both terms and applies the current substitution as it goes along."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 43,
+ "id": "0f59567c",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ "\n",
+ "unify(X,Y,SubSoFar,Res) :-\n",
+ " apply(X,SubSoFar,NX),\n",
+ " apply(Y,SubSoFar,NY),\n",
+ " unify2(NX,NY,SubSoFar,Res).\n",
+ "\n",
+ "unify2(X,Y,SubSoFar,Res) :- X==Y,!, \n",
+ " Res=SubSoFar. % there are no disagreements at this position; keep the current substitution\n",
+ "unify2(X,Y,SubSoFar,Res) :- variable(X),!, % ak is a variable which does not occur in bk \n",
+ " not_occurs(X,Y),\n",
+ " compose_mgu(SubSoFar,[X/Y],Res).\n",
+ "unify2(X,Y,SubSoFar,Res) :- variable(Y),!, % bk is a variable which does not occur in ak \n",
+ " not_occurs(Y,X),\n",
+ " compose_mgu(SubSoFar,[Y/X],Res).\n",
+ "unify2(FX,FY,SubSoFar,Res) :-\n",
+ " FX =.. [Func|ArgsX],\n",
+ " FY =.. [Func|ArgsY], % check we have the same function symbol and proceed unifying arguments\n",
+ " l_unify(ArgsX,ArgsY,SubSoFar,Res).\n",
+ "\n",
+ "compose_mgu(SubSoFar,New,Res) :-\n",
+ " compose_subst(SubSoFar,New,Res),\n",
+ " format('Adding binding ~w, new candidate MGU ~w~n',[New,Res]).\n",
+ "\n",
+ "l_unify([],[],Sub,Sub).\n",
+ "l_unify([X1|TX],[Y1|TY],Sub,Res) :-\n",
+ " unify(X1,Y1,Sub,Sub2),\n",
+ " l_unify(TX,TY,Sub2,Res).\n",
+ "\n",
+ "occurs(X,Y) :- X==Y,!.\n",
+ "occurs(X,FY) :- FY =.. [_|Args], member(Y,Args), occurs(X,Y).\n",
+ "\n",
+ "not_occurs(X,Term) :- \\+ occurs(X,Term).\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 44,
+ "id": "ca8373d0",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mtrue"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- occurs('X',f('X'))."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 45,
+ "id": "e2e2a0fe",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Adding binding [X/a], new candidate MGU [X/a]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mRes = [X/a]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- unify(f('X'),f(a),[],Res)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 46,
+ "id": "e04a20d1",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1;31mfalse"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- unify(f('X'),'X',[],Res)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 47,
+ "id": "c2b9d14f",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Adding binding [Y/f(X)], new candidate MGU [Y/f(X)]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mRes = [Y/f(X)]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- unify(f('X'),'Y',[],Res)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 48,
+ "id": "126098d1",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mY = f(X)"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- f(X)=Y."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 49,
+ "id": "679ece73",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Adding binding [Y/X], new candidate MGU [Y/X]\n",
+ "Adding binding [X/s(0)], new candidate MGU [Y/s(0),X/s(0)]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mRes = [Y/s(0),X/s(0)]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- unify(f('Y',s('Y')),f('X',s(s(0))),[],Res)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "89c66d0d",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": []
+ }
+ ],
+ "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
+}