From 057fca4581e099b939d49470eca2875ae000bd48 Mon Sep 17 00:00:00 2001
From: dajiaohuang <mikewushuwen@outlook.com>
Date: Fri, 23 Oct 2026 19:00:01 +0800
Subject: [PATCH] Document first-order syntax support

---
 notebooks/logic.ipynb | 68 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 68 insertions(+)

diff --git a/notebooks/logic.ipynb b/notebooks/logic.ipynb
index f5013aa76..e06feb44e 100644
--- a/notebooks/logic.ipynb
+++ b/notebooks/logic.ipynb
@@ -3503,6 +3503,74 @@
     "The class `FolKB` can be used to represent a knowledge base of First-order logic sentences. You would initialize and use it the same way as you would for `PropKB` except that the clauses are first-order definite clauses. We will see how to write such clauses to create a database and query them in the following sections."
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "### Syntax in this implementation\n",
+    "\n",
+    "`expr()` builds `Expr` trees with Python syntax and special handling for `==>`, `<==`, and `<=>`.\n",
+    "It is not a parser for the full first-order grammar.\n",
+    "The same call form can denote a relation-like atom (`Teaches(x, y)`) or a function-like term\n",
+    "(`SubjectOf(y)`). In `Mentors(x, SubjectOf(y))`, the call is nested as a term. The tree does not\n",
+    "assign separate predicate and function types; context supplies the role.\n",
+    "In the FOL helpers, a no-argument lowercase symbol is treated as a variable; names such as\n",
+    "`Ada` are constants.\n",
+    "\n",
+    "`Expr.__eq__` compares expression trees: `x == y` is a Python boolean, not a logical equality\n",
+    "formula. `FolKB` does not provide built-in equality reasoning. Use `unify` for syntactic term\n",
+    "matching; a named predicate such as `SamePerson(x, y)` is an ordinary relation, not equality.\n",
+    "\n",
+    "`FolKB` accepts first-order definite clauses. Variables in these rules are implicitly universally\n",
+    "quantified by rule application; the chaining API does not implement general `forall`/`exists`\n",
+    "formulas. Query variables yield substitutions, as shown below."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 100,
+   "metadata": {"collapsed": true},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "(False, Teaches(x, y), Mentors(x, SubjectOf(y)))"
+      ]
+     },
+     "execution_count": 100,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "x, y = expr('x, y')\n",
+    "x == y, expr('Teaches(x, y)'), expr('Mentors(x, SubjectOf(y))')"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 101,
+   "metadata": {"collapsed": true},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "[{q: Logic}]"
+      ]
+     },
+     "execution_count": 101,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "syntax_demo_kb = FolKB([\n",
+    "    expr('Tutor(x, y) ==> Learns(x, y)'),\n",
+    "    expr('Tutor(Ada, Logic)'),\n",
+    "])\n",
+    "list(fol_fc_ask(syntax_demo_kb, expr('Learns(Ada, q)')))"
+   ]
+  },
   {
    "cell_type": "markdown",
    "metadata": {},