{-
File:     Cnf.hs
Desc:     Transformer functions for InfixLgoic for conjunctive normal form
Author:   Dan Mead
Date:     Fall 2006
Liscence: GPLv2 


Overview:
         This module contains functions for representing
      first order logic. It also provides the nessicary
      functions for use with the resolution theorem prover
      in prover.hs. Also included here is a set of rules for
      parsec that allows logic expression to be constructed 
      from strings.

 TODO: still need code for skolemization, unification
       and predicates
      
-}
module Cnf where

import InfixLogic

{-
Function: makeNegation
-}
makeNeg(F) = T
makeNeg(T) = F
makeNeg(a) = Neg a


{-
Function: makeDisjunction
-}

makeDisj (a, F) = a
makeDisj (F, b) = b
makeDisj (T, b) = T
makeDisj (a, T) = T
makeDisj (a , b) = if a == b then a
                   else if a `negationOf` b then T
                   else a :\/ b

{-
Function: makeConj
-}

makeConj(a,F) = F
makeConj(F,b) = F
makeConj(a,T) = a
makeConj(T,b) = b
makeConj(a,b) = if a == b then a
                else if a `negationOf` b then F
                else  a :& b

{-
Function: ra (remove arrows)
Desc:     removes implications and bioconditionals from 
         a logic expression

Examples
         ra(a <-> b) = (a & b) v (~a & ~b)
         ra( a -> b) = ~a v b

-}


removeArrows (Neg a)  	   = makeNeg (removeArrows a)
removeArrows (a :& b)      = makeConj(removeArrows a, removeArrows b)
removeArrows (a :\/ b)     = makeDisj(removeArrows a , removeArrows b)
removeArrows (a :-> b)     = makeDisj(makeNeg (removeArrows a), removeArrows b)
removeArrows (a :<-> b)    = makeDisj(makeConj(removeArrows a,removeArrows b), 
                                      makeConj(makeNeg (removeArrows a), makeNeg(removeArrows b)))
removeArrows  e = e


{-
Function: removeNegation
Desc:     Use de Morgans laws to distribute negations onto disjunctions and conjunctions
        so that each negation operator applies to the smallest scope possible

Examples:
        ~(PvQ) = (~P&~Q)
        ~(P&Q) = (~Pv~Q)
        ~~P    = P
-}

removeNegation (Neg (Neg a))   = removeNegation a
removeNegation (a :&  b)       = makeConj(removeNegation a,removeNegation b)
removeNegation (a :\/ b)       = makeDisj(removeNegation a, removeNegation b)
removeNegation (Neg (a :\/ b)) = makeConj(removeNegation (makeNeg a),removeNegation (makeNeg b))
removeNegation (Neg (a :&  b)) = makeDisj(removeNegation (makeNeg a), removeNegation (makeNeg b))
removeNegation e = e


{-
Function: dd (distribute disjuncts)
Desc:     Apply the distribution rule over a conjunct

Examples:
           Pv(Q&R) = (PvQ)&(PvR)
           (Q&R)vP = (QvP)&(RvP)
-}





dd (a :\/ (b :& c))  | (a == b)  = dd(a)
                     | (a == c)  = dd(a)
                     | otherwise =dd( makeConj( dd(makeDisj(a,b)) , dd(makeDisj(a, c)) ))

dd ((a :& b) :\/ c) |(c == b)    = dd(c)
                    |(c == a)    = dd(c)
                    |otherwise   =dd( makeConj( dd(makeDisj(c,a)) , dd(makeDisj(c, b))))

dd (a :&  b)          = (makeConj(dd(a),dd(b)))
dd (a :\/ b)          = (makeDisj(dd(a), dd(b)))
dd e = e



{-
Function: simp
Desc:     Simplifies a logic expression so that:

           PvP     = P
           PvT     = T
           P&F     = F
           P&~P    = F



simp (Neg (Neg a)) = simp a


simp ((a :\/ b) :& (c :\/ d)) | (a `negationOf` b) = simp(makeConj(c,d))
                              | (c `negationOf` d) = simp(makeConj(a,b))
                              | otherwise          = makeConj(simp (makeDisj(a,b)), simp (makeDisj(c,d)))
 
simp (a :\/ b)                = makeDisj(simp(a), simp(b))

simp (a :& b)                = makeConj((simp a),(simp b))

simp x = x

-}

{-
Function: cnf (conjunctive normal form)
Desc:     Converts a given expression (as a string)
          to a corresponding Expresison object in cnf form

Examples
          cnf "~(PvQ)" evaluates to P :& Q

-}

cnf(a) = (dd(removeNegation(removeArrows(a))))


{-
Function: makedb
Desc      Constructs a list of conjuncts from an Expression
          in conjunctive normal form

Examples:
           P&Q         = [P,Q]
          (PvR)&(~PvS) = [PvR,~PvS]
-}


makedb (a :& b) = makedb a ++ makedb b
makedb e = [e]



{-
Function: disjtolist
Desc:     Transforms a disjunction of any length to a list
          of propositions

Examples:
          PvQv~R   becomes   [P,Q,~R]   
-}

disjTolist :: Expression -> [Expression]
disjTolist (a :\/ b) = disjTolist(a) ++ disjTolist(b)
disjTolist e = [e]


{-
Function: listTodisj
Desc:     Transforms a list of propositions to a dijunct

Examples: 
          [P,Q,~R] becomes PvQv~R 
-}

listTodisj :: [Expression] -> Expression
listTodisj [] = Nil
listTodisj (a:[]) = a
listTodisj (x:xs) = x :\/ (listTodisj(xs))



--test data. all of these are tautologies
--all run with the prover unless otherwise commented
s1 = "Pv~P"
s2 = "~(P&~P)"
s3 = "P->P"

--idempotent laws 
s4a = "P<->(PvP)"
s4b = "P<->(P&P)"

--double negation 
s5 = "~(~P)<->P" 

--commutative laws
s6a = "(PvQ)<->(QvP)"
s6b = "(P&Q)<->(Q&P)"
s6c = "(P<->Q)<->(Q<->P)"


--associative laws 
s7a = "(Pv(QvR))<->((PvQ)vR)"
s7b = "(P&(Q&R))<->((P&Q)&R)"

--distributive laws
s8a = "(P&(QvR))<->((P&Q)v(P&R))" --prover hangs on this
s8b = "(Pv(Q&R))<->((PvQ)&(PvR))" --and this

--identity laws 
s9a = "(PvF)<->P"
s9b = "(P&F)<->F"
s9c = "(PvT)<->T"
s9d = "(P&T)<->P"

--DeMorgan laws 
s10a = "~(P&Q)<->(~Pv~Q)"
s10b = "~(PvQ)<->(~P&~Q)"

--equivalence 
s11a = "(P<->Q)<->((P->Q)&(Q->P))" 
s11b = "(P<->Q)<->((P&Q)v(~P&~Q))"
s11c = "(P<->Q)<->(~P<->~Q)"

--implication 
s12a = "(P->Q)<->(~PvQ)"
s12b = "~(P->Q)<->(P&~Q)"

--contrapositive 
s13  = "(P->Q)<->(~Q->~P)"

--reductio ad absurdum 
s14  = "(P->Q)<->((P&~Q)->F)"

s15a = "((P->R)&(Q->R))<->((PvQ)->R)"
s15b = "((P->Q)&(P->R))<->(P->(Q&R))" 
s15c = "((P->Q)v(P->R))<->(P->(QvR))"


-- exportation law 
s16  = "((P&Q)->R)<->(P->(Q->R))"

--addition 
s17  = "P->(PvQ)"

--simplification 
s18  = "(P&Q)->P"

-- modus ponens 
s19  = "(P&(P->Q))->Q"

-- modus tollens 
s20  = "((P->Q)&~Q)->~P"

--hypothetical syllogism 
s21  = "((P->Q)&(Q->R))->(P->R)"

--disjunctive syllogism 
s22  = "((PvQ)&~P)->Q"

--absurdity 
s23  = "(P->F)->~P"
s24  = "((P->Q)&(R->S))->((PvR)->(QvS))"
s25  = "(P->Q)->((PvR)->(QvR))"
          

--tim's equation
s26 = "((~P&Q)v(P&~Q))->(PvQ)"