My Weblog

Blog about programming and math

Propositional Logic course ( Coursera )

Recently I took a logic course on Coursera. Although I am bit familiar with logic but this course was great. I got more clear grasp on Proposition logic, Proof tree, bit of Prolog and came to know about Quine–McCluskey algorithm ( in my TODO list of implementation ) while learning about circuit minimisation. In one of the assignments, we have to tell if the given formula is tautology, contradiction or contingent so I wrote some quick Haskell code to solve the assignment

import Text.Parsec.Prim
import Text.Parsec.Expr
import Text.Parsec.Char
import Text.Parsec.String ( Parser )
import Control.Applicative hiding ( ( <|> ) , many )
import qualified Data.Map as M
import Data.Maybe
import Data.List
import Control.Monad

data LExpr = Lit Char
           | Not LExpr       
           | And LExpr LExpr
           | Or LExpr LExpr
           | Imp LExpr LExpr  -- ( P =>  Q )
           | Red LExpr LExpr  -- ( P <=  Q )
           | Eqi LExpr LExpr  -- ( P <=> Q ) 
           deriving Show

exprCal :: Parser LExpr
exprCal = buildExpressionParser table atom 

table = [  [  Prefix ( Not <$ string  "~"  ) ]
         , [  Infix  ( And <$ string  "&"  ) AssocLeft ]
         , [  Infix  ( Or  <$ string  "|"  ) AssocLeft ]
         , [  Infix  ( Eqi <$ try ( string "<=>" ) ) AssocLeft 
            , Infix  ( Imp <$  string "=>"         ) AssocLeft 
            , Infix  ( Red <$  string "<="         ) AssocLeft 
           ]
        ]

atom :: Parser LExpr
atom =  char '(' *>  exprCal   <* char ')' 
     <|> ( Lit <$> letter )

assignment :: LExpr -> [ M.Map Char Bool ]
assignment expr = map ( M.fromList . zip vs ) ps where
    vs = variables expr
    ps = replicateM ( length vs ) [ True, False]
 

variables :: LExpr -> [ Char ]
variables expr = map head . group . sort . vars expr $ []  where
    vars ( Lit c )    xs = c : xs
    vars ( Not expr ) xs = vars expr xs
    vars ( And exprf exprs ) xs = vars exprf xs ++ vars exprs xs
    vars ( Or  exprf exprs ) xs = vars exprf xs ++ vars exprs xs
    vars ( Imp exprf exprs ) xs = vars exprf xs ++ vars exprs xs
    vars ( Red exprf exprs ) xs = vars exprf xs ++ vars exprs xs
    vars ( Eqi exprf exprs ) xs = vars exprf xs ++ vars exprs xs


expEval :: LExpr -> M.Map Char  Bool -> Bool
expEval ( Lit v   )         mp =  fromMaybe False ( M.lookup v mp )
expEval ( Not expr  )       mp =  not . expEval  expr $ mp
expEval ( And exprf exprs ) mp =  expEval exprf mp && expEval  exprs mp
expEval ( Or  exprf exprs ) mp =  expEval exprf mp || expEval  exprs mp
expEval ( Imp exprf exprs ) mp =  (  not . expEval  exprf $ mp  ) || expEval exprs mp 
expEval ( Red exprf exprs ) mp =  expEval ( Imp exprs exprf  ) mp 
expEval ( Eqi exprf exprs ) mp =  expEval exprf mp == expEval exprs mp

values :: LExpr -> [ Bool ]
values expr = map ( expEval expr ) ( assignment expr ) 

isTautology :: LExpr -> Bool
isTautology = and . values

isContradiction :: LExpr -> Bool
isContradiction  = not . or . values

isContingent :: LExpr -> Bool
isContingent expr = not ( isTautology expr || isContradiction expr )
  
calculator :: String -> LExpr
calculator expr = case parse  exprCal ""  expr of
                       Left msg -> error "failed to parse"
                       Right val -> val

Mukeshs-MacBook-Pro:Compilers mukeshtiwari$ ghci LogicPraser.hs 
GHCi, version 7.8.1: http://www.haskell.org/ghc/  😕 for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Main             ( LogicPraser.hs, interpreted )
Ok, modules loaded: Main.
*Main> calculator "p=>q|q=>p"
Loading package transformers-0.3.0.0 ... linking ... done.
Loading package array-0.5.0.0 ... linking ... done.
Loading package deepseq-1.3.0.2 ... linking ... done.
Loading package containers-0.5.5.1 ... linking ... done.
Loading package bytestring-0.10.4.0 ... linking ... done.
Loading package mtl-2.1.3.1 ... linking ... done.
Loading package text-1.1.1.1 ... linking ... done.
Loading package parsec-3.1.5 ... linking ... done.
Imp (Imp (Lit 'p') (Or (Lit 'q') (Lit 'q'))) (Lit 'p')
*Main> calculator "(p=>q)|(q=>p)"
Or (Imp (Lit 'p') (Lit 'q')) (Imp (Lit 'q') (Lit 'p'))
*Main> isTautology ( Or (Imp (Lit 'p') (Lit 'q')) (Imp (Lit 'q') (Lit 'p')) )
True
*Main> calculator "(p=>q)&(q=>p)"
And (Imp (Lit 'p') (Lit 'q')) (Imp (Lit 'q') (Lit 'p'))
*Main> isTautology ( And (Imp (Lit 'p') (Lit 'q')) (Imp (Lit 'q') (Lit 'p')) )
False
*Main> isCont ( And (Imp (Lit 'p') (Lit 'q')) (Imp (Lit 'q') (Lit 'p')) )
isContingent     isContradiction
*Main> isContingent  ( And (Imp (Lit 'p') (Lit 'q')) (Imp (Lit 'q') (Lit 'p')) )
True
*Main> isCont  ( And (Imp (Lit 'p') (Lit 'q')) (Imp (Lit 'q') (Lit 'p')) )
isContingent     isContradiction
*Main> isContradiction   ( And (Imp (Lit 'p') (Lit 'q')) (Imp (Lit 'q') (Lit 'p')) )
False

Proof tree for propositional logic was something which I learned from this course. Why proof tree method is great ? We will take a example to understand it more clearly.

p \Rightarrow ( q \vee r ) \newline  s \Rightarrow ( \neg r) \newline  \line(1,0){70}\newline  ( p\wedge s ) \Rightarrow q

A set of premises Δ logically entails a conclusion ϕ (written as Δ |= ϕ) if and only if every interpretation that satisfies the premises also satisfies the conclusion. Logical formulas above the line are premises and below is conclusion.

p \hspace{5 mm} q \hspace{5 mm}  r \hspace{5 mm}  s \hspace{5 mm} p \Rightarrow ( q \vee r ) \hspace{5 mm}            s \Rightarrow ( \neg r) \hspace{5 mm}( p\wedge s ) \Rightarrow q

\begin{tabular}{ | l | l | l | l | p{2cm} | p{2cm} | p{2cm} | }     \hline      0 & 0 & 0 & 0 & 1 & 1 & 1  \\    0 & 0 & 0 & 1 & 1 & 1 & 1  \\    0 & 0 & 1 & 0 & 1 & 1 & 1  \\    0 & 0 & 1 & 1 & 1 & 0 & 1  \\    0 & 1 & 0 & 0 & 1 & 1 & 1  \\    0 & 1 & 0 & 1 & 1 & 1 & 1  \\    0 & 1 & 1 & 0 & 1 & 1 & 1  \\    0 & 1 & 1 & 1 & 1 & 0 & 1  \\    1 & 0 & 0 & 0 & 0 & 1 & 1  \\    1 & 0 & 0 & 1 & 0 & 1 & 0  \\    1 & 0 & 1 & 0 & 1 & 1 & 1  \\    1 & 0 & 1 & 1 & 1 & 0 & 0  \\    1 & 1 & 0 & 0 & 1 & 1 & 1  \\    1 & 1 & 0 & 1 & 1 & 1 & 1  \\    1 & 1 & 1 & 0 & 1 & 1 & 1  \\    1 & 1 & 1 & 1 & 1 & 0 & 1  \\       \hline      \end{tabular}

We can see from the truth table that all the interpretation which satisfy premises also satisfy conclusion. Looks great but lengthy.
Proof tree rules

A \wedge B  \hspace*{10mm} A \vee B \hspace*{10mm} A \Rightarrow B\hspace*{10mm} A \equiv  B \hspace*{10mm} A \newline   \hspace*{5mm}| \hspace*{15mm} / \hspace*{8mm}  \backslash \hspace*{10mm} / \hspace*{8mm}\backslash \hspace*{10mm} / \hspace*{8mm} \backslash \hspace*{7mm} \neg A\newline  \hspace*{4mm} A \hspace*{13mm} A \hspace*{8mm} B \hspace*{5mm} \neg A \hspace*{8mm}B \hspace*{6mm} A \hspace*{10mm} \neg A \hspace*{5mm} \times \newline  \hspace*{4mm} B  \hspace*{55mm} B\hspace*{10mm} \neg B\newline

\neg ( A \wedge B ) \hspace*{5mm} \neg ( A \vee B) \hspace*{5mm} \neg ( A \Rightarrow B) \hspace*{5mm} \neg ( A \equiv B) \hspace*{5mm} \neg \neg A \newline  \hspace*{4mm} / \hspace*{8mm} \backslash \hspace*{15mm} | \hspace*{23mm} | \hspace*{15mm} /\hspace*{8mm} \backslash \hspace*{15mm} | \newline  \hspace*{2mm} \neg A \hspace*{6mm} \neg B \hspace*{8mm} \neg A \hspace*{20mm} A \hspace*{13mm} A\hspace*{8mm} \neg A \hspace*{10mm} A \newline  \hspace*{28mm} \neg B \hspace*{18mm} \neg B \hspace*{11mm} \neg B\hspace*{8mm} B  \newline

Theorem: Δ |= ϕ if and only if Δ ∪ {¬ϕ} is unsatisfiable. Following the theorem, our problem translates into proving that

p \Rightarrow ( q \vee r ) \newline  s \Rightarrow ( \neg r) \newline  \neg ( ( p\wedge s ) \Rightarrow q )

is unsatisfiable. We can see that tree is closed and there is no interpretation which makes it satisfiable. Chose any branch and start moving up the tree and if it contains both A and ~A then we close the branch because it’s not possible to make A and ~A true simultaneously. You can see the course notes.
Screen Shot 2014-05-03 at 2.06.54 am.
See Propositional logic library from hackage. Source code on github

Advertisements

May 2, 2014 Posted by | Haskell, Programming | , , , , | Leave a comment