{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Artificial Intelligence, Lab 4\n",
    "\n",
    "Propositional logic, Conjunctive Normal Forms, resolution, Horn clauses, forward and backward chaining "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Exercise I.\n",
    "\n",
    "Recall that an implication $\\alpha \\Rightarrow \\beta$ is valid if \n",
    "\n",
    "(R&N) which of the following propositions are correct?\n",
    "\n",
    "- False $\\vDash$ True\n",
    "- True $\\vDash$ False\n",
    "- $(A\\wedge B)\\vDash (A\\Leftrightarrow B)$\n",
    "- $A \\Leftrightarrow B \\vDash A \\vee B$\n",
    "- $A \\Leftrightarrow B \\vDash \\lnot A \\vee B$\n",
    "- $(A\\wedge B) \\Rightarrow C\\vDash (A\\Rightarrow C)\\vee (B\\Rightarrow C)$\n",
    "- $(C\\wedge (\\lnot A\\wedge \\lnot B))\\equiv ((A\\Rightarrow C)\\wedge (B\\Rightarrow C))$\n",
    "- $(A\\vee B)\\wedge (\\lnot C\\vee \\lnot D\\vee E)\\vDash (A\\vee B)$\n",
    "- $(A\\vee B)\\wedge (\\lnot C\\vee \\lnot D\\vee E)\\vDash (A\\vee B)\\wedge (\\lnot D\\vee E)$\n",
    "\n",
    "Recall that \n",
    "\n",
    "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.\n",
    "\n",
    "Finally, any two sentences are equivalent if and only if $\\alpha \\vDash \\beta$ and $\\beta \\vDash \\alpha$.  "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Exercise II, Propositional connectives \n",
    "\n",
    "At the end of this exercise, you should have a way to store and decompose logical expressions. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Exercise II.1.\n",
    "\n",
    "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."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "def is_symbol(exp):\n",
    "    \n",
    "    '''the function should return True if the expression stored in exp is \n",
    "    a literal (single symbol), i.e. if exp is a string that starts with an upper \n",
    "    case letter'''\n",
    "    \n",
    "    \n",
    "    if # complete the clause\n",
    "    \n",
    "        return True \n",
    "    \n",
    "    else:\n",
    "        return False"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Exercise II.2.\n",
    "\n",
    "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"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "class LogicalOr:\n",
    "    \n",
    "    '''class '''\n",
    "    \n",
    "    def __init__(self, arg1, arg2):\n",
    "        \n",
    "        self.arg1 = arg1\n",
    "        self.arg2 = arg2\n",
    "        \n",
    "        \n",
    "    def strRepresentation():\n",
    "        \n",
    "        '''complete'''\n",
    "        \n",
    "class LogicalAnd:\n",
    "    \n",
    "\n",
    "    def __init__(self,arg1, arg2):\n",
    "        \n",
    "        self.arg1 = arg1\n",
    "        self.arg2 = arg2\n",
    "        \n",
    "    def strRepresentation():\n",
    "        \n",
    "        '''complete'''\n",
    "        "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Exercise II.3. \n",
    "\n",
    "Extend the two classes above and include the implication, equivalence and the negation"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "class LogicalNot:\n",
    "    \n",
    "    def __init__(self, arg1):\n",
    "        \n",
    "        self.arg1 = arg1        \n",
    "        \n",
    "    def strRepresentation():\n",
    "        \n",
    "        '''complete'''\n",
    "        \n",
    "class LogicalEquivalence:\n",
    "    \n",
    "\n",
    "    def __init__(self,arg1, arg2):\n",
    "        \n",
    "        self.arg1 = arg1\n",
    "        self.arg2 = arg2\n",
    "        \n",
    "    def strRepresentation():\n",
    "        \n",
    "\n",
    "class LogicalImplication:\n",
    "    \n",
    "    def __init__(self, arg1, arg2):\n",
    "        \n",
    "        self.arg1 = arg1\n",
    "        self.arg2 = arg2\n",
    "        \n",
    "        \n",
    "    def strRepresentation():\n",
    "        \n",
    "        '''complete'''\n",
    "        \n",
    "class LogicalEquivalence:\n",
    "    \n",
    "\n",
    "    def __init__(self,arg1, arg2):\n",
    "        \n",
    "        self.arg1 = arg1\n",
    "        self.arg2 = arg2\n",
    "        \n",
    "    def strRepresentation():\n",
    "        \n",
    "        '''complete'''\n",
    "        "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Exercise III. Conjunctive Normal Forms. \n",
    "\n",
    "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\n",
    "\n",
    "- $\\Leftrightarrow$ Elimination. replace $\\alpha \\Rightarrow \\beta $ with $(\\alpha\\Rightarrow \\beta )\\wedge (\\beta \\Rightarrow \\alpha)$\n",
    "- $\\Rightarrow$ Elimination. Replace $\\alpha \\Rightarrow \\beta $ with $\\not \\alpha \\vee \\beta$ \n",
    "- Distribbution of $\\lnot$: iteratively apply any of the following three steps\n",
    "\n",
    "    - $\\lnot(\\lnot \\alpha ) \\equiv \\alpha$ (double negation elimination)\n",
    "    - $\\lnot(\\alpha\\wedge \\beta) \\equiv (\\lnot \\alpha \\vee \\lnot \\beta) $ (De Morgan)\n",
    "    - $\\lnot(\\alpha \\vee \\beta) \\equiv (\\lnot \\alpha \\wedge \\lnot\\beta )$\n",
    "\n",
    "- Distribution of $\\vee$ over $\\wedge$. $(\\alpha\\vee (\\beta \\wedge \\gamma))\\equiv ((\\alpha \\vee \\beta)\\wedge(\\alpha \\vee \\gamma))$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "def to_Conjunctive_NormalForm(proposition):\n",
    "    \n",
    "    '''The function should return the CNF for the given proposition'''\n",
    "    \n",
    "    \n",
    "    return propositionCNF"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Exercise IV. Resolution rules\n",
    "\n",
    "Recall that the general resolution rule takes as premises two disjunctions and return a disjunction. I.e.\n",
    "\n",
    "$$\\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}$$\n",
    "\n",
    "\n",
    "#### Exercise IV.1. Resolution function\n",
    "\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.\n",
    "\n",
    "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}$\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "### \n",
    "\n",
    "def resolution(clause1, clause2):\n",
    "    \n",
    "    '''the function should return '''\n",
    "    \n",
    "    \n",
    "    \n",
    "    \n",
    "    return proposition\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Exercise IV.4. Resolution algorithm. \n",
    "\n",
    "Code the resolution algorithm below. recall that this algorithm iterates on the following steps:\n",
    "    \n",
    "<img src=\"PLresolution.png\">\n",
    "\n",
    "\n",
    "Start by trying the algorithm with simple KB such as single simple propositions. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "def resolutionAlgorithm(KB, proposition):\n",
    "    \n",
    "    '''The algorithm should return true if the sentence stored in Proposition is \n",
    "    entailed by the knowledge base KB'''\n",
    "    \n",
    "    \n",
    "    \n",
    "    \n",
    "    return conclusion"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Exercise IV.3. Propositional 2CNF\n",
    "\n",
    "A propositional 2-CNF expression is a conjunction of clauses, each containing _exactly_ two literals. As an example, consider the 2-CNF below:\n",
    "    \n",
    "$$(A\\vee B)\\wedge (\\lnot A\\vee C)\\wedge (\\lnot B\\vee D)\\wedge (\\lnot C\\vee G)\\wedge (\\lnot D\\vee G)$$\n",
    "\n",
    "Use your resolution algorithm to show that the knowledge base $KB$ represented by the single 2-CNF above entails the literal $G$."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Exercise V. Horn clauses and Forward chaining. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "A Horn clause is a disjunction of literals with at most one positive literal. As an example\n",
    "\n",
    "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$.\n",
    "\n",
    "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. \n",
    "\n",
    "<img src=\"PLresolutionHorn.png\">\n",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Code this algorithm below and test it on the KB give by\n",
    "\n",
    "- $P\\Rightarrow Q$\n",
    "- $L \\wedge M \\Rightarrow P$\n",
    "- $B\\wedge L \\Rightarrow M$\n",
    "- $A\\wedge P\\Rightarrow L$\n",
    "- $A\\wedge B\\Rightarrow L$\n",
    "- $A$\n",
    "- $B$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "def ForwardChainingPL(KB, proposition):\n",
    "    \n",
    "    '''the function should determine the value of the literal stored in proposition \n",
    "    from the set of Horn clauses stored in the knowledge base KB'''\n",
    "    \n",
    "    \n",
    "    \n",
    "    return conclusion"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 2",
   "language": "python",
   "name": "python2"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 2
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython2",
   "version": "2.7.13"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}