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

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.

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

Proof tree rules

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

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