{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "As promised on the posts about logical expressions parsing: https://lion137.blogspot.co.uk/2016/12/propositional-logic-evaluation-in.html, I've create a module to check if given propositional calculus formula is a tautology, it may helps when one's learning logic."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "import string\n",
    "import re\n",
    "import operator as op\n",
    "import functools\n",
    "from itertools import product"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now import quoted above blog post:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "from  propositional_logic_eval import *"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "def fill_values(formula):\n",
    "    \"\"\"returns genexp with the all fillings with 0 and 1\"\"\"\n",
    "    letters = ''.join(set(re.findall('[A-Z]', formula)))\n",
    "    for digits in product('10', repeat=len(letters)):\n",
    "         table = str.maketrans(letters, ''.join(digits))\n",
    "         yield formula.translate(table)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This function returns all possible substitutions with 0 and 1 for the variables in the formula as a iterator: "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(~1 -> ~1)\n",
      "(~0 -> ~1)\n",
      "(~1 -> ~0)\n",
      "(~0 -> ~0)\n"
     ]
    }
   ],
   "source": [
    "for x in fill_values('(~P -> ~Q)'):\n",
    "    print(x)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "def is_tautology(formula):\n",
    "    for x in fill_values(formula):\n",
    "        if not evaluate_parse_tree(build_parse_tree(x)):\n",
    "            return False\n",
    "    return True"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Finally, simple test for a tautology in a loop, and of course a few examples:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "is_tautology('(P -> (Q -> P))')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "is_tautology('((P -> (Q -> R)) -> ((P -> Q) -> (P -> R)))')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "is_tautology('((~P -> ~Q) -> (Q -> P))')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "is_tautology('((P && (P -> Q)) -> Q)')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The first free formulas are the axioms of the Lukasiewicz propsitional logic system (https://en.wikipedia.org/wiki/Propositional_calculus) and therefore must be true, the last one is the known modus ponens rule. That was short, thank you."
   ]
  }
 ],
 "metadata": {
  "anaconda-cloud": {},
  "kernelspec": {
   "display_name": "Python [default]",
   "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.5.2"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 1
}