Return to prop.sml CVS log

Up to [Research Unix] / researchv10no / cmd / sml / doc / examples

Annotation of researchv10no/cmd/sml/doc/examples/prop.sml, revision 1.1

1.1     ! root        1: (* propositional calculus *)
        !             2: 
        !             3: datatype truth = TRUE | FALSE
        !             4: 
        !             5: datatype term
        !             6:   = VAR of string
        !             7:   | CON of truth
        !             8:   | NOT of term
        !             9:   | AND of term * term
        !            10:   | OR  of term * term
        !            11: 
        !            12: (* (~ p) and q  ==> AND(NOT(VAR "p"), VAR "q") *)
        !            13: 
        !            14: (* transform term to conjuctive normal form *)
        !            15: 
        !            16: fun negate (NOT(NOT p)) = negate p 
        !            17:   | negate (NOT p) = p
        !            18:   | negate (AND(p,q)) = OR(NOT p, NOT q)
        !            19:   | negate (OR(p,q)) = AND(NOT p, NOT q)
        !            20:   | negate p = NOT p
        !            21: 
        !            22: fun cnf (AND(p,q)) = AND(cnf p, cnf q)
        !            23:   | cnf (NOT(NOT p)) = cnf p
        !            24:   | cnf (NOT(AND(p,q))) = cnf(OR(negate p, negate q))
        !            25:   | cnf (NOT(OR(p,q))) = AND(cnf(NOT p), cnf(NOT q))
        !            26:   | cnf (OR(AND(p,q),r)) = AND(cnf(OR(p,r)),cnf(OR(q,r)))
        !            27:   | cnf (OR(p,AND(q,r))) = AND(cnf(OR(p,q)),cnf(OR(p,r)))
        !            28:   | cnf (OR(NOT p,q)) = cnf(OR(negate p, q))
        !            29:   | cnf (OR(p, NOT q)) = cnf(OR(p, negate q))
        !            30:   | cnf p = p
        !            31: 
        !            32: (* exercise: write a tautology checker.
        !            33:   (hint: use resolution) *)

This archive runs on limited infrastructure. Preserving old code on modern bandwidth. Automated agents are requested to crawl responsibly.