***     COSC3308        SNOBOL PROGRAM-9                Fall 2006
**			Logic Checker
**      This program checks the logical validity of
***     simple propositional logical expressions involving four operators
***     1. NOT
***     2. AND
***     3. OR
***     4. IMP
***     and operands
        &TRIM  =  1
        UnOp =  "NOT"
        BinOp =  "AND"  |  "OR"  |  "IMP"
        Formula =  " " UnOp . Op  "("  BAL .  First ")" |
+                  " " BinOp . Op "("  BAL .  First ","  BAL . Second  ")"
        Atom =  (' '  BAL  ' ') .  Opd
        define('Wang(Ante,Conseq)First,Second')
***     Main program starts here
READ    Exp = INPUT                                     :F(Done)
        Count = Count + 1
        Output =  
        Output =  "INPUT COUNT:" Count  ":" Exp
        Wang(, " " Exp)                                 :F(InValid)
        Output = "                   IS VALID..."       :(READ)
InValid OUTPUT = "                   IS NOT VALID..."   :(READ)
*** Start of the function Wang that checks the validity of an expression
*** in terms of its antecedent and its consequent.
Wang    Ante  Formula =                                 :S($("A" Op))
        Conseq Formula  =                               :S($("C" Op))
        Ante   = " " Ante   " "
        Conseq = " " Conseq " "
Test    Ante Atom  =  ' '                               :F(Freturn)
        Conseq Opd                                      :S(return)F(Test)
***     ANOT
ANOT    Wang(Ante, Conseq  ' ' First)                   :S(Return)F(Freturn)
***     AAND
AAND    Wang(Ante ' ' First ' ' Second, Conseq)         :S(return)F(Freturn)
***     AOR
AOR     Wang(Ante ' ' First, Conseq)                    :F(Freturn)
        Wang(Ante ' ' Second, Conseq)                   :F(Freturn)S(Return)
***     CNOT
CNOT    Wang(Ante ' ' First, Conseq)                    :F(Freturn)S(Return)
***     COR
COR     Wang(Ante, Conseq ' ' First ' ' Second)         :F(Freturn)S(Return)
***     CAND
CAND    Wang(Ante, Conseq ' ' First)                    :F(Freturn)
        Wang(Ante, Conseq ' ' Second)                   :F(Freturn)S(Return)
***     AIMP
AIMP    Wang(Ante " " Second, Conseq)                   :F(Freturn)
        Wang(Ante, Conseq " " First)                    :F(Freturn)S(Return)
CIMP    Wang(Ante " " First, Conseq " " Second)         :F(Freturn)S(Return)
Done    Output =
        Output =  "THERE ARE "  Count " INPUT EXPRESSIONS..."
End
OR(ABC,NOT(ABC))
IMP(AND(IMP(A,B),INP(B,C)),IMP(A,C))
IMP(IMP(IMP(A,B),C),IMP(A,IMP(B,C)))
IMP(IMP(A,IMP(B,C)),IMP(IMP(A,B),C))
AND(OR(A,B),NOT(AND(A,B)))
OR(AND(AND(A,B),C),NOT(AND(AND(A,B),C)))