Document first-order syntax support

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": {},