# My Weblog

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

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  = 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
[1 of 1] Compiling Main             ( LogicPraser.hs, interpreted )
*Main> calculator "p=>q|q=>p"
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')) )
*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')) )
*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.
.
See Propositional logic library from hackage. Source code on github