source/notebooks/First_Order_Logic.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "a2dbdd75",
   "metadata": {},
   "outputs": [],
   "source": [
    "import nltk"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "c1b3d22b",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Grammar with 25 productions (start state = S)\n",
      "    S -> FORALL\n",
      "    S -> IMPLIES\n",
      "    S -> NOT\n",
      "    S -> ATOMIC\n",
      "    FORALL -> 'forall' VARIABLE S\n",
      "    IMPLIES -> '(' S '->' S ')'\n",
      "    NOT -> '(' 'not' S ')'\n",
      "    ATOMIC -> PD_LESS_THAN\n",
      "    ATOMIC -> PD_EQUALS\n",
      "    PD_LESS_THAN -> '<' TERM TERM\n",
      "    PD_EQUALS -> '=' TERM TERM\n",
      "    TERM -> FN_SUCC\n",
      "    TERM -> FN_PLUS\n",
      "    TERM -> FN_TIMES\n",
      "    TERM -> FN_EXP\n",
      "    TERM -> VARIABLE\n",
      "    TERM -> CONSTANT_ZERO\n",
      "    FN_SUCC -> 'S' TERM\n",
      "    FN_PLUS -> '+' TERM TERM\n",
      "    FN_TIMES -> '*' TERM TERM\n",
      "    FN_EXP -> 'E' TERM TERM\n",
      "    VARIABLE -> 'x'\n",
      "    VARIABLE -> 'y'\n",
      "    VARIABLE -> 'z'\n",
      "    CONSTANT_ZERO -> '0'\n"
     ]
    }
   ],
   "source": [
    "def is_var_or_const(x):\n",
    "    return x in ['x','y','z','0']\n",
    "\n",
    "elementary_number_theory_grammar = nltk.CFG.fromstring(\"\"\"\n",
    "S -> FORALL\n",
    "S -> IMPLIES\n",
    "S -> NOT\n",
    "S -> ATOMIC\n",
    "FORALL -> 'forall' VARIABLE S\n",
    "IMPLIES -> '(' S '->' S ')'\n",
    "NOT -> '(' 'not' S ')'\n",
    "ATOMIC -> PD_LESS_THAN\n",
    "ATOMIC -> PD_EQUALS\n",
    "PD_LESS_THAN -> '<' TERM TERM\n",
    "PD_EQUALS -> '=' TERM TERM\n",
    "TERM -> FN_SUCC\n",
    "TERM -> FN_PLUS\n",
    "TERM -> FN_TIMES\n",
    "TERM -> FN_EXP\n",
    "TERM -> VARIABLE\n",
    "TERM -> CONSTANT_ZERO\n",
    "FN_SUCC -> 'S' TERM\n",
    "FN_PLUS -> '+' TERM TERM\n",
    "FN_TIMES -> '*' TERM TERM\n",
    "FN_EXP -> 'E' TERM TERM\n",
    "VARIABLE -> 'x'\n",
    "VARIABLE -> 'y'\n",
    "VARIABLE -> 'z'\n",
    "CONSTANT_ZERO -> '0'\n",
    "    \"\"\")\n",
    "print(elementary_number_theory_grammar)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "6a49c032",
   "metadata": {},
   "outputs": [],
   "source": [
    "def tokenize(exp):\n",
    "    \"\"\"\n",
    "    Returns the tokens of an expression\n",
    "    \"\"\"\n",
    "    return exp.split()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "608a17bb",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/svg+xml": [
       "<svg baseProfile=\"full\" height=\"360px\" preserveAspectRatio=\"xMidYMid meet\" style=\"font-family: times, serif; font-weight: normal; font-style: normal; font-size: 16px;\" version=\"1.1\" viewBox=\"0,0,312.0,360.0\" width=\"312px\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:ev=\"http://www.w3.org/2001/xml-events\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">S</text></svg><svg width=\"100%\" x=\"0%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">NOT</text></svg><svg width=\"7.69231%\" x=\"0%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">(</text></svg></svg><line stroke=\"black\" x1=\"50%\" x2=\"3.84615%\" y1=\"19.2px\" y2=\"48px\" /><svg width=\"12.8205%\" x=\"7.69231%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">not</text></svg></svg><line stroke=\"black\" x1=\"50%\" x2=\"14.1026%\" y1=\"19.2px\" y2=\"48px\" /><svg width=\"71.7949%\" x=\"20.5128%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">S</text></svg><svg width=\"100%\" x=\"0%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">ATOMIC</text></svg><svg width=\"100%\" x=\"0%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">PD_EQUALS</text></svg><svg width=\"10.7143%\" x=\"0%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">=</text></svg></svg><line stroke=\"black\" x1=\"50%\" x2=\"5.35714%\" y1=\"19.2px\" y2=\"48px\" /><svg width=\"35.7143%\" x=\"10.7143%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">TERM</text></svg><svg width=\"100%\" x=\"0%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">VARIABLE</text></svg><svg width=\"100%\" x=\"0%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">x</text></svg></svg><line stroke=\"black\" x1=\"50%\" x2=\"50%\" y1=\"19.2px\" y2=\"48px\" /></svg><line stroke=\"black\" x1=\"50%\" x2=\"50%\" y1=\"19.2px\" y2=\"48px\" /></svg><line stroke=\"black\" x1=\"50%\" x2=\"28.5714%\" y1=\"19.2px\" y2=\"48px\" /><svg width=\"53.5714%\" x=\"46.4286%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">TERM</text></svg><svg width=\"100%\" x=\"0%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">CONSTANT_ZERO</text></svg><svg width=\"100%\" x=\"0%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">0</text></svg></svg><line stroke=\"black\" x1=\"50%\" x2=\"50%\" y1=\"19.2px\" y2=\"48px\" /></svg><line stroke=\"black\" x1=\"50%\" x2=\"50%\" y1=\"19.2px\" y2=\"48px\" /></svg><line stroke=\"black\" x1=\"50%\" x2=\"73.2143%\" y1=\"19.2px\" y2=\"48px\" /></svg><line stroke=\"black\" x1=\"50%\" x2=\"50%\" y1=\"19.2px\" y2=\"48px\" /></svg><line stroke=\"black\" x1=\"50%\" x2=\"50%\" y1=\"19.2px\" y2=\"48px\" /></svg><line stroke=\"black\" x1=\"50%\" x2=\"56.4103%\" y1=\"19.2px\" y2=\"48px\" /><svg width=\"7.69231%\" x=\"92.3077%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">)</text></svg></svg><line stroke=\"black\" x1=\"50%\" x2=\"96.1538%\" y1=\"19.2px\" y2=\"48px\" /></svg><line stroke=\"black\" x1=\"50%\" x2=\"50%\" y1=\"19.2px\" y2=\"48px\" /></svg>"
      ],
      "text/plain": [
       "Tree('S', [Tree('NOT', ['(', 'not', Tree('S', [Tree('ATOMIC', [Tree('PD_EQUALS', ['=', Tree('TERM', [Tree('VARIABLE', ['x'])]), Tree('TERM', [Tree('CONSTANT_ZERO', ['0'])])])])]), ')'])])"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "elementary_number_theory_parser = nltk.ChartParser(elementary_number_theory_grammar)\n",
    "list(elementary_number_theory_parser.parse(tokenize(\"( not = x 0 )\")))[0]"
   ]
  },
  {
   "cell_type": "raw",
   "id": "62eef342",
   "metadata": {},
   "source": [
    "Any nonzero natural number is the successor of some number"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "1a1ccce5",
   "metadata": {},
   "outputs": [],
   "source": [
    "sent = \"forall x ( ( not = x 0 ) -> ( not forall y ( not = x S y ) ) )\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "06306218",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "['forall',\n",
       " 'x',\n",
       " '(',\n",
       " '(',\n",
       " 'not',\n",
       " '=',\n",
       " 'x',\n",
       " '0',\n",
       " ')',\n",
       " '->',\n",
       " '(',\n",
       " 'not',\n",
       " 'forall',\n",
       " 'y',\n",
       " '(',\n",
       " 'not',\n",
       " '=',\n",
       " 'x',\n",
       " 'S',\n",
       " 'y',\n",
       " ')',\n",
       " ')',\n",
       " ')']"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tokenize(sent)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "31c8570f",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(S\n",
      "  (FORALL\n",
      "    forall\n",
      "    (VARIABLE x)\n",
      "    (S\n",
      "      (IMPLIES\n",
      "        (\n",
      "        (S\n",
      "          (NOT\n",
      "            (\n",
      "            not\n",
      "            (S\n",
      "              (ATOMIC\n",
      "                (PD_EQUALS\n",
      "                  =\n",
      "                  (TERM (VARIABLE x))\n",
      "                  (TERM (CONSTANT_ZERO 0)))))\n",
      "            )))\n",
      "        ->\n",
      "        (S\n",
      "          (NOT\n",
      "            (\n",
      "            not\n",
      "            (S\n",
      "              (FORALL\n",
      "                forall\n",
      "                (VARIABLE y)\n",
      "                (S\n",
      "                  (NOT\n",
      "                    (\n",
      "                    not\n",
      "                    (S\n",
      "                      (ATOMIC\n",
      "                        (PD_EQUALS\n",
      "                          =\n",
      "                          (TERM (VARIABLE x))\n",
      "                          (TERM (FN_SUCC S (TERM (VARIABLE y)))))))\n",
      "                    )))))\n",
      "            )))\n",
      "        )))))\n"
     ]
    }
   ],
   "source": [
    "T = list(elementary_number_theory_parser.parse(tokenize(sent)))[0]\n",
    "print(T)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "33614a99",
   "metadata": {},
   "outputs": [],
   "source": [
    "def is_var_or_const(x):\n",
    "    return x in ['x','y','z','0']\n",
    "\n",
    "def pruneTree(tree):\n",
    "    if isinstance(tree, str):\n",
    "        if not is_var_or_const(tree):\n",
    "            return None\n",
    "        return tree\n",
    "    if len(tree) == 1:\n",
    "        return pruneTree(tree[0])\n",
    "    children_trees = []\n",
    "    for child in tree:\n",
    "        child_tree = pruneTree(child)\n",
    "        if child_tree is not None:\n",
    "            children_trees.append(child_tree)\n",
    "    return nltk.tree.Tree(tree.label(), children_trees)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "01817fcd",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/svg+xml": [
       "<svg baseProfile=\"full\" height=\"360px\" preserveAspectRatio=\"xMidYMid meet\" style=\"font-family: times, serif; font-weight: normal; font-style: normal; font-size: 16px;\" version=\"1.1\" viewBox=\"0,0,232.0,360.0\" width=\"232px\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:ev=\"http://www.w3.org/2001/xml-events\" xmlns:xlink=\"http://www.w3.org/1999/xlink\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">FORALL</text></svg><svg width=\"10.3448%\" x=\"0%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">x</text></svg></svg><line stroke=\"black\" x1=\"50%\" x2=\"5.17241%\" y1=\"19.2px\" y2=\"48px\" /><svg width=\"89.6552%\" x=\"10.3448%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">IMPLIES</text></svg><svg width=\"42.3077%\" x=\"0%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">NOT</text></svg><svg width=\"100%\" x=\"0%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">PD_EQUALS</text></svg><svg width=\"50%\" x=\"0%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">x</text></svg></svg><line stroke=\"black\" x1=\"50%\" x2=\"25%\" y1=\"19.2px\" y2=\"48px\" /><svg width=\"50%\" x=\"50%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">0</text></svg></svg><line stroke=\"black\" x1=\"50%\" x2=\"75%\" y1=\"19.2px\" y2=\"48px\" /></svg><line stroke=\"black\" x1=\"50%\" x2=\"50%\" y1=\"19.2px\" y2=\"48px\" /></svg><line stroke=\"black\" x1=\"50%\" x2=\"21.1538%\" y1=\"19.2px\" y2=\"48px\" /><svg width=\"57.6923%\" x=\"42.3077%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">NOT</text></svg><svg width=\"100%\" x=\"0%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">FORALL</text></svg><svg width=\"20%\" x=\"0%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">y</text></svg></svg><line stroke=\"black\" x1=\"50%\" x2=\"10%\" y1=\"19.2px\" y2=\"48px\" /><svg width=\"80%\" x=\"20%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">NOT</text></svg><svg width=\"100%\" x=\"0%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">PD_EQUALS</text></svg><svg width=\"25%\" x=\"0%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">x</text></svg></svg><line stroke=\"black\" x1=\"50%\" x2=\"12.5%\" y1=\"19.2px\" y2=\"48px\" /><svg width=\"75%\" x=\"25%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">FN_SUCC</text></svg><svg width=\"100%\" x=\"0%\" y=\"48px\"><defs /><svg width=\"100%\" x=\"0\" y=\"0px\"><defs /><text text-anchor=\"middle\" x=\"50%\" y=\"16px\">y</text></svg></svg><line stroke=\"black\" x1=\"50%\" x2=\"50%\" y1=\"19.2px\" y2=\"48px\" /></svg><line stroke=\"black\" x1=\"50%\" x2=\"62.5%\" y1=\"19.2px\" y2=\"48px\" /></svg><line stroke=\"black\" x1=\"50%\" x2=\"50%\" y1=\"19.2px\" y2=\"48px\" /></svg><line stroke=\"black\" x1=\"50%\" x2=\"60%\" y1=\"19.2px\" y2=\"48px\" /></svg><line stroke=\"black\" x1=\"50%\" x2=\"50%\" y1=\"19.2px\" y2=\"48px\" /></svg><line stroke=\"black\" x1=\"50%\" x2=\"71.1538%\" y1=\"19.2px\" y2=\"48px\" /></svg><line stroke=\"black\" x1=\"50%\" x2=\"55.1724%\" y1=\"19.2px\" y2=\"48px\" /></svg>"
      ],
      "text/plain": [
       "Tree('FORALL', ['x', Tree('IMPLIES', [Tree('NOT', [Tree('PD_EQUALS', ['x', '0'])]), Tree('NOT', [Tree('FORALL', ['y', Tree('NOT', [Tree('PD_EQUALS', ['x', Tree('FN_SUCC', ['y'])])])])])])])"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "pruneTree(T)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "212d4fd1",
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "5174f197-19ed-4bda-82b0-04fa378a6392",
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "a9f43fd2-afb5-4ea1-9c9e-3eafa48f2a6c",
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.11.9"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}