From 98f692d9977c3772467a70d27bacf5a34617bdb9 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Tue, 22 Nov 2022 16:06:05 +0100
Subject: [PATCH] add some text
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
logic_programming/7_Unification.ipynb | 53 ++++++++++++++++++++-------
1 file changed, 39 insertions(+), 14 deletions(-)
diff --git a/logic_programming/7_Unification.ipynb b/logic_programming/7_Unification.ipynb
index 5d3c0ac..03e3dbc 100644
--- a/logic_programming/7_Unification.ipynb
+++ b/logic_programming/7_Unification.ipynb
@@ -9,7 +9,9 @@
}
},
"source": [
- "## Substitutions\n",
+ "This notebook is not finished yet and lacks some markdown explanations.\n",
+ "\n",
+ "### Substitutions\n",
"\n",
"Substitution: mapping from variables to terms\n",
"\n",
@@ -23,7 +25,7 @@
},
{
"cell_type": "code",
- "execution_count": 13,
+ "execution_count": 50,
"id": "78764141",
"metadata": {
"vscode": {
@@ -39,7 +41,7 @@
"variable('X'). % a few artificial variables for easier reading\n",
"variable('Y').\n",
"variable('Z').\n",
- "term(_)."
+ "term(_). % no checks done at the moment; we allow any Prolog term, but suppose we have no real Prolog variables"
]
},
{
@@ -72,6 +74,8 @@
"id": "ab0d39bc",
"metadata": {},
"source": [
+ "### Applying Substitutions\n",
+ "\n",
"Applying a substitution to a term or wff\n",
"Instantaneous replacement by right-hand sides\n"
]
@@ -101,7 +105,7 @@
},
{
"cell_type": "code",
- "execution_count": 15,
+ "execution_count": 51,
"id": "c675dc2a",
"metadata": {
"vscode": {
@@ -235,6 +239,14 @@
" apply(p('Z','Z'),S,Res2)."
]
},
+ {
+ "cell_type": "markdown",
+ "id": "5fd84486",
+ "metadata": {},
+ "source": [
+ "This is not a unifier:"
+ ]
+ },
{
"cell_type": "code",
"execution_count": 23,
@@ -268,9 +280,11 @@
"id": "96d07660",
"metadata": {},
"source": [
+ "### Composing Substitutions\n",
"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",
+ "is defined like composition of functions: A(s1s2) = (As1)s2\n",
+ "Let s1={X1/t1,...},s2={Y1/r1,...}, \n",
+ "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:"
@@ -305,7 +319,7 @@
},
{
"cell_type": "code",
- "execution_count": 28,
+ "execution_count": 52,
"id": "b1f992d9",
"metadata": {
"vscode": {
@@ -329,7 +343,7 @@
},
{
"cell_type": "code",
- "execution_count": 29,
+ "execution_count": 53,
"id": "df25466a",
"metadata": {
"vscode": {
@@ -353,7 +367,7 @@
},
{
"cell_type": "code",
- "execution_count": 30,
+ "execution_count": 55,
"id": "c6a79cdf",
"metadata": {
"vscode": {
@@ -404,6 +418,8 @@
"id": "778e0b71",
"metadata": {},
"source": [
+ "### Robinson's Unification Algorithm\n",
+ "\n",
"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."
@@ -480,7 +496,7 @@
},
{
"cell_type": "code",
- "execution_count": 45,
+ "execution_count": 56,
"id": "e2e2a0fe",
"metadata": {
"vscode": {
@@ -513,7 +529,7 @@
},
{
"cell_type": "code",
- "execution_count": 46,
+ "execution_count": 57,
"id": "e04a20d1",
"metadata": {
"vscode": {
@@ -524,7 +540,16 @@
{
"data": {
"text/plain": [
- "\u001b[1;31mfalse"
+ "Adding binding [X/f(a)], new candidate MGU [X/f(a)]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mRes = [X/f(a)]"
]
},
"metadata": {},
@@ -532,7 +557,7 @@
}
],
"source": [
- "?- unify(f('X'),'X',[],Res)."
+ "?- unify(f(a),'X',[],Res)."
]
},
{
@@ -594,7 +619,7 @@
},
{
"cell_type": "code",
- "execution_count": 49,
+ "execution_count": 58,
"id": "679ece73",
"metadata": {
"vscode": {
--
GitLab