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

# ## Artificial Intelligence, Lab 4
# 
# Propositional logic, Conjunctive Normal Forms, resolution, Horn clauses, forward and backward chaining 

# ### Exercise I.
# 
# Recall that an implication $\alpha \Rightarrow \beta$ is valid if 
# 
# (R&N) which of the following propositions are correct?
# 
# - False $\vDash$ True
# - True $\vDash$ False
# - $(A\wedge B)\vDash (A\Leftrightarrow B)$
# - $A \Leftrightarrow B \vDash A \vee B$
# - $A \Leftrightarrow B \vDash \lnot A \vee B$
# - $(A\wedge B) \Rightarrow C\vDash (A\Rightarrow C)\vee (B\Rightarrow C)$
# - $(C\wedge (\lnot A\wedge \lnot B))\equiv ((A\Rightarrow C)\wedge (B\Rightarrow C))$
# - $(A\vee B)\wedge (\lnot C\vee \lnot D\vee E)\vDash (A\vee B)$
# - $(A\vee B)\wedge (\lnot C\vee \lnot D\vee E)\vDash (A\vee B)\wedge (\lnot D\vee E)$
# 
# Recall that 
# 
# for any sentences $\alpha$ and $\beta$, we write $\alpha\vDash \beta$ if and only if the sentence $\alpha\Rightarrow \beta$ is valid (true in every row from the truth table). Moreover, $\alpha \vDash \beta$ if and only if the sentence $\alpha\wedge \lnot \beta$ is unsatisfiable. Recall that a sentence is satisfiable if it is true in some model. Consequently $\alpha$ is satisfiable iff $\lnot \alpha$ is not valid.
# 
# Finally, any two sentences are equivalent if and only if $\alpha \vDash \beta$ and $\beta \vDash \alpha$.  

# ### Exercise II, Propositional connectives 
# 
# At the end of this exercise, you should have a way to store and decompose logical expressions. 

# #### Exercise II.1.
# 
# We will encode symbols as strings starting with an uppercase letter such as 'A', 'Aa' or 'Bonjour'. When decomposing a propositional expression into its components, we will need a function that tells us whenever we have reached such symbol, called 'literal' and not an expression (with underlying connectives). Complete the function 'is_symbol' below which should check whether a given object is a literal or not.

# In[ ]:


def is_symbol(exp):
    
    '''the function should return True if the expression stored in exp is 
    a literal (single symbol), i.e. if exp is a string that starts with an upper 
    case letter'''
    
    
    if # complete the clause
    
        return True 
    
    else:
        return False


# #### Exercise II.2.
# 
# Conjunctions and disjunctions. Complete the code below by providing for each object, a function strRepresentation that displays the proposition as a string. Use recursion in order to unfold the whole proposition. Test your function by encoding by displaying a couple of propostions. we will use the symbols '&' '|' and '=>' as well as '<=>' to display ther espective logical connectives

# In[ ]:


class LogicalOr:
    
    '''class '''
    
    def __init__(self, arg1, arg2):
        
        self.arg1 = arg1
        self.arg2 = arg2
        
        
    def strRepresentation():
        
        '''complete'''
        
class LogicalAnd:
    

    def __init__(self,arg1, arg2):
        
        self.arg1 = arg1
        self.arg2 = arg2
        
    def strRepresentation():
        
        '''complete'''
        


# #### Exercise II.3. 
# 
# Extend the two classes above and include the implication, equivalence and the negation

# In[ ]:


class LogicalNot:
    
    def __init__(self, arg1):
        
        self.arg1 = arg1        
        
    def strRepresentation():
        
        '''complete'''
        
class LogicalEquivalence:
    

    def __init__(self,arg1, arg2):
        
        self.arg1 = arg1
        self.arg2 = arg2
        
    def strRepresentation():
        

class LogicalImplication:
    
    def __init__(self, arg1, arg2):
        
        self.arg1 = arg1
        self.arg2 = arg2
        
        
    def strRepresentation():
        
        '''complete'''
        
class LogicalEquivalence:
    

    def __init__(self,arg1, arg2):
        
        self.arg1 = arg1
        self.arg2 = arg2
        
    def strRepresentation():
        
        '''complete'''
        


# ### Exercise III. Conjunctive Normal Forms. 
# 
# By relying on the objects defined above, turn a general expression from propositional logic into a conjunctive normal form (CNF). Recall that the precedence rule are encoded by the order in wich the Propositional objects are built. We rely on the following rules
# 
# - $\Leftrightarrow$ Elimination. replace $\alpha \Rightarrow \beta $ with $(\alpha\Rightarrow \beta )\wedge (\beta \Rightarrow \alpha)$
# - $\Rightarrow$ Elimination. Replace $\alpha \Rightarrow \beta $ with $\not \alpha \vee \beta$ 
# - Distribbution of $\lnot$: iteratively apply any of the following three steps
# 
#     - $\lnot(\lnot \alpha ) \equiv \alpha$ (double negation elimination)
#     - $\lnot(\alpha\wedge \beta) \equiv (\lnot \alpha \vee \lnot \beta) $ (De Morgan)
#     - $\lnot(\alpha \vee \beta) \equiv (\lnot \alpha \wedge \lnot\beta )$
# 
# - Distribution of $\vee$ over $\wedge$. $(\alpha\vee (\beta \wedge \gamma))\equiv ((\alpha \vee \beta)\wedge(\alpha \vee \gamma))$

# In[ ]:


def to_Conjunctive_NormalForm(proposition):
    
    '''The function should return the CNF for the given proposition'''
    
    
    return propositionCNF


# ### Exercise IV. Resolution rules
# 
# Recall that the general resolution rule takes as premises two disjunctions and return a disjunction. I.e.
# 
# $$\frac{\ell_1\vee \ldots \vee \ell_k, \quad m_1\vee \ldots m_n}{\ell_1\vee \ldots \ell_{i-1}\vee \ell_{i+1}\vee \ldots \ell_k\vee m_1\vee m_{j-1}\vee m_{j+1}\vee \ldots m_n}$$
# 
# 
# #### Exercise IV.1. Resolution function
# 
# complete the function CNFresolution below which takes two disjunctions as premises and return all the propositions that can be derived from those clauses through validation.
# 
# Apply your resolution algorithm to the Wumpus example where KB is represented by the proposition $(B_{1,1}\Leftrightarrow (P_{1,2}\vee P_{2,1}))\wedge \lnot B_{1,1}$ and we want to prove that $KB\vDash \lnot P_{1,2}$
# 

# In[ ]:


### 

def resolution(clause1, clause2):
    
    '''the function should return '''
    
    
    
    
    return proposition


# #### Exercise IV.4. Resolution algorithm. 
# 
# Code the resolution algorithm below. recall that this algorithm iterates on the following steps:
#     
# <img src="PLresolution.png">
# 
# 
# Start by trying the algorithm with simple KB such as single simple propositions. 

# In[ ]:


def resolutionAlgorithm(KB, proposition):
    
    '''The algorithm should return true if the sentence stored in Proposition is 
    entailed by the knowledge base KB'''
    
    
    
    
    return conclusion


# #### Exercise IV.3. Propositional 2CNF
# 
# A propositional 2-CNF expression is a conjunction of clauses, each containing _exactly_ two literals. As an example, consider the 2-CNF below:
#     
# $$(A\vee B)\wedge (\lnot A\vee C)\wedge (\lnot B\vee D)\wedge (\lnot C\vee G)\wedge (\lnot D\vee G)$$
# 
# Use your resolution algorithm to show that the knowledge base $KB$ represented by the single 2-CNF above entails the literal $G$.

# ### Exercise V. Horn clauses and Forward chaining. 

# A Horn clause is a disjunction of literals with at most one positive literal. As an example
# 
# such clauses are particulary interesting because a clause of the form $(\lnot A\vee \lnot B\vee C)$ can always be writte as $(A\wedge B)\Rightarrow C$.
# 
# Given a set of Horn clauses, we can determine whether the set entails a particular literal by using the Forward or Backward chaining algorithms which run in linear time in the size of the knowledge base. 
# 
# <img src="PLresolutionHorn.png">
# 
# 

# Code this algorithm below and test it on the KB give by
# 
# - $P\Rightarrow Q$
# - $L \wedge M \Rightarrow P$
# - $B\wedge L \Rightarrow M$
# - $A\wedge P\Rightarrow L$
# - $A\wedge B\Rightarrow L$
# - $A$
# - $B$

# In[ ]:


def ForwardChainingPL(KB, proposition):
    
    '''the function should determine the value of the literal stored in proposition 
    from the set of Horn clauses stored in the knowledge base KB'''
    
    
    
    return conclusion