Notes for my automated reasoning class. http://nbviewer.ipython.org/5376231

cs264a.ipynb

{
 "metadata": {
  "name": "cs264a"
 },
 "nbformat": 3,
 "nbformat_minor": 0,
 "worksheets": [
  {
   "cells": [
    {
     "cell_type": "heading",
     "level": 1,
     "metadata": {},
     "source": [
      "CS 264A - Automated Reasoning"
     ]
    },
    {
     "cell_type": "heading",
     "level": 2,
     "metadata": {},
     "source": [
      "Chapter 1 - Propositional Logic"
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Syntax"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "This class, in contrast to CS 262A, deals primarily with Boolean logic rather than partial beliefs (as encoded by probabilities).\n",
      "\n",
      "Propositional variables are sentences that are either true or false and are encapsulated in variables such as $\\alpha$ and $\\beta$.\n",
      "\n",
      "Logical connectives of sentences are also sentences.\n",
      "\n",
      "* Negation: $\\lnot$\n",
      "* Conjunction: $\\land$\n",
      "* Disjunction: $\\lor$\n",
      "\n",
      "Literals are single variables such as $\\alpha$ and $\\lnot \\alpha$.\n",
      "\n",
      "A knowledge base (KB) is a set of propositional sentences, $\\Delta = \\lbrace \\alpha_1, \\alpha_2, \\ldots \\rbrace$.\n",
      "\n",
      "Knowledge bases can be specified in one of three ways: just high output, all input and output, and all relations (see Boolean Functions)."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "World Semantics"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "A world $\\omega$ is a full instantiation of all variables $P_i$. With Boolean variables there are a total of $2^n$ worlds where $n$ is the number of variables.\n",
      "\n",
      "A sentence $\\alpha$ is true at a particular world $\\omega$, written as $\\omega \\models \\alpha$ if\n",
      "\n",
      "* $\\omega \\models P_i \\text{ iff } \\omega (P_i) = true$\n",
      "* $\\omega \\models \\lnot \\alpha \\text{ iff } \\omega \\not\\models \\alpha$\n",
      "* $\\omega \\models \\alpha \\lor \\beta \\text{ iff } \\omega \\models \\alpha \\text{ or } \\omega \\models \\beta$\n",
      "* $\\omega \\models \\alpha \\land \\beta \\text{ iff } \\omega \\models \\alpha \\text{ and } \\omega \\models \\beta$\n",
      "\n",
      "Determining the truth of a sentence at a particular world can be done in time linear in the size of the sentence.\n",
      "\n",
      "We say that sentence $\\alpha$ is *consistent/satisfiable* iff there is *at least one world* $\\omega$ at which $\\alpha$ is true, otherwise it is inconsistent/unsatisfiable.\n",
      "\n",
      "We say that sentence $\\alpha$ is *valid* iff it is true *at every world*."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Relationships"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "* Two sentences are *equivalent* iff they are true at the same set of worlds.\n",
      "* Two sentences are mutually eclusive iff they are never true at the same world.\n",
      "* Two sentences are exhaustive iff one of them is true at each world.\n",
      "* Sentence $\\alpha$ *implies* sentence $\\beta$ iff whenever $\\alpha$ is true at world $\\omega$, then $\\beta$ is also true at world $\\omega$. That is, if $\\omega \\models \\alpha$ then $\\omega \\models \\beta$ for all worlds $\\omega$."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Knowledge as Worlds"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The set of worlds that satisfy sentence $\\alpha$ are called the *models* of $\\alpha$ and are denoted by $Mods(\\alpha) = \\lbrace \\omega: \\omega \\models \\alpha \\rbrace$.\n",
      "\n",
      "* Sentence $\\alpha$ is satisfiable iff $Mods(\\alpha) \\neq \\emptyset$\n",
      "* Sentence $\\alpha$ is valid iff $Mods(\\alpha) = \\Omega$\n",
      "* Sentence $\\alpha$ is complete iff $Mods(\\alpha) = \\lbrace \\omega \\rbrace$\n",
      "* Sentence $\\alpha$ implies sentence $\\beta$ iff $Mods(\\alpha) \\subset Mods(\\beta)$\n",
      "* Sentence $\\alpha$ is equivalent to sentence $\\beta$ iff $Mods(\\alpha) = Mods(\\beta)$\n",
      "* Two sentences $\\alpha$ and $\\beta$ are mutually exclusive iff $Mods(\\alpha) \\cap Mods(\\beta) = \\emptyset$\n",
      "* Two sentences $\\alpha$ and $\\beta$ are exhaustive iff $Mods(\\alpha) \\cup Mods(\\beta) = \\Omega$\n",
      "\n",
      "We can think of a knowledge base as a set of worlds. Additional information in the knowledge base reduces the set of possible worlds. The knowledge base is complete if it specifies only one world. The knowledge base becomes inconsistent/unsatisfiable when $Mods(\\Delta) = \\emptyset$."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Relationships as Properties"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Logical relationships can be reduced to logical properties. For example, $\\alpha$ implies $\\beta$ can be tested by seeing whether $\\alpha \\land \\beta$ is satisfiable."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Refutation Theorem"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "$$ \\alpha \\text{ implies } \\beta, \\alpha \\models \\beta, \\text{ iff } \\alpha \\land \\lnot \\beta \\text{ is inconsistent}. $$\n",
      "\n",
      "It is the same thing as \"proof by contradiction.\"\n",
      "\n",
      "This means if we want to check if a sentence is consistent with a knowledge base we can add the negation to the knowledge base and check if it remains consistent. \\*"
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Quantified Propositional Logic"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "We can condition a knowledge base $\\Delta$ on a literal by replacing every occurence of that literal in $\\Delta$ by its truth value (*true* or *false*).\n",
      "\n",
      "Boole's expansion allows us to re-write $\\Delta$ as $( P \\land \\Delta \\mid P ) \\lor ( \\lnot P \\land \\Delta \\mid \\lnot P )$. Recursive application will decompose a knowledge base down to trivial knowledge bases that are equivalent to either *true* or *false*.\n",
      "\n",
      "Existential quantification can eliminate a variable $P$ from a knowledge base $\\Delta$ if $P$ is unknown:\n",
      "\n",
      "$$ \\exists P \\Delta = \\Delta \\mid P \\lor \\Delta \\mid \\lnot P $$\n",
      "\n",
      "Existential quantification can be though of as a projection that returns the *strongest sentence* implied by $\\Delta$ without $P$.\n",
      "\n",
      "Universal quantification also removes $P$ from a knowledge base $\\Delta$ but can be thought of as returning the *weakest sentence* implied by $\\Delta$ without $P$:\n",
      "\n",
      "$$ \\forall P \\Delta = \\Delta \\mid P \\land \\Delta \\mid \\lnot P $$\n",
      "\n",
      "These two quantifications are related as below:\n",
      "\n",
      "* $ \\exists P \\Delta = \\lnot ( \\forall P \\lnot \\Delta ) $\n",
      "* $ \\forall P \\Delta = \\lnot ( \\exists P \\lnot \\Delta ) $\n",
      "\n",
      "You can quantify over multiple variables and the order does not matter.\n",
      "\n",
      "Conditioning, existential quantification, and universal quantification are transformations on a knowledge base. They can also be represented in world satisfaction semantics (see page 15)."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Queries and Transformations on Knowledge Bases"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Where $\\Delta$ and $\\Gamma$ are knowledge bases:\n",
      "\n",
      "Queries:\n",
      "\n",
      "* **CO**: Testing whether a $\\Delta$ is satisfiable.\n",
      "* **VA**: Testing whether a $\\Delta$ is valid.\n",
      "* **CT**: Counting the models of $\\Delta$.\n",
      "* **EN**: Enumerating the models of $\\Delta$.\n",
      "* **IP**: Testing whether $\\Delta$ implies a disjunction of literals (clause) $\\alpha$.\n",
      "* **PI**: Testing whether a conjunction of literations (term) $\\beta$ implies $\\Delta$.\n",
      "* **IM**: Testing whether $\\Delta$ implies $\\Gamma$.\n",
      "* **EQ**: Testing whether $\\Delta$ is equivalent to $\\Gamma$.\n",
      "\n",
      "Transformations:\n",
      "\n",
      "* **NEG**: Negating $\\Delta$.\n",
      "* **CON**: Conjoining $\\Delta$ and $\\Gamma$.\n",
      "* **DIS**: Disjoining $\\Delta$ and $\\Gamma$.\n",
      "* **CND**: Conditioning $\\Delta$ on a literal.\n",
      "* **EQT**: Existentially quantifying variable $P$ out of $\\Delta$.\n",
      "* **FQT**: Universally quantifying variable $P$ out of $\\Delta$.\n",
      "\n",
      "The difficulty of some of these queries or transformations is dependent on the form the knowledge base takes (e.g. CNF, DNF, etc.)."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Boolean Functions"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "A *Boolean function* $f$ over Boolean variables $X_1, \\ldots, X_n$ is a function that maps each value of these variables into a 1 or 0. We can then represent logic circuits as Boolean functions.\n",
      "\n",
      "A *Type III* Boolean function is a function over the circuit inputs.\n",
      "\n",
      "A *Type II* Boolean function is a function over the circuit inputs and outputs.\n",
      "\n",
      "A *Type I* Boolean function is functoin over the circuit inputs, outputs, and all internal wires."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Discrete Variables"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Propositional logic can be extended to discrete variables because the world semantics are general."
     ]
    },
    {
     "cell_type": "heading",
     "level": 2,
     "metadata": {},
     "source": [
      "Chapter 2 - Propositional Resolution"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Resolution is an inference rule allowing us to derive sentences that are logically implied by a knowledge base.\n",
      "\n",
      "The most general form of propositional resolution,\n",
      "\n",
      "$$ \\alpha \\lor \\beta \\text{ and } \\lnot \\beta \\lor \\gamma \\implies \\alpha \\lor \\gamma $$\n",
      "\n",
      "Resolution is *sound*,\n",
      "\n",
      "$$ \\Delta \\cup \\lbrace \\alpha \\lor \\beta \\text{ and } \\lnot \\beta \\lor \\gamma \\rbrace \\models \\alpha \\lor \\gamma $$\n",
      "\n",
      "Resolution is *not complete* meaning if you close a knowledge base under resolution there may be additional sentences implied by the knowledge base that are not found.\n",
      "\n",
      "Resolution can be used to prove that $\\Delta$ implies some sentence $\\alpha$.\n",
      "\n",
      "Resolution can be used to simplify $\\Delta$ by uncovering all unit clauses implied by $\\Delta$.\n",
      "\n",
      "Resolution can be used to existentially quantify variables in $\\Delta$ and maintain clausal form.\n",
      "\n",
      "Resolution can be represented as a directed acyclic graph (DAG) known as a *resolution graph*. Resolution graphs are useful in describing resolution strategies."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Clausal Form"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "A clause is a disjunction of literals (e.g. $(A \\lor B \\lor \\lnot C)$).\n",
      "\n",
      "A propositional sentence is in conjunctive normal form (CNF) if it is a sequence of conjunctions of clauses (e.g. $\\alpha_1 \\land \\alpha_2 \\land \\alpha_3$).\n",
      "\n",
      "A clause with no literals, the *empty clause*, corresponds to an inconsistent sentence (i.e. $\\emptyset \\in \\Delta$). However, a CNF with no clauses is a valid sentence (i.e. $\\Delta = \\emptyset$).\n",
      "\n",
      "A clause can be represented by a set of literals and a CNF can be represented as a set of clauses which we call *causal form*:\n",
      "\n",
      "$$ \\lbrace \\lbrace A, B, \\lnot C \\rbrace, \\lbrace \\lnot A, D \\rbrace, \\lbrace B, C, D \\rbrace \\rbrace $$\n",
      "\n",
      "We say that a clausal form is closed under resolution if any clause that can be derived from the form using resolution is already in clausal form."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Converting Sentences into Clausal Form"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "1. Remove all logical connectives except for conjunction, disjunction, and negation.\n",
      "  * e.g. $\\alpha \\implies \\beta$ to $\\lnot \\alpha \\lor \\beta$.\n",
      "2. Push negations inside the sentence until they only appear next to propositional variables.\n",
      "  * $\\lnot \\lnot \\alpha$ is transformed into $\\alpha$.\n",
      "  * $\\lnot(\\alpha \\lor \\beta)$ is transformed into $\\lnot \\alpha \\land \\lnot \\beta$.\n",
      "  * $\\lnot(\\alpha \\land \\beta)$ is transformed into $\\lnot \\alpha \\lor \\lnot \\beta$.\n",
      "3. Distribute disjunctions over conjunctions.\n",
      "  * e.g. $\\alpha \\lor ( \\beta \\land \\gamma)$ is transformed to $(\\alpha \\lor \\beta) \\land (\\alpha \\lor \\gamma)$).\n",
      "4. Now that we're in conjunctive normal form we convert to clausal form by removing the logical connectives and using set notation instead.\n",
      "\n",
      "Note that the result may \"blow up\" resulting in a large sentence."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Conditioning with Clausal Form"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "$$ \\Delta \\mid P = \\lbrace \\alpha \\setminus \\lbrace \\lnot P \\rbrace \\mid \\alpha \\in \\Delta, P \\not\\in \\alpha \\rbrace $$\n",
      "\n",
      "1. Remove clauses that contain positive literal $P$.\n",
      "2. Keep clauses that contain negative literal $\\lnot P$ but remove the $\\lnot P$ from each.\n",
      "3. Otherwise keep a clause unchanged.\n",
      "\n",
      "For example, given $\\Delta = \\lbrace \\lbrace A, B, \\lnot C \\rbrace, \\lbrace \\lnot A, D \\rbrace, \\lbrace B, C, D \\rbrace \\rbrace$,\n",
      "\n",
      "$$ \\Delta \\mid C = \\lbrace \\lbrace A, B \\rbrace, \\lbrace \\lnot A, D \\rbrace \\rbrace $$\n",
      "\n",
      "$$ \\Delta \\mid CA = \\lbrace \\lbrace D \\rbrace \\rbrace $$\n",
      "\n",
      "$$ \\Delta \\mid CA \\lnot D = \\lbrace \\lbrace \\rbrace \\rbrace = \\lbrace \\emptyset \\rbrace $$\n",
      "\n",
      "$$ \\Delta \\mid CAD = \\lbrace \\rbrace = \\emptyset $$\n",
      "\n",
      "Note that $\\Delta \\mid CA \\lnot D$ is inconsistent but $\\Delta \\mid CAD$ is valid."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Connectivity Graph"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Undirected graph over variables in $\\Delta$ that contains an edge between two variables if they appear in the same clause in $\\Delta$.\n",
      "\n",
      "Provides bounds on resolution because resolving two clauses results in a clause that *cannot* contain variables that are *not* neighbors of the variable resolved."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Deduction Using Resolution"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Since resolution is not *complete* we cannot check if $\\Delta$ implies $\\alpha$ by closing under resolution and looking for $\\alpha$. However, resolution is *refutation complete* on clausal forms so if a clausal form is inconsistent then resolution is capable of deriving the empty clause.\n",
      "\n",
      "Using this we can prove $\\Delta \\models \\alpha$ by showing $\\Delta \\land \\lnot \\alpha$ is inconsistent. We can do this by adding $\\lnot \\alpha$ to $\\Delta$ and performing resolution until we derive the empty clause. If we *do not* derive an empty clause then $\\Delta \\not\\models \\alpha$. If we *do* derive the empty clause then $\\Delta \\models \\alpha$.\n",
      "\n",
      "We can also resolve the knowledge base and the query independently and then combine the results and perform further resolution to complete the query."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Resolution Strategies"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Applying resolution can be computationally costly. A *resolution strategy* is a restriction on which clauses can participate in a resolution step. However, care must be taken to ensure that a resolution strategy remains refutation complete."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Linear Resolution"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Only resolves two clauses if one is a root clause or an ancestor of the other clause.\n",
      "\n",
      "Linear resolution constructs chains in the resolution graph.\n",
      "\n",
      "Linear resolution is refutation complete."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Set-of-Support Resolution"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Requires that at least one of the resolved clauses must be in or a descendent of some clause in the set of support. When checking $\\Delta \\land \\lnot \\alpha$ it is gauranteed that $\\lnot \\alpha$ will be a set of support.\n",
      "\n",
      "Set-of-support is refutation complete.\n",
      "\n",
      "I'm not sure if I'm really understanding this one."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Unit Resolution"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "A *unit clause* is a clause that contains a single literal.\n",
      "\n",
      "Unit resolution requires that at least one of the resolved clauses is a unit clause.\n",
      "\n",
      "Unit resolution *is not* refutation complete except for Horn clausal form.\n",
      "\n",
      "Unit resolution is very efficient.\n",
      "\n",
      "Unit resolution can be thought of as simplification."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Horn Clausal Form"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "A *Horn clause* is one that contains at most one positive literal (e.g. $\\lbrace \\lnot A, \\lnot B, C \\rbrace$).\n",
      "\n",
      "Resolving two Horn clauses results in a horn clause (i.e. closed under resolution).\n",
      "\n",
      "*Horn clausal form* contains only Horn clauses.\n",
      "\n",
      "All unit resolutions can be exhausted in linear time so consistency checks can be performed in linear time."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Directed Resolution"
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Forgetting"
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Model Enumeration and Counting"
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Complexity Analysis"
     ]
    }
   ],
   "metadata": {}
  }
 ]
}