Home My Page Projects Code Snippets Project Openings SML/NJ
 Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

# SCM Repository

[smlnj] View of /archive/0.93/doc/examples/prop.sml
 [smlnj] / archive / 0.93 / doc / examples / prop.sml # View of /archive/0.93/doc/examples/prop.sml

Wed Apr 10 01:33:29 2019 UTC (3 months, 1 week ago) by dbm
File size: 911 byte(s)
`adding 0.93 src and doc to archive`
```(* propositional calculus *)

datatype truth = TRUE | FALSE

datatype term
= VAR of string
| CON of truth
| NOT of term
| AND of term * term
| OR  of term * term

(* (~ p) and q  ==> AND(NOT(VAR "p"), VAR "q") *)

(* transform term to conjuctive normal form *)

fun negate (NOT(NOT p)) = negate p
| negate (NOT p) = p (* BUG! *)
| negate (AND(p,q)) = OR(NOT p, NOT q)
| negate (OR(p,q)) = AND(NOT p, NOT q)
| negate p = NOT p

fun cnf (AND(p,q)) = AND(cnf p, cnf q)
| cnf (NOT(NOT p)) = cnf p
| cnf (NOT(AND(p,q))) = cnf(OR(negate p, negate q))
| cnf (NOT(OR(p,q))) = AND(cnf(NOT p), cnf(NOT q))
| cnf (OR(AND(p,q),r)) = AND(cnf(OR(p,r)),cnf(OR(q,r)))
| cnf (OR(p,AND(q,r))) = AND(cnf(OR(p,q)),cnf(OR(p,r)))
| cnf (OR(NOT p,q)) = cnf(OR(negate p, q))
| cnf (OR(p, NOT q)) = cnf(OR(p, negate q))
| cnf p = p

(* exercise: write a tautology checker.
(hint: use resolution) *)
```