Propositional logic, Conjunctive Normal Forms, resolution, Horn clauses, forward and backward chaining

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

At the end of this exercise, you should have a way to store and decompose logical expressions.

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
```

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'''
```

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'''
```

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
```

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}$$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
```

Code the resolution algorithm below. recall that this algorithm iterates on the following steps:

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
```

A propositional 2-CNF expression is a conjunction of clauses, each containing *exactly* two literals. As an example, consider the 2-CNF below:

Use your resolution algorithm to show that the knowledge base $KB$ represented by the single 2-CNF above entails the literal $G$.

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.

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
```