{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": false
   },
   "source": [
    " <h1>An Introduction to Logic using Sage</h1>\n",
    "<b><a href=\"http://faculty.uml.edu/klevasseur/ads2/\">Applied Discrete Structures</a></b> by Alan Doerr & Kenneth Levasseur is licensed under a Creative Commons Attribution - Noncommercial -  No Derivative Works 3.0 United States License.</p>\n",
    "<p>Here are a few tips on how to get started using Sage to work logic.  We look at possible answers to #2 in Section 3.3 of Applied Discrete Structures.</p>\n",
    "<p>\n",
    "    Here are the symbols used in Sage.\n",
    "</p>\n",
    "<table>\n",
    "    <tr><td>and</td><td> ....</td><td>&</td></tr>\n",
    "    <tr><td>or</td><td> ....</td><td>|</td></tr>\n",
    "    <tr><td>not</td><td> ....</td><td>~</td></tr>\n",
    "</table>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 63,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(p&~q)|(r&p)"
      ]
     },
     "execution_count": 63,
     "metadata": {
     },
     "output_type": "execute_result"
    }
   ],
   "source": [
    "import sage.logic.propcalc as propcalc\n",
    "prop=propcalc.formula\n",
    "x = prop(\"(p&~q)|(r&p)\")\n",
    "x"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "p      q      r      value\n",
       "False  False  False  False  \n",
       "False  False  True   False  \n",
       "False  True   False  False  \n",
       "False  True   True   False  \n",
       "True   False  False  True   \n",
       "True   False  True   True   \n",
       "True   True   False  False  \n",
       "True   True   True   True   \n"
      ]
     },
     "execution_count": 33,
     "metadata": {
     },
     "output_type": "execute_result"
    }
   ],
   "source": [
    "x.truthtable()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": false
   },
   "source": [
    "<p>Something that is equivalent to x?</p>\n",
    "<p>\n",
    "    It's a cop-out but you could answer x here.  ... and the same for the other two parts.\n",
    "</p>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "p      q      r      value\n",
       "False  False  False  True   \n",
       "False  False  True   True   \n",
       "False  True   False  True   \n",
       "False  True   True   True   \n",
       "True   False  False  True   \n",
       "True   False  True   True   \n",
       "True   True   False  True   \n",
       "True   True   True   True   \n"
      ]
     },
     "execution_count": 21,
     "metadata": {
     },
     "output_type": "execute_result"
    }
   ],
   "source": [
    "x.iff(x).truthtable()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": false
   },
   "source": [
    "<p>\n",
    "    Here is one that is a bit more <q>interesting</q>.\n",
    "</p>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 64,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(p&~q&~r)|(p&~q&r)|(p&q&r)"
      ]
     },
     "execution_count": 64,
     "metadata": {
     },
     "output_type": "execute_result"
    }
   ],
   "source": [
    "w=prop(\"(p&~q&~r)|(p&~q&r)|(p&q&r)\")\n",
    "w"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "p      q      r      value\n",
       "False  False  False  True   \n",
       "False  False  True   True   \n",
       "False  True   False  True   \n",
       "False  True   True   True   \n",
       "True   False  False  True   \n",
       "True   False  True   True   \n",
       "True   True   False  True   \n",
       "True   True   True   True   \n"
      ]
     },
     "execution_count": 36,
     "metadata": {
     },
     "output_type": "execute_result"
    }
   ],
   "source": [
    "x.iff(w).truthtable()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 37,
     "metadata": {
     },
     "output_type": "execute_result"
    }
   ],
   "source": [
    "x.equivalent(w)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": false
   },
   "source": [
    "<p>Something that implies x?</p><p>\n",
    "    Here you need a proposition that has the property that when it is true, <m>x</m> is also true.  Looking at the truth table, one proposition that works is \"p and q and r.\"  Let's test it.\n",
    "</p>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
   ],
   "source": [
    "y=prop(\"p&q&r\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 39,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "p      q      r      value\n",
       "False  False  False  True   \n",
       "False  False  True   True   \n",
       "False  True   False  True   \n",
       "False  True   True   True   \n",
       "True   False  False  True   \n",
       "True   False  True   True   \n",
       "True   True   False  True   \n",
       "True   True   True   True   \n"
      ]
     },
     "execution_count": 39,
     "metadata": {
     },
     "output_type": "execute_result"
    }
   ],
   "source": [
    "y.ifthen(x).truthtable()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 40,
     "metadata": {
     },
     "output_type": "execute_result"
    }
   ],
   "source": [
    "y.implies(x)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": false
   },
   "source": [
    "Something that is implied by x?\n",
    "<p>\n",
    "    There are lots of pos\n",
    "    sible answers here, as there was in the previous part. One is to notice that whenever p is true in the truth table, x is also true.\n",
    "</p>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 65,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
   ],
   "source": [
    "p=prop(\"p\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 66,
   "metadata": {
    "collapsed": false,
    "scrolled": true
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 66,
     "metadata": {
     },
     "output_type": "execute_result"
    }
   ],
   "source": [
    "x.implies(p)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": false
   },
   "source": [
    "\n",
    "Here is an algorithmic solution to exercise 10 at the end of Section 3.7, on Mathematical Induction. The problem was to prove that all postage amounts greater than or equal to 8 can be made using 3 and 5 cent stamps. Notice that the solution for any value of <m>n</m> greater than 8 relies on the solution of the previous value, <m>n-1</m>, in the same way as we can verify by induction that if the case of <m>n-1</m> can be solved, then we can use it to solve the case of <m>n</m>."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 0,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
   ],
   "source": [
    "def ThreeFive(n):\n",
    "    if n==8:\n",
    "        return [1,1]\n",
    "    previous=ThreeFive(n-1)\n",
    "    if previous[1]>0:\n",
    "        return [previous[0]+2,previous[1]-1]\n",
    "    else:\n",
    "        return [previous[0]-3,previous[1]+2]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 0,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
   ],
   "source": [
    "ThreeFive(56)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": false
   },
   "source": [
    "<p>\n",
    "    Thanks to Richard Voss for the following code that produces a truth table that is more compatible with the text.\n",
    "</p>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 44,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
   ],
   "source": [
    "def TruthTable(formula):\n",
    "    txt = str(propcalc.formula(formula).truthtable()).replace(\"value\",formula)\n",
    "    return txt.replace(\"False\",\"0\").replace(\"True \",\"1\").replace(\"     \",\" \")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "p  q  ((p | ~q)& ~p) ->~q\n",
      "0  0  1  \n",
      "0  1  1  \n",
      "1  0  1  \n",
      "1  1  1  \n",
      "\n"
     ]
    }
   ],
   "source": [
    "print TruthTable('((p | ~q)& ~p) ->~q')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": false
   },
   "source": [
    "<h3>\n",
    "    Testing the validity of a logical argument.\n",
    "</h3>\n",
    "<p>\n",
    "    Consider the argument \\[a \\lor b, c\\land d,a\\rightarrow \\neg c  \\Rightarrow b\\]\n",
    "</p>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 69,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
   ],
   "source": [
    "p1=prop(\"a|b\")\n",
    "p2=prop(\"c&d\")\n",
    "p3=prop(\"a->~c\")\n",
    "concl=prop(\"b\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 70,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 70,
     "metadata": {
     },
     "output_type": "execute_result"
    }
   ],
   "source": [
    "propcalc.valid_consequence(concl,p1,p2,p3)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 71,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "execution_count": 71,
     "metadata": {
     },
     "output_type": "execute_result"
    }
   ],
   "source": [
    "propcalc.valid_consequence(prop(\"~b\"),p1,p2,p3)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 73,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
   ],
   "source": [
    "c,r1,r2=propcalc.get_formulas(\"b\", \"c->b\", \"c\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 74,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 74,
     "metadata": {
     },
     "output_type": "execute_result"
    }
   ],
   "source": [
    "propcalc.valid_consequence(c,r1,r2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 75,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "execution_count": 75,
     "metadata": {
     },
     "output_type": "execute_result"
    }
   ],
   "source": [
    "propcalc.valid_consequence(p2,p1,c)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 76,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
   ],
   "source": [
    "q1,q2,q3,q4=propcalc.get_formulas(\"c->b\", \"c->a\", \"a->~b\",\"c\")\n",
    "cx=prop(\"a&b\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 77,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 77,
     "metadata": {
     },
     "output_type": "execute_result"
    }
   ],
   "source": [
    "propcalc.valid_consequence(cx,q1,q2,q3,q4)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 78,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 78,
     "metadata": {
     },
     "output_type": "execute_result"
    }
   ],
   "source": [
    "propcalc.valid_consequence(~cx,q1,q2,q3,q4)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 79,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "execution_count": 79,
     "metadata": {
     },
     "output_type": "execute_result"
    }
   ],
   "source": [
    "propcalc.consistent(q1,q2,q3,q4)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 0,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
   ],
   "source": [
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "SageMath (stable)",
   "language": "sagemath",
   "metadata": {
    "cocalc": {
     "description": "Open-source mathematical software system",
     "priority": 10,
     "url": "https://www.sagemath.org/"
    }
   },
   "name": "sagemath"
  },
  "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.15"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 0
}