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

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.