Last active
December 5, 2018 11:30
-
-
Save chokkan/b97833da26488b81bb1a05adae99acc2 to your computer and use it in GitHub Desktop.
logic
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| { | |
| "nbformat": 4, | |
| "nbformat_minor": 0, | |
| "metadata": { | |
| "colab": { | |
| "name": "logic.ipynb", | |
| "version": "0.3.2", | |
| "provenance": [], | |
| "include_colab_link": true | |
| }, | |
| "kernelspec": { | |
| "display_name": "Python 3", | |
| "language": "python", | |
| "name": "python3" | |
| } | |
| }, | |
| "cells": [ | |
| { | |
| "cell_type": "markdown", | |
| "metadata": { | |
| "id": "view-in-github", | |
| "colab_type": "text" | |
| }, | |
| "source": [ | |
| "<a href=\"https://colab.research.google.com/gist/chokkan/00b09dc775590ac1035c1b111ff68274/logic.ipynb\" target=\"_parent\"><img src=\"https://colab.research.google.com/assets/colab-badge.svg\" alt=\"Open In Colab\"/></a>" | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "pX-fF1b0EhsL", | |
| "colab_type": "text" | |
| }, | |
| "cell_type": "markdown", | |
| "source": [ | |
| "# Pythonによる命題論理（sympy.logic）" | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "UYpnsEH-EhsM", | |
| "colab_type": "text" | |
| }, | |
| "cell_type": "markdown", | |
| "source": [ | |
| "[Google Colaboratory](https://colab.research.google.com/)を使うと，Pythonのプログラムをブラウザ上で動かすことができる．Pythonの豊富なライブラリの一つである[SymPy](http://www.sympy.org/)を使って，命題論理の演算や簡略化，真理値表の描画，真理値表から標準形を得る処理の例を示す．" | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "IDf8YfE8EhsN", | |
| "colab_type": "text" | |
| }, | |
| "cell_type": "markdown", | |
| "source": [ | |
| "まず，SymPyというライブラリを読み込む．Google Colaboratory上で数式を綺麗に表示するため，色々とおまじないを書いておく（中身を理解しなくてもよい）．" | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "MYEyfh7kEhsP", | |
| "colab_type": "code", | |
| "colab": {} | |
| }, | |
| "cell_type": "code", | |
| "source": [ | |
| "import sympy\n", | |
| "from sympy import *\n", | |
| "from sympy.logic import SOPform, POSform\n", | |
| "\n", | |
| "def custom_latex_printer(exp,**options):\n", | |
| " from google.colab.output._publish import javascript\n", | |
| " url = \"https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.3/latest.js?config=default\"\n", | |
| " javascript(url=url)\n", | |
| " return sympy.printing.latex(exp,**options)\n", | |
| "init_printing(use_latex=\"mathjax\",latex_printer=custom_latex_printer)" | |
| ], | |
| "execution_count": 0, | |
| "outputs": [] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "ujxtjZWQEhsS", | |
| "colab_type": "text" | |
| }, | |
| "cell_type": "markdown", | |
| "source": [ | |
| "命題変数$a,b$を宣言" | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "WrxyU7gAEhsT", | |
| "colab_type": "code", | |
| "colab": {} | |
| }, | |
| "cell_type": "code", | |
| "source": [ | |
| "a, b = symbols('a,b')" | |
| ], | |
| "execution_count": 0, | |
| "outputs": [] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "LrunXVzGEhsX", | |
| "colab_type": "text" | |
| }, | |
| "cell_type": "markdown", | |
| "source": [ | |
| "## 論理積" | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "xXnWF1DGEhsY", | |
| "colab_type": "code", | |
| "colab": { | |
| "base_uri": "https://localhost:8080/", | |
| "height": 66 | |
| }, | |
| "outputId": "c56a852b-cf87-4c31-e88b-e05932c84334" | |
| }, | |
| "cell_type": "code", | |
| "source": [ | |
| "a & b" | |
| ], | |
| "execution_count": 3, | |
| "outputs": [ | |
| { | |
| "output_type": "display_data", | |
| "data": { | |
| "text/html": [ | |
| "<script src='https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.3/latest.js?config=default'></script>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| } | |
| }, | |
| { | |
| "output_type": "execute_result", | |
| "data": { | |
| "text/latex": "$$a \\wedge b$$", | |
| "text/plain": [ | |
| "a ∧ b" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| }, | |
| "execution_count": 3 | |
| } | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "H66kF-ALEhse", | |
| "colab_type": "code", | |
| "colab": { | |
| "base_uri": "https://localhost:8080/", | |
| "height": 66 | |
| }, | |
| "outputId": "f6d2ad2d-4dcb-46ba-a007-82df636a23ea" | |
| }, | |
| "cell_type": "code", | |
| "source": [ | |
| "(a & b).subs({a: True, b: False})" | |
| ], | |
| "execution_count": 4, | |
| "outputs": [ | |
| { | |
| "output_type": "display_data", | |
| "data": { | |
| "text/html": [ | |
| "<script src='https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.3/latest.js?config=default'></script>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| } | |
| }, | |
| { | |
| "output_type": "execute_result", | |
| "data": { | |
| "text/latex": "$$\\mathrm{False}$$", | |
| "text/plain": [ | |
| "False" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| }, | |
| "execution_count": 4 | |
| } | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "9hce9VRaEhsi", | |
| "colab_type": "text" | |
| }, | |
| "cell_type": "markdown", | |
| "source": [ | |
| "## 論理和" | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "hiy4A9yzEhsj", | |
| "colab_type": "code", | |
| "colab": { | |
| "base_uri": "https://localhost:8080/", | |
| "height": 66 | |
| }, | |
| "outputId": "1b88f5c2-c858-4236-973d-fa51c9d53950" | |
| }, | |
| "cell_type": "code", | |
| "source": [ | |
| "a | b" | |
| ], | |
| "execution_count": 5, | |
| "outputs": [ | |
| { | |
| "output_type": "display_data", | |
| "data": { | |
| "text/html": [ | |
| "<script src='https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.3/latest.js?config=default'></script>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| } | |
| }, | |
| { | |
| "output_type": "execute_result", | |
| "data": { | |
| "text/latex": "$$a \\vee b$$", | |
| "text/plain": [ | |
| "a ∨ b" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| }, | |
| "execution_count": 5 | |
| } | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "cNkd-sP7Ehsn", | |
| "colab_type": "code", | |
| "colab": { | |
| "base_uri": "https://localhost:8080/", | |
| "height": 66 | |
| }, | |
| "outputId": "20ba7c7d-cb81-44ca-c11a-341189aebc9b" | |
| }, | |
| "cell_type": "code", | |
| "source": [ | |
| "(a | b).subs({a: True, b: False})" | |
| ], | |
| "execution_count": 6, | |
| "outputs": [ | |
| { | |
| "output_type": "display_data", | |
| "data": { | |
| "text/html": [ | |
| "<script src='https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.3/latest.js?config=default'></script>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| } | |
| }, | |
| { | |
| "output_type": "execute_result", | |
| "data": { | |
| "text/latex": "$$\\mathrm{True}$$", | |
| "text/plain": [ | |
| "True" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| }, | |
| "execution_count": 6 | |
| } | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "tSIbMQu0Ehsr", | |
| "colab_type": "text" | |
| }, | |
| "cell_type": "markdown", | |
| "source": [ | |
| "## 否定" | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "018lDW-EEhss", | |
| "colab_type": "code", | |
| "colab": { | |
| "base_uri": "https://localhost:8080/", | |
| "height": 66 | |
| }, | |
| "outputId": "a1e37c6e-d1b8-4604-bb50-5e0ede4f7b4b" | |
| }, | |
| "cell_type": "code", | |
| "source": [ | |
| "~a" | |
| ], | |
| "execution_count": 7, | |
| "outputs": [ | |
| { | |
| "output_type": "display_data", | |
| "data": { | |
| "text/html": [ | |
| "<script src='https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.3/latest.js?config=default'></script>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| } | |
| }, | |
| { | |
| "output_type": "execute_result", | |
| "data": { | |
| "text/latex": "$$\\neg a$$", | |
| "text/plain": [ | |
| "¬a" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| }, | |
| "execution_count": 7 | |
| } | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "o1QrKeroEhsw", | |
| "colab_type": "code", | |
| "colab": { | |
| "base_uri": "https://localhost:8080/", | |
| "height": 66 | |
| }, | |
| "outputId": "e2b7cd9d-1e83-4694-ec07-87a8e99de3de" | |
| }, | |
| "cell_type": "code", | |
| "source": [ | |
| "(~a).subs({a: False})" | |
| ], | |
| "execution_count": 8, | |
| "outputs": [ | |
| { | |
| "output_type": "display_data", | |
| "data": { | |
| "text/html": [ | |
| "<script src='https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.3/latest.js?config=default'></script>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| } | |
| }, | |
| { | |
| "output_type": "execute_result", | |
| "data": { | |
| "text/latex": "$$\\mathrm{True}$$", | |
| "text/plain": [ | |
| "True" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| }, | |
| "execution_count": 8 | |
| } | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "K5wgo7UkEhsz", | |
| "colab_type": "text" | |
| }, | |
| "cell_type": "markdown", | |
| "source": [ | |
| "## 含意" | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "t4xIyrrnEhs1", | |
| "colab_type": "code", | |
| "colab": { | |
| "base_uri": "https://localhost:8080/", | |
| "height": 66 | |
| }, | |
| "outputId": "f7690c8b-cc01-462d-dfe1-7fd0378acf64" | |
| }, | |
| "cell_type": "code", | |
| "source": [ | |
| "a >> b" | |
| ], | |
| "execution_count": 9, | |
| "outputs": [ | |
| { | |
| "output_type": "display_data", | |
| "data": { | |
| "text/html": [ | |
| "<script src='https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.3/latest.js?config=default'></script>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| } | |
| }, | |
| { | |
| "output_type": "execute_result", | |
| "data": { | |
| "text/latex": "$$a \\Rightarrow b$$", | |
| "text/plain": [ | |
| "a → b" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| }, | |
| "execution_count": 9 | |
| } | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "w3GIU2J7Ehs6", | |
| "colab_type": "code", | |
| "colab": { | |
| "base_uri": "https://localhost:8080/", | |
| "height": 66 | |
| }, | |
| "outputId": "03afd99b-ed2a-4eb2-d6b1-cb11f3b41edf" | |
| }, | |
| "cell_type": "code", | |
| "source": [ | |
| "(a >> b).subs({a: False, b: False})" | |
| ], | |
| "execution_count": 10, | |
| "outputs": [ | |
| { | |
| "output_type": "display_data", | |
| "data": { | |
| "text/html": [ | |
| "<script src='https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.3/latest.js?config=default'></script>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| } | |
| }, | |
| { | |
| "output_type": "execute_result", | |
| "data": { | |
| "text/latex": "$$\\mathrm{True}$$", | |
| "text/plain": [ | |
| "True" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| }, | |
| "execution_count": 10 | |
| } | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "1TK4XsVbEhs9", | |
| "colab_type": "text" | |
| }, | |
| "cell_type": "markdown", | |
| "source": [ | |
| "## 同値" | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "C3MTp_sbEhs_", | |
| "colab_type": "code", | |
| "colab": { | |
| "base_uri": "https://localhost:8080/", | |
| "height": 66 | |
| }, | |
| "outputId": "7206003e-c720-4636-b871-5fd376180139" | |
| }, | |
| "cell_type": "code", | |
| "source": [ | |
| "Equivalent(a, b)" | |
| ], | |
| "execution_count": 11, | |
| "outputs": [ | |
| { | |
| "output_type": "display_data", | |
| "data": { | |
| "text/html": [ | |
| "<script src='https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.3/latest.js?config=default'></script>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| } | |
| }, | |
| { | |
| "output_type": "execute_result", | |
| "data": { | |
| "text/latex": "$$a \\equiv b$$", | |
| "text/plain": [ | |
| "a ≡ b" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| }, | |
| "execution_count": 11 | |
| } | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "YUDeRSDOEhtD", | |
| "colab_type": "code", | |
| "colab": { | |
| "base_uri": "https://localhost:8080/", | |
| "height": 66 | |
| }, | |
| "outputId": "bc1b6ee6-182f-4be8-e16f-deb433488d08" | |
| }, | |
| "cell_type": "code", | |
| "source": [ | |
| "Equivalent(a, b).subs({a: False, b: True})" | |
| ], | |
| "execution_count": 12, | |
| "outputs": [ | |
| { | |
| "output_type": "display_data", | |
| "data": { | |
| "text/html": [ | |
| "<script src='https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.3/latest.js?config=default'></script>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| } | |
| }, | |
| { | |
| "output_type": "execute_result", | |
| "data": { | |
| "text/latex": "$$\\mathrm{False}$$", | |
| "text/plain": [ | |
| "False" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| }, | |
| "execution_count": 12 | |
| } | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "F2BS_vL3EhtI", | |
| "colab_type": "text" | |
| }, | |
| "cell_type": "markdown", | |
| "source": [ | |
| "## 真理値表を書く" | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "6_pUlLtkEhtJ", | |
| "colab_type": "text" | |
| }, | |
| "cell_type": "markdown", | |
| "source": [ | |
| "真理値表を書くプログラムは自前で実装する．" | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "Hhv9PQJKEhtK", | |
| "colab_type": "code", | |
| "colab": {} | |
| }, | |
| "cell_type": "code", | |
| "source": [ | |
| "def b2i(b):\n", | |
| " return 1 if b else 0\n", | |
| "\n", | |
| "def explore(expr_string):\n", | |
| " expr = sympify(expr_string)\n", | |
| " variables = sorted(expr.free_symbols, key=lambda v: str(v))\n", | |
| " print('{} | f'.format(' '.join([str(v) for v in variables])))\n", | |
| " print('{}-+--'.format('-'.join(['-' for v in variables])))\n", | |
| " for truth_values in cartes([False, True], repeat=len(variables)):\n", | |
| " values = dict(zip(variables, truth_values))\n", | |
| " print('{} | {}'.format(' '.join([str(b2i(x)) for x in values.values()]), b2i(expr.subs(values))))" | |
| ], | |
| "execution_count": 0, | |
| "outputs": [] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "WYUpix0NEhtN", | |
| "colab_type": "code", | |
| "colab": { | |
| "base_uri": "https://localhost:8080/", | |
| "height": 122 | |
| }, | |
| "outputId": "b0f35621-c69a-4af3-d0e6-f79fbf6b2c1c" | |
| }, | |
| "cell_type": "code", | |
| "source": [ | |
| "explore(\"a >> (b >> a)\")" | |
| ], | |
| "execution_count": 14, | |
| "outputs": [ | |
| { | |
| "output_type": "stream", | |
| "text": [ | |
| "a b | f\n", | |
| "----+--\n", | |
| "0 0 | 1\n", | |
| "0 1 | 1\n", | |
| "1 0 | 1\n", | |
| "1 1 | 1\n" | |
| ], | |
| "name": "stdout" | |
| } | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "FcBNAaNCEhtR", | |
| "colab_type": "text" | |
| }, | |
| "cell_type": "markdown", | |
| "source": [ | |
| "## 命題論理式を簡素化する" | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "doUVyBjFEhtS", | |
| "colab_type": "code", | |
| "colab": { | |
| "base_uri": "https://localhost:8080/", | |
| "height": 66 | |
| }, | |
| "outputId": "48acbab4-3503-4e60-cd86-8fb81ff493f2" | |
| }, | |
| "cell_type": "code", | |
| "source": [ | |
| "simplify(\"(a | b) & (~a | b)\")" | |
| ], | |
| "execution_count": 15, | |
| "outputs": [ | |
| { | |
| "output_type": "display_data", | |
| "data": { | |
| "text/html": [ | |
| "<script src='https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.3/latest.js?config=default'></script>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| } | |
| }, | |
| { | |
| "output_type": "execute_result", | |
| "data": { | |
| "text/latex": "$$b$$", | |
| "text/plain": [ | |
| "b" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| }, | |
| "execution_count": 15 | |
| } | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "nN8gTKVgEhtV", | |
| "colab_type": "text" | |
| }, | |
| "cell_type": "markdown", | |
| "source": [ | |
| "## 真理値表から標準形を得る" | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "09L5oy5OEhtW", | |
| "colab_type": "text" | |
| }, | |
| "cell_type": "markdown", | |
| "source": [ | |
| "`SOPform`関数は積和標準形（sum of products）を求める．第１引数は命題変数，第２引数は全体が真になるときの各変数の真理値のリスト（真理値表の行）のリスト（真理値表）という形で与える．" | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "hhtuRC2eEhtX", | |
| "colab_type": "code", | |
| "colab": { | |
| "base_uri": "https://localhost:8080/", | |
| "height": 66 | |
| }, | |
| "outputId": "b9031d41-f58d-4089-94a3-5366b89fddb8" | |
| }, | |
| "cell_type": "code", | |
| "source": [ | |
| "SOPform([a, b], [[0,1], [1,0]])" | |
| ], | |
| "execution_count": 16, | |
| "outputs": [ | |
| { | |
| "output_type": "display_data", | |
| "data": { | |
| "text/html": [ | |
| "<script src='https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.3/latest.js?config=default'></script>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| } | |
| }, | |
| { | |
| "output_type": "execute_result", | |
| "data": { | |
| "text/latex": "$$\\left(a \\wedge \\neg b\\right) \\vee \\left(b \\wedge \\neg a\\right)$$", | |
| "text/plain": [ | |
| "(a ∧ ¬b) ∨ (b ∧ ¬a)" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| }, | |
| "execution_count": 16 | |
| } | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "Aqdq_LbNEhta", | |
| "colab_type": "text" | |
| }, | |
| "cell_type": "markdown", | |
| "source": [ | |
| "`POSform`関数は和積標準形（product of sums）を求める．第１引数は命題変数，第２引数は全体が真になるときの各変数の真理値のリスト（真理値表の行）のリスト（真理値表）という形で与える．" | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "KRwvxYKcEhtc", | |
| "colab_type": "code", | |
| "colab": { | |
| "base_uri": "https://localhost:8080/", | |
| "height": 66 | |
| }, | |
| "outputId": "01925b7f-2524-4379-ad03-aa5863b0b623" | |
| }, | |
| "cell_type": "code", | |
| "source": [ | |
| "POSform([a, b], [[0,1], [1,0]])" | |
| ], | |
| "execution_count": 17, | |
| "outputs": [ | |
| { | |
| "output_type": "display_data", | |
| "data": { | |
| "text/html": [ | |
| "<script src='https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.3/latest.js?config=default'></script>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| } | |
| }, | |
| { | |
| "output_type": "execute_result", | |
| "data": { | |
| "text/latex": "$$\\left(a \\vee b\\right) \\wedge \\left(\\neg a \\vee \\neg b\\right)$$", | |
| "text/plain": [ | |
| "(a ∨ b) ∧ (¬a ∨ ¬b)" | |
| ] | |
| }, | |
| "metadata": { | |
| "tags": [] | |
| }, | |
| "execution_count": 17 | |
| } | |
| ] | |
| }, | |
| { | |
| "metadata": { | |
| "id": "73cM168tFbkA", | |
| "colab_type": "code", | |
| "colab": {} | |
| }, | |
| "cell_type": "code", | |
| "source": [ | |
| "" | |
| ], | |
| "execution_count": 0, | |
| "outputs": [] | |
| } | |
| ] | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment