{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Lógica de primer orden\n",
    "\n",
    "* *30 min* | Última modificación: Diciembre 10, 2020"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "http://www.nltk.org/book/\n",
    "\n",
    "Text Analytics with Python"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "## Las sentencias declaraticas son True/False en ciertas situaciones\n",
    "## NP (Noun phrases) y NNS (sustantivos) se refieren a cosas en el mundo"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Definición de modelo: "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "negation       \t-\n",
      "conjunction    \t&\n",
      "disjunction    \t|\n",
      "implication    \t->\n",
      "equivalence    \t<->\n"
     ]
    }
   ],
   "source": [
    "import nltk\n",
    "\n",
    "nltk.boolean_ops()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "read_expr = nltk.sem.Expression.fromstring"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<NegatedExpression -P>"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "##\n",
    "## Negación\n",
    "##\n",
    "read_expr('-P')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<AndExpression (P & Q)>"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "##\n",
    "## Conjunción (and)\n",
    "##\n",
    "read_expr('P & Q')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<OrExpression (P | Q)>"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "##\n",
    "## Disyunción (or)\n",
    "##\n",
    "read_expr('P | Q')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<ImpExpression (P -> Q)>"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "##\n",
    "## Implicación (if ... then ...)\n",
    "##\n",
    "read_expr('P -> Q')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<IffExpression (P <-> Q)>"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "##\n",
    "## Equivalencia (if and only if ... / iff)\n",
    "##\n",
    "read_expr('P <-> Q')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<NegatedExpression -(P & Q)>"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('-(P & Q)')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<OrExpression (P | (R -> Q))>"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('P | (R -> Q)')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<IffExpression (P <-> --P)>"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('P <-> -- P')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Get:1 http://security.ubuntu.com/ubuntu bionic-security InRelease [88.7 kB]\n",
      "Get:2 http://archive.ubuntu.com/ubuntu bionic InRelease [242 kB]\n",
      "Get:3 http://security.ubuntu.com/ubuntu bionic-security/restricted amd64 Packages [237 kB]\n",
      "Get:4 http://archive.ubuntu.com/ubuntu bionic-updates InRelease [88.7 kB]      \n",
      "Get:5 http://archive.ubuntu.com/ubuntu bionic-backports InRelease [74.6 kB]    \n",
      "Get:6 http://security.ubuntu.com/ubuntu bionic-security/multiverse amd64 Packages [15.3 kB]\n",
      "Get:7 http://security.ubuntu.com/ubuntu bionic-security/main amd64 Packages [1816 kB]\n",
      "Get:8 http://archive.ubuntu.com/ubuntu bionic/restricted amd64 Packages [13.5 kB]\n",
      "Get:9 http://archive.ubuntu.com/ubuntu bionic/universe amd64 Packages [11.3 MB]\n",
      "Get:10 http://security.ubuntu.com/ubuntu bionic-security/universe amd64 Packages [1372 kB]\n",
      "Get:11 http://archive.ubuntu.com/ubuntu bionic/main amd64 Packages [1344 kB]   \n",
      "Get:12 http://archive.ubuntu.com/ubuntu bionic/multiverse amd64 Packages [186 kB]\n",
      "Get:13 http://archive.ubuntu.com/ubuntu bionic-updates/main amd64 Packages [2244 kB]\n",
      "Get:14 http://archive.ubuntu.com/ubuntu bionic-updates/universe amd64 Packages [2136 kB]\n",
      "Get:15 http://archive.ubuntu.com/ubuntu bionic-updates/multiverse amd64 Packages [53.8 kB]\n",
      "Get:16 http://archive.ubuntu.com/ubuntu bionic-updates/restricted amd64 Packages [266 kB]\n",
      "Get:17 http://archive.ubuntu.com/ubuntu bionic-backports/main amd64 Packages [11.3 kB]\n",
      "Get:18 http://archive.ubuntu.com/ubuntu bionic-backports/universe amd64 Packages [11.4 kB]\n",
      "Fetched 21.5 MB in 12s (1738 kB/s)                                             \n",
      "Reading package lists... Done\n",
      "Reading package lists...\n",
      "Building dependency tree...\n",
      "Reading state information...\n",
      "The following additional packages will be installed:\n",
      "  libladr4\n",
      "Suggested packages:\n",
      "  ladr4-apps prover9-doc\n",
      "The following NEW packages will be installed:\n",
      "  libladr4 prover9\n",
      "0 upgraded, 2 newly installed, 0 to remove and 23 not upgraded.\n",
      "Need to get 245 kB of archives.\n",
      "After this operation, 801 kB of additional disk space will be used.\n",
      "Get:1 http://archive.ubuntu.com/ubuntu bionic/universe amd64 libladr4 amd64 0.0.200911a-2.1build1 [168 kB]\n",
      "Get:2 http://archive.ubuntu.com/ubuntu bionic/universe amd64 prover9 amd64 0.0.200911a-2.1build1 [77.8 kB]\n",
      "Fetched 245 kB in 1s (219 kB/s)\n",
      "debconf: unable to initialize frontend: Dialog\n",
      "debconf: (No usable dialog-like program is installed, so the dialog based frontend cannot be used. at /usr/share/perl5/Debconf/FrontEnd/Dialog.pm line 76, <> line 2.)\n",
      "debconf: falling back to frontend: Readline\n",
      "Selecting previously unselected package libladr4.\n",
      "(Reading database ... 13639 files and directories currently installed.)\n",
      "Preparing to unpack .../libladr4_0.0.200911a-2.1build1_amd64.deb ...\n",
      "Unpacking libladr4 (0.0.200911a-2.1build1) ...\n",
      "Selecting previously unselected package prover9.\n",
      "Preparing to unpack .../prover9_0.0.200911a-2.1build1_amd64.deb ...\n",
      "Unpacking prover9 (0.0.200911a-2.1build1) ...\n",
      "Setting up libladr4 (0.0.200911a-2.1build1) ...\n",
      "Setting up prover9 (0.0.200911a-2.1build1) ...\n",
      "Processing triggers for libc-bin (2.27-3ubuntu1.2) ...\n"
     ]
    }
   ],
   "source": [
    "!apt-get update -y && apt-get install -yq prover9"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "lp = nltk.sem.Expression.fromstring\n",
    "SnF = read_expr('SnF')\n",
    "NotFnS = read_expr('-FnS')\n",
    "R = read_expr('SnF -> -FnS')\n",
    "prover = nltk.Prover9()\n",
    "prover.prove(NotFnS, [SnF, R])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [],
   "source": [
    "val = nltk.Valuation([('P', True), ('Q', True), ('R', False)])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "val['P']"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "False\n",
      "False\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "dom = set()\n",
    "g = nltk.Assignment(dom)\n",
    "\n",
    "## inicialización del modelo\n",
    "m = nltk.Model(dom, val)\n",
    "\n",
    "print(m.evaluate('(P & Q)', g))\n",
    "print(m.evaluate('-(P & Q)', g))\n",
    "print(m.evaluate('(P & R)', g))\n",
    "print(m.evaluate('(P | R)', g))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<ConstantExpression angus>"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr = nltk.sem.Expression.fromstring\n",
    "expr = read_expr('walk(angus)', type_check=True)\n",
    "expr.argument"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "e"
      ]
     },
     "execution_count": 21,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expr.argument.type"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<ConstantExpression walk>"
      ]
     },
     "execution_count": 23,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expr.function"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<e,?>"
      ]
     },
     "execution_count": 22,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expr.function.type"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "e"
      ]
     },
     "execution_count": 25,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "sig = {'walk': '<e, t>'}\n",
    "expr = read_expr('walk(angus)', signature=sig)\n",
    "expr.function.type"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "set()"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr = nltk.sem.Expression.fromstring\n",
    "read_expr('dog(cyril)').free()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{Variable('x')}"
      ]
     },
     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('dog(x)').free()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "set()"
      ]
     },
     "execution_count": 29,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('own(angus, cyril)').free()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "set()"
      ]
     },
     "execution_count": 30,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('exists x.dog(x)').free()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{Variable('x')}"
      ]
     },
     "execution_count": 31,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('((some x. walk(x)) -> sing(x))').free()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{Variable('y')}"
      ]
     },
     "execution_count": 32,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('exists x.own(y, x)').free()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 34,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "NotFnS = read_expr('-north_of(f, s)') \n",
    "SnF = read_expr('north_of(s, f)')  \n",
    "R = read_expr('all x. all y. (north_of(x, y) -> -north_of(y, x))')\n",
    "prover = nltk.Prover9()  \n",
    "prover.prove(NotFnS, [SnF, R]) "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "execution_count": 36,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FnS = read_expr('north_of(f, s)')\n",
    "prover.prove(FnS, [SnF, R])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "metadata": {},
   "outputs": [],
   "source": [
    "dom = {'b', 'o', 'c'}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 39,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{'bertie': 'b',\n",
      " 'boy': {('b',)},\n",
      " 'cyril': 'c',\n",
      " 'dog': {('c',)},\n",
      " 'girl': {('o',)},\n",
      " 'olive': 'o',\n",
      " 'see': {('o', 'c'), ('b', 'o'), ('c', 'b')},\n",
      " 'walk': {('o',), ('c',)}}\n"
     ]
    }
   ],
   "source": [
    "v = \"\"\"\n",
    "bertie => b\n",
    "olive => o\n",
    "cyril => c\n",
    "boy => {b}\n",
    "girl => {o}\n",
    "dog => {c}\n",
    "walk => {o, c}\n",
    "see => {(b, o), (c, b), (o, c)}\n",
    "\"\"\"\n",
    "val = nltk.Valuation.fromstring(v)\n",
    "print(val)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 40,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "('o', 'c') in val['see']"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 41,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "('b',) in val['boy']"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "\n",
      "\n",
      "\n",
      "v = \"\"\"\n",
      "bertie => b\n",
      "olive => o\n",
      "cyril => c\n",
      "boy => {b}\n",
      "girl => {o}\n",
      "dog => {c}\n",
      "walk => {o, c}\n",
      "see => {(b, o), (c, b), (o, c)}\n",
      "\"\"\"\n",
      "val = nltk.Valuation.fromstring(v)\n",
      "print(val)\n",
      "\n",
      "\n",
      "\n"
     ]
    }
   ],
   "source": [
    "text = '''\n",
    "\n",
    "\n",
    "\n",
    ">>> v = \"\"\"\n",
    "... bertie => b\n",
    "... olive => o\n",
    "... cyril => c\n",
    "... boy => {b}\n",
    "... girl => {o}\n",
    "... dog => {c}\n",
    "... walk => {o, c}\n",
    "... see => {(b, o), (c, b), (o, c)}\n",
    "... \"\"\"\n",
    ">>> val = nltk.Valuation.fromstring(v)\n",
    ">>> print(val)\n",
    "\n",
    "\n",
    "'''\n",
    "\n",
    "\n",
    "text = text.replace(\">>> \", \"\").replace(\"... \", \"\").replace(\"...\", \"\").replace(\"\\t\", \"\")\n",
    "print(text)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "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.6.9"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}