{
  "nbformat": 4,
  "nbformat_minor": 0,
  "metadata": {
    "colab": {
      "provenance": [],
      "collapsed_sections": []
    },
    "kernelspec": {
      "name": "python3",
      "display_name": "Python 3"
    },
    "language_info": {
      "name": "python"
    }
  },
  "cells": [
    {
      "cell_type": "markdown",
      "source": [
        "# Domácí úloha 1\n",
        "\n",
        "---"
      ],
      "metadata": {
        "id": "nECGmqDPwfjV"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "## Instalace a import"
      ],
      "metadata": {
        "id": "QqlKMVNESnAy"
      }
    },
    {
      "cell_type": "code",
      "execution_count": 2,
      "metadata": {
        "id": "YKaRYO1pA_Cu",
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "outputId": "eceb80cd-f3af-4222-f65e-5eb3127539a5"
      },
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "Looking in indexes: https://pypi.org/simple, https://us-python.pkg.dev/colab-wheels/public/simple/\n",
            "Collecting truth-table-generator\n",
            "  Downloading truth_table_generator-1.1.2.tar.gz (14 kB)\n",
            "Requirement already satisfied: numpy in /usr/local/lib/python3.7/dist-packages (from truth-table-generator) (1.21.6)\n",
            "Requirement already satisfied: pandas in /usr/local/lib/python3.7/dist-packages (from truth-table-generator) (1.3.5)\n",
            "Collecting PTable\n",
            "  Downloading PTable-0.9.2.tar.gz (31 kB)\n",
            "Requirement already satisfied: pyparsing in /usr/local/lib/python3.7/dist-packages (from truth-table-generator) (3.0.9)\n",
            "Requirement already satisfied: tabulate in /usr/local/lib/python3.7/dist-packages (from truth-table-generator) (0.8.10)\n",
            "Requirement already satisfied: jinja2 in /usr/local/lib/python3.7/dist-packages (from truth-table-generator) (2.11.3)\n",
            "Requirement already satisfied: MarkupSafe>=0.23 in /usr/local/lib/python3.7/dist-packages (from jinja2->truth-table-generator) (2.0.1)\n",
            "Requirement already satisfied: pytz>=2017.3 in /usr/local/lib/python3.7/dist-packages (from pandas->truth-table-generator) (2022.4)\n",
            "Requirement already satisfied: python-dateutil>=2.7.3 in /usr/local/lib/python3.7/dist-packages (from pandas->truth-table-generator) (2.8.2)\n",
            "Requirement already satisfied: six>=1.5 in /usr/local/lib/python3.7/dist-packages (from python-dateutil>=2.7.3->pandas->truth-table-generator) (1.15.0)\n",
            "Building wheels for collected packages: truth-table-generator, PTable\n",
            "  Building wheel for truth-table-generator (setup.py) ... \u001b[?25l\u001b[?25hdone\n",
            "  Created wheel for truth-table-generator: filename=truth_table_generator-1.1.2-py3-none-any.whl size=13960 sha256=57014e659bd1a4c942f4838009d10d6a16866a4aaf2c5dc6ee76d5465cf29de1\n",
            "  Stored in directory: /root/.cache/pip/wheels/9a/55/b5/77f5756832494eafda92c7a94c1365ac31088a18a3a97dd480\n",
            "  Building wheel for PTable (setup.py) ... \u001b[?25l\u001b[?25hdone\n",
            "  Created wheel for PTable: filename=PTable-0.9.2-py3-none-any.whl size=22925 sha256=871198a06b17e207d92b3f215885a162ce296b4a5d62f5f9cdb7bf6e650f74c8\n",
            "  Stored in directory: /root/.cache/pip/wheels/33/df/2f/674985b3f8a2de3f96357d1eadef5110f74fa91b3785e52a54\n",
            "Successfully built truth-table-generator PTable\n",
            "Installing collected packages: PTable, truth-table-generator\n",
            "Successfully installed PTable-0.9.2 truth-table-generator-1.1.2\n"
          ]
        }
      ],
      "source": [
        "%pip install truth-table-generator"
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "import ttg"
      ],
      "metadata": {
        "id": "1GC4peTNwz5H"
      },
      "execution_count": 3,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "source": [
        "## Pomocné funkce\n",
        "\n",
        "Níže jsou definovány pomocné funkce, které můžete v domácím úkolu použít. Pro použití je potřeba buňku s definicí funkcí spustit. Použití jednotlivých funkcí je vysvětleno níže."
      ],
      "metadata": {
        "id": "Htjfm2x2dym9"
      }
    },
    {
      "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": "LVbHjWAIeSa2"
      },
      "execution_count": 23,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "source": [
        "### Použití pomocných funkcí\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",
        "* 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",
        "* 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)"
      ],
      "metadata": {
        "id": "QiWUrnJFh-eJ"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "print(ttg.Truths([\"p\", \"q\", \"r\", \"s\"], [\"p => q\", \"q => (-r)\", \"s => r\", \"((((p => q) and (q => (-r))) and (s => r)) and p) => (-s)\"]))"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "ovKxj--Gh8Fn",
        "outputId": "e9fa7e18-c3ed-4f7c-f163-3813bbbed54d"
      },
      "execution_count": 5,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "+-----+-----+-----+-----+----------+-------------+----------+-------------------------------------------------------------+\n",
            "|  p  |  q  |  r  |  s  |  p => q  |  q => (-r)  |  s => r  |  ((((p => q) and (q => (-r))) and (s => r)) and p) => (-s)  |\n",
            "|-----+-----+-----+-----+----------+-------------+----------+-------------------------------------------------------------|\n",
            "|  1  |  1  |  1  |  1  |    1     |      0      |    1     |                              1                              |\n",
            "|  1  |  1  |  1  |  0  |    1     |      0      |    1     |                              1                              |\n",
            "|  1  |  1  |  0  |  1  |    1     |      1      |    0     |                              1                              |\n",
            "|  1  |  1  |  0  |  0  |    1     |      1      |    1     |                              1                              |\n",
            "|  1  |  0  |  1  |  1  |    0     |      1      |    1     |                              1                              |\n",
            "|  1  |  0  |  1  |  0  |    0     |      1      |    1     |                              1                              |\n",
            "|  1  |  0  |  0  |  1  |    0     |      1      |    0     |                              1                              |\n",
            "|  1  |  0  |  0  |  0  |    0     |      1      |    1     |                              1                              |\n",
            "|  0  |  1  |  1  |  1  |    1     |      0      |    1     |                              1                              |\n",
            "|  0  |  1  |  1  |  0  |    1     |      0      |    1     |                              1                              |\n",
            "|  0  |  1  |  0  |  1  |    1     |      1      |    0     |                              1                              |\n",
            "|  0  |  1  |  0  |  0  |    1     |      1      |    1     |                              1                              |\n",
            "|  0  |  0  |  1  |  1  |    1     |      1      |    1     |                              1                              |\n",
            "|  0  |  0  |  1  |  0  |    1     |      1      |    1     |                              1                              |\n",
            "|  0  |  0  |  0  |  1  |    1     |      1      |    0     |                              1                              |\n",
            "|  0  |  0  |  0  |  0  |    1     |      1      |    1     |                              1                              |\n",
            "+-----+-----+-----+-----+----------+-------------+----------+-------------------------------------------------------------+\n"
          ]
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "print(ttg.Truths([\"p\", \"q\", \"r\", \"s\"], [l_imply(\"p\", \"q\"), l_imply(\"q\", \"-r\"), l_imply(\"s\", \"r\"), infer(\"-s\", l_imply(\"p\", \"q\"), l_imply(\"q\", \"-r\"), l_imply(\"s\", \"r\"), \"p\")]))"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "Uqj4z3lpja8o",
        "outputId": "ad737a2e-0812-43be-bf5b-cf08a6b87a98"
      },
      "execution_count": 24,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "+-----+-----+-----+-----+----------------+-----------------+----------------+-----------------------------------------------------------------------------------+\n",
            "|  p  |  q  |  r  |  s  |  ((p) => (q))  |  ((q) => (-r))  |  ((s) => (r))  |  ((((((((p) => (q))) and (((q) => (-r)))) and (((s) => (r)))) and (p))) => (-s))  |\n",
            "|-----+-----+-----+-----+----------------+-----------------+----------------+-----------------------------------------------------------------------------------|\n",
            "|  1  |  1  |  1  |  1  |       1        |        0        |       1        |                                         1                                         |\n",
            "|  1  |  1  |  1  |  0  |       1        |        0        |       1        |                                         1                                         |\n",
            "|  1  |  1  |  0  |  1  |       1        |        1        |       0        |                                         1                                         |\n",
            "|  1  |  1  |  0  |  0  |       1        |        1        |       1        |                                         1                                         |\n",
            "|  1  |  0  |  1  |  1  |       0        |        1        |       1        |                                         1                                         |\n",
            "|  1  |  0  |  1  |  0  |       0        |        1        |       1        |                                         1                                         |\n",
            "|  1  |  0  |  0  |  1  |       0        |        1        |       0        |                                         1                                         |\n",
            "|  1  |  0  |  0  |  0  |       0        |        1        |       1        |                                         1                                         |\n",
            "|  0  |  1  |  1  |  1  |       1        |        0        |       1        |                                         1                                         |\n",
            "|  0  |  1  |  1  |  0  |       1        |        0        |       1        |                                         1                                         |\n",
            "|  0  |  1  |  0  |  1  |       1        |        1        |       0        |                                         1                                         |\n",
            "|  0  |  1  |  0  |  0  |       1        |        1        |       1        |                                         1                                         |\n",
            "|  0  |  0  |  1  |  1  |       1        |        1        |       1        |                                         1                                         |\n",
            "|  0  |  0  |  1  |  0  |       1        |        1        |       1        |                                         1                                         |\n",
            "|  0  |  0  |  0  |  1  |       1        |        1        |       0        |                                         1                                         |\n",
            "|  0  |  0  |  0  |  0  |       1        |        1        |       1        |                                         1                                         |\n",
            "+-----+-----+-----+-----+----------------+-----------------+----------------+-----------------------------------------------------------------------------------+\n"
          ]
        }
      ]
    },
    {
      "cell_type": "markdown",
      "source": [
        "## Zadání domácí úlohy\n",
        "\n",
        "* Převeďte následující výroky do podoby logických formulí, označte premisy a závěr a pomocí ttg ověřte jejich deduktivní platnost.\n",
        "* Při vypracování můžete použít pomocné funkce, které máte připravené výše.\n",
        "\n",
        "### Výrok 1\n",
        "\n",
        "Jonathan Strange a pan Norell jsou angličtí mágové. Pan Norell je anglický mág, takže Jonathan Strange není.\n",
        "\n",
        "### Výrok 2\n",
        "\n",
        "Azirafal nebo Crowley byli démoni. Azirafal nebyl démon, takže Crowley byl démon."
      ],
      "metadata": {
        "id": "FUOKDzdXlOif"
      }
    },
    {
      "cell_type": "code",
      "source": [],
      "metadata": {
        "id": "mLDKSyPlni18"
      },
      "execution_count": null,
      "outputs": []
    }
  ]
}