#!/usr/bin/env python
# coding: utf-8

# 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.

# In[1]:


import string
import re
import operator as op
import functools
from itertools import product


# Now import quoted above blog post:

# In[2]:


from  propositional_logic_eval import *


# In[3]:


def fill_values(formula):
    """returns genexp with the all fillings with 0 and 1"""
    letters = ''.join(set(re.findall('[A-Z]', formula)))
    for digits in product('10', repeat=len(letters)):
         table = str.maketrans(letters, ''.join(digits))
         yield formula.translate(table)


# This function returns all possible substitutions with 0 and 1 for the variables in the formula as a iterator: 

# In[4]:


for x in fill_values('(~P -> ~Q)'):
    print(x)


# In[5]:


def is_tautology(formula):
    for x in fill_values(formula):
        if not evaluate_parse_tree(build_parse_tree(x)):
            return False
    return True


# Finally, simple test for a tautology in a loop, and of course a few examples:

# In[6]:


is_tautology('(P -> (Q -> P))')


# In[7]:


is_tautology('((P -> (Q -> R)) -> ((P -> Q) -> (P -> R)))')


# In[8]:


is_tautology('((~P -> ~Q) -> (Q -> P))')


# In[10]:


is_tautology('((P && (P -> Q)) -> Q)')


# 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.