{
  "nbformat": 4,
  "nbformat_minor": 0,
  "metadata": {
    "colab": {
      "provenance": [],
      "collapsed_sections": [
        "VFwDG6ls7P8P"
      ]
    },
    "kernelspec": {
      "name": "python3",
      "display_name": "Python 3"
    },
    "language_info": {
      "name": "python"
    }
  },
  "cells": [
    {
      "cell_type": "markdown",
      "source": [
        "# Domácí úloha 3 - Pravdivostní tabulky a typová analýza"
      ],
      "metadata": {
        "id": "zdum_tfQ7H2F"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "## Importy knihoven a definice pomocných funkcí\n",
        "\n",
        "Následující buňky je potřeba spustit, aby vše fungovalo, jak má"
      ],
      "metadata": {
        "id": "VFwDG6ls7P8P"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "%pip install truth-table-generator"
      ],
      "metadata": {
        "id": "blEJ1eq05QeH"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "import graphviz as gv\n",
        "import nltk\n",
        "import nltk.sem.logic as lg\n",
        "import ttg"
      ],
      "metadata": {
        "id": "tDvdce1K7Uj6"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "def l_not(argument):\n",
        "    \"\"\"Fuknce pro vytvoření negace logického argumentu.\n",
        "    \"\"\"\n",
        "    return f\"(-{argument})\"\n",
        "\n",
        "def l_and(*args):\n",
        "    \"\"\"Funkce pro spojení dvou a více výroků pomocí logické spojky and. Pokud\n",
        "    je na vstupu pouze jeden výrok, funkce jej vrátí uzávorkovaný.\n",
        "    \"\"\"\n",
        "\n",
        "    result = f\"({args[0]})\"\n",
        "\n",
        "    for c_arg in args[1:]:\n",
        "        result = f\"({result} and ({c_arg}))\"\n",
        "\n",
        "    return result\n",
        "\n",
        "def l_or(*args):\n",
        "    \"\"\"Funkce pro spojení dvou a více výroků pomocí logické spojky or. Pokud\n",
        "    je na vstupu pouze jeden výrok, funkce jej vrátí uzávorkovaný.\n",
        "    \"\"\"\n",
        "    result = f\"({args[0]})\"\n",
        "\n",
        "    for c_arg in args[1:]:\n",
        "        result = f\"({result} or ({c_arg}))\"\n",
        "\n",
        "    return result\n",
        "\n",
        "def l_imply(arg1, arg2):\n",
        "    \"\"\"Funkce pro spojení dvou výroků pomocí logické spojky implikace.\n",
        "    \"\"\"\n",
        "\n",
        "    return f\"(({arg1}) => ({arg2}))\"\n",
        "\n",
        "def infer(conclusion, *premises):\n",
        "    \"\"\"Funkce, která pro závěr (conclusion) a nenulový počet premis (premises)\n",
        "    vytvoří správně uzávorkovanou formuli, kterou půjde přímo použít pro vyhodnocení\n",
        "    pomocí ttg.\n",
        "    \"\"\"\n",
        "\n",
        "    assert len(premises) > 0, \"Lze použít pouze pro jednu a více premis\"\n",
        "    return l_imply(l_and(*premises), conclusion)"
      ],
      "metadata": {
        "id": "RnVVWfg25XOj"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "def construct_tree(expression: nltk.sem.Expression, is_lambda: bool = False, variable: lg.Variable = None):\n",
        "    \"\"\"Funkce, která výstup NLTK převede do stromové struktury.\n",
        "    Funkce prozatím nepokrývá veškeré možnosti výstupu NLTK,\n",
        "    pro naši potřebu je ale postačující.\n",
        "    \"\"\"\n",
        "    tree = {\"node\": str(expression), \"type\": expression.type}\n",
        "\n",
        "    if isinstance(expression, lg.ApplicationExpression):\n",
        "        if (not is_lambda) or (not isinstance(expression.argument, lg.IndividualVariableExpression)):\n",
        "            tree[\"children\"] = [\n",
        "                construct_tree(expression.function, is_lambda, variable),\n",
        "                construct_tree(expression.argument)\n",
        "            ]\n",
        "        else:\n",
        "            tree = {\n",
        "                \"node\": str(expression),\n",
        "                \"type\": expression.function.type,\n",
        "                \"children\": []\n",
        "            }\n",
        "    elif isinstance(expression, lg.BinaryExpression):\n",
        "        if isinstance(expression, lg.AndExpression):\n",
        "            operand = \"AND\"\n",
        "        elif isinstance(expression, lg.OrExpression):\n",
        "            operand = \"OR\"\n",
        "        elif isinstance(expression, lg.ImpExpression):\n",
        "            operand = \"=>\"\n",
        "        elif isinstance(expression, lg.IffExpression):\n",
        "            operand = \"<=>\"\n",
        "        if not is_lambda:\n",
        "            tree[\"children\"] = [\n",
        "                construct_tree(expression.first),\n",
        "                {\"node\": f\"{operand} {expression.second}\", \"type\": \"<t,t>\", \"children\": [{\"node\": operand, \"type\": \"<t,<t,t>>\"}, construct_tree(expression.second)]}\n",
        "            ]\n",
        "        else:\n",
        "            tree[\"children\"] = [\n",
        "                construct_tree(lg.LambdaExpression(variable, expression.first), True, variable),\n",
        "                construct_tree(lg.LambdaExpression(variable, expression.second), True, variable)\n",
        "            ]\n",
        "    elif isinstance(expression, lg.NegatedExpression):\n",
        "        if not is_lambda:\n",
        "            tree[\"children\"] = [\n",
        "                {\"node\": \"NOT\", \"type\": \"<t,t>\"},\n",
        "                construct_tree(expression.term)\n",
        "            ]\n",
        "        else:\n",
        "            child = construct_tree(lg.LambdaExpression(variable, expression.term), True, variable)\n",
        "            tree = {\n",
        "                \"node\": str(expression),\n",
        "                \"type\": child[\"type\"],\n",
        "                \"children\": [child]\n",
        "            }\n",
        "    elif isinstance(expression, lg.LambdaExpression):\n",
        "        tree[\"children\"] = construct_tree(expression.term, True, expression.variable)[\"children\"]\n",
        "    return tree"
      ],
      "metadata": {
        "id": "VH2tn42a8cjY"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "def id_generator():\n",
        "    \"\"\"Generátor unikátních ID - jsou níže použita pro jednoznačné identifikování uzlů v grafu\n",
        "    \"\"\"\n",
        "    idx = 0\n",
        "    while True:\n",
        "        yield str(idx)\n",
        "        idx += 1\n",
        "\n",
        "def generate_graph(graph):\n",
        "    \"\"\"Ze stromové struktury vytvořené pomocí construct_tree vykreslí graf\n",
        "    \"\"\"\n",
        "    dot = gv.Digraph(node_attr={\"shape\": \"plaintext\"}, edge_attr={\"dir\": \"back\"})\n",
        "    nodeid = id_generator()\n",
        "    root = next(nodeid)\n",
        "    dot.node(root, f\"{graph['node']}\\ntyp: {graph['type']}\")\n",
        "\n",
        "    def add_level(parent, children, digraph, id_gen):\n",
        "        for child in children:\n",
        "            node = next(id_gen)\n",
        "            digraph.node(node, f\"{child['node']}\\ntyp: {child['type']}\")\n",
        "            digraph.edge(parent, node)\n",
        "            add_level(node, child.get(\"children\", []), digraph, id_gen)\n",
        "\n",
        "    add_level(root, graph.get(\"children\", []), dot, nodeid)\n",
        "    return dot"
      ],
      "metadata": {
        "id": "-yQ3y7ZuBJHc"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "def type_analysis(expression, signature):\n",
        "    \"\"\"Funkce, která na základě zadaného výrazu a přiřazení typů vykreslí strom s typy.\n",
        "    \"\"\"\n",
        "    expr = nltk.sem.Expression.fromstring(expression, signature=signature, type_check=True)\n",
        "    tree = construct_tree(expr)\n",
        "    return generate_graph(tree)"
      ],
      "metadata": {
        "id": "PakDXGXhGmbl"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "source": [
        "## Domácí úloha\n",
        "\n",
        "### Zadání a bodování\n",
        "\n",
        "Níže máte zadané dva argumenty. U argumentů už máte identifikované premisy a závěr. Jednotlivé premisy a závěr přepište pomocí logických formulí a vyhodnoťte s pomocí knihovny `ttg` (tj. `print(ttg.Truths([...], [...]))`). Ke každému argumentu uveďte, jestli je na základě pravdivostní tabulky deduktivně platný, nebo neplatný. Za převedení každého argumentu do logických formulí, použití `ttg` a rozhodnutí o deduktivní platnosti argumentu můžete dostat až 3 body (6 bodů dohromady za oba argumenty).\n",
        "\n",
        "Ke každému argumentu máte uvedenu jednu větu pro typovou analýzu. Věta může být pro jednoduchost mírně upravená oproti příslušné větě z argumentu. Za typovou analýzu každé věty můžete dostat až 2 body, dohromady tak 4 body.\n",
        "\n",
        "### Pravdivostní tabulky - pomocné funkce\n",
        "\n",
        "Podobně jako u první domácí úlohy máte k dispozici pomocné funkce, které vám mohou pomoct s uzávorkováním logických formulí.\n",
        "\n",
        "Pomocné funkce lze využít k zápisu logických formulí\n",
        "Místo \"a and b\" lze použít zápis `l_and(\"a\", \"b\")`, funkce zajistí i uzávorkování formule.\n",
        "\n",
        "Funkce infer vytvoří konjunkci ze všech vložených premis a vloží je do implikace se závěrem (závěr se v případě této funkce vkládá na první pozici!)\n",
        "Použití funkcí lze kombinovat se standardním zápisem\n",
        "`\"a and (-b)\"` lze zapsat jako `l_and(\"a\", l_not(\"b\"))`, ale také jako `l_and(\"a\", \"-b\")`.\n",
        "\n",
        "Funkce závorkují velmi agresivně (víc než by bylo nutné), abyste se vy o závorkování nemuseli starat\n",
        "Níže ukázka na cvičení 4 z minulého týdne (nejdříve varianta bez použití funkcí, pak s)\n",
        "\n",
        "### Typová analýza\n",
        "\n",
        "Podobně jako v případě domácí úlohy číslo 2 stačí zadat typy do předpřipraveného \"slovníku\" (taková ta struktura ve složených závorkách).\n",
        "\n",
        "V textech se můžou vyskytovat jmenné fráze v rolích příslovečných určení, případně přívlastků. Věřím, že se tím nenecháte zmást, stále se jedná o množiny (a jejich průniky).\n",
        "\n",
        "Původně jsem se chtěl vyhnout \"shifteru\" `ten`, ukázalo se ale, že by se tím věci spíše zkomplikovaly, proto na něj můžete u některých vět narazit (vždy jsem použil `ten`, i když by někdy bylo vhodnější použití například `ta` apod.).\n",
        "\n",
        "Vlastní jména (případně přezdívky s velkým písmenem na začátku) jsou uvažovány jako entity."
      ],
      "metadata": {
        "id": "L1Hzmo0BGuV-"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "### Úloha 1\n",
        "\n",
        "#### Argument:\n",
        "\n",
        "##### Premisy:\n",
        "\n",
        "* Kdyby Vlahoš slyšel křik bánší, umřel by strašlivou smrtí.\n",
        "* Kdyby Vlahoš umřel strašlivou smrtí, Vetinari by hledal nového poštmistra.\n",
        "* Vetinari nového poštmistra nehledal.\n",
        "\n",
        "##### Závěr:\n",
        "\n",
        "* Vlahoš neslyšel křik bánší."
      ],
      "metadata": {
        "id": "FW-jBjpSosWh"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "print(ttg.Truths([], []))"
      ],
      "metadata": {
        "id": "fRbK_XKAmgnr"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "source": [
        "Je argument deduktivně platný?"
      ],
      "metadata": {
        "id": "Ypg4tBnSmnB1"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "#### Typová analýza\n",
        "\n",
        "* Kdyby Vlahoš slyšel bánší, umřel by strašlivou smrtí."
      ],
      "metadata": {
        "id": "dS1qqjY7mqET"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "sig = {\n",
        "    \"slyšet\": \"\",\n",
        "    \"ten\": \"\",\n",
        "    \"bánší\": \"\",\n",
        "    \"Vlahoš\": \"\",\n",
        "    \"umřít\": \"\",\n",
        "    \"strašlivá\": \"\",\n",
        "    \"smrt\": \"\",\n",
        "}\n",
        "\n",
        "type_analysis(r\"(\\x.slyšet(x, ten(\\y.bánší(y)))(Vlahoš) => \\x.(umřít(x) & (strašlivá(x) & smrt(x)))(Vlahoš))\", sig)"
      ],
      "metadata": {
        "id": "9tvTxejap1lK"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "source": [
        "### Úloha 2\n",
        "\n",
        "#### Argument:\n",
        "\n",
        "##### Premisy:\n",
        "\n",
        "* Pokud Tyler Durden převezme kontrolu, mýdlo nebude v obchodech k dostání.\n",
        "* Pokud nebude mýdlo v obchodech k dostání, anarchie povládne světu.\n",
        "\n",
        "##### Závěr:\n",
        "\n",
        "* Tyler Durden převzal kontrolu, ale anarchie světu nevládne."
      ],
      "metadata": {
        "id": "3eMUaSSwnErE"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "print(ttg.Truths([], []))"
      ],
      "metadata": {
        "id": "qqPwzo87nErG"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "source": [
        "Je argument deduktivně platný?"
      ],
      "metadata": {
        "id": "WWaNVZsfnErG"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "#### Typová analýza\n",
        "\n",
        "* Pokud Tyler Durden převezme kontrolu, mýdlo nebude v obchodech k dostání."
      ],
      "metadata": {
        "id": "Jpnt63kanErH"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "sig = {\n",
        "    \"převzít\": \"\",\n",
        "    \"ten\": \"\",\n",
        "    \"kontrola\": \"\",\n",
        "    \"Tyler_Durden\": \"\",\n",
        "    \"být_k_dostání\": \"\",\n",
        "    \"v_obchodech\": \"\",\n",
        "    \"mýdlo\": \"\",\n",
        "}\n",
        "\n",
        "type_analysis(r\"\\x.převzít(x, ten(\\y.kontrola(y)))(Tyler_Durden) => \\x.(být_k_dostání(x) & v_obchodech(x))(ten(\\y.mýdlo(y)))\", sig)"
      ],
      "metadata": {
        "id": "fTAT5o60nErH"
      },
      "execution_count": null,
      "outputs": []
    }
  ]
}