Thank you for your question. I enjoy ML coding, as it is a very
beautiful language.
Coincidentally I just solved exactly this problem, and have the
solution ready for you, from:
https://answers.google.com/answers/main?cmd=threadview&id=117574.
A solution is at:
http://www.rbnn.com/google/ml/checker.sml
based on the URLs:
http://www.cl.cam.ac.uk/users/lcp/MLbook/programs/sample3.sml.gz
http://www.cl.cam.ac.uk/users/lcp/MLbook/programs/sample4.sml.gz
from:
Sample programs for ML for the Working Programmer:
http://www.cl.cam.ac.uk/users/lcp/MLbook/programs/
These URLs are in gzipped format, if you cannot read them they have
been unzipped, respectively, here:
http://www.rbnn.com/google/ml/sample3.sml
http://www.rbnn.com/google/ml/sample4.sml
Here is a script illustrating that code:
Here is a sample run:
% sml.bat
Standard ML of New Jersey, Version 110.0.7, September 28, 2000
[CM&CMB]
 use "checker.sml";
[opening checker.sml]
infix mem
val mem = fn : ''a * ''a list > bool
GC #0.0.0.0.1.15: (0 ms)
val inter = fn : ''a list * ''a list > ''a list
datatype prop
= Atom of string  Conj of prop * prop  Disj of prop * prop  Neg
of prop
val nnf = fn : prop > prop
val distrib = fn : prop * prop > prop
val cnf = fn : prop > prop
exception NonCNF
val positives = fn : prop > string list
val negatives = fn : prop > string list
GC #0.0.0.0.2.59: (0 ms)
val taut = fn : prop > bool
val checker = fn : prop > bool
val it = () : unit
 checker (
Disj (
Atom "A",
Neg (
Disj (
Conj (Atom "A", Neg (Atom "B")),
Conj (Neg (Atom "C"), Atom "C"))
)
)
)
;
val it = true : bool
 checker(Atom "A");
val it = false : bool

Should you like any more information or explanation, please do use the
"Request Clarification" button before rating this answer. 
Request for Answer Clarification by
dwtga
on
04 Dec 2002 23:12 PST
Thank you for your answer, but I need a brand new one. This one is
been used for others. Would you write a totally different SML code for
me? That will be great for me...Would you?

Clarification of Answer by
rbnnga
on
05 Dec 2002 00:33 PST
I have rewritten the file as requested.
I have changed the names to follow exactly the definition in the
problem specification; I have removed the distribute function; I have
removed the inter function and replaced it with an intersects
function; and have made several other simplifying changes.
I have placed the revised file at:
http://www.rbnn.com/google/ml/checker2.sml .
Here is a log file:
checker (
Disj (
Atom "A",
Neg (
Disj (
Conj (Atom "A", Neg (Atom "B")),
Conj (Neg (Atom "C"), Atom "C"))
)
)
)
Here is the actual code:
(*version 3*)
datatype form =
Atom of string  Neg of form  Conj of form * form  Disj of
form * form;
fun NNF (Neg(Neg p))= NNF p
 NNF (Neg (Conj(p,q))) = NNF (Disj (Neg p, Neg q))
 NNF (Neg (Disj(p,q))) = NNF (Conj (Neg p, Neg q))
 NNF (Conj(p,q)) = Conj(NNF p, NNF q)
 NNF (Disj(p,q)) = Disj(NNF p, NNF q)
 NNF (Neg p) = Neg (NNF p)
 NNF (p) = p;
fun CNF (Conj(p,q)) = Conj (CNF p, CNF q)
 CNF (Disj(p,Conj(q,r))) = Conj(CNF(Disj(p,q)), CNF(Disj(p,r)))
 CNF (Disj(Conj(q,r),p)) = Conj (CNF (Disj (q,p)), CNF (Disj
(r,p)))
 CNF p = p;
fun atoms (Atom a) = [a]
 atoms (Disj(p,q)) = atoms p @ atoms q
 atoms _ = [];
fun negations (Neg(Atom a)) = [a]
 negations (Disj(p,q)) = negations p @ negations q
 negations _ = [];
fun intersects(_,[])= false
 intersects([],_)=false
 intersects(p,q)=((hd p)=(hd q)) orelse intersects (p,tl q) orelse
intersects (tl p, q);
fun tautology (Conj(p,q)) = tautology p andalso tautology q
 tautology p = intersects(atoms p, negations p);
fun checker(p)= tautology (CNF (NNF p));

Request for Answer Clarification by
dwtga
on
05 Dec 2002 08:06 PST
Thanks for your code, Would you give me some comments in the
code to explain what is happening. That will be helped me a lot...appreciate it.

Clarification of Answer by
rbnnga
on
05 Dec 2002 08:54 PST
Sure.
I have uploaded a commented version of checker2.sml to:
http://www.rbnn.com/google/ml/checker2.sml
and I have pasted it below (although sometimes code does not paste
very clearly) .
Because ML is interpretive, I recommend also just trying out different
examples to see what happens. For example, try
intersects (["a"], ["b" , "a"])
and similarly with the other functions
(*follows the description here:
http://www.geocities.com/dwt06182002/tautology_checker.htm*)
(* A propositional formula*)
datatype form =
Atom of string  Neg of form  Conj of form * form  Disj of
form * form;
(*NNF takes a propositional formula as input and
converts it into an equivalent formula in negation normal form that
has only literals negated
*)
fun NNF (Neg(Neg p))= NNF p
 NNF (Neg (Conj(p,q))) = NNF (Disj (Neg p, Neg q))
 NNF (Neg (Disj(p,q))) = NNF (Conj (Neg p, Neg q))
 NNF (Conj(p,q)) = Conj(NNF p, NNF q)
 NNF (Disj(p,q)) = Disj(NNF p, NNF q)
 NNF (Neg p) = Neg (NNF p)
 NNF (p) = p;
(*CNF takes a propositional formula in negation normal form as input
and converts it recursively
using the distributive law into a propositional formula in conjunction
normal form. The algorithm follows the
description.*)
fun CNF (Conj(p,q)) = Conj (CNF p, CNF q)
 CNF (Disj(p,Conj(q,r))) = Conj(CNF(Disj(p,q)), CNF(Disj(p,r)))
 CNF (Disj(Conj(q,r),p)) = Conj (CNF (Disj (q,p)), CNF (Disj
(r,p)))
 CNF p = p;
(* The function Atom takes as input a propositional form that is a
disjunct of literals and returns
a list of the atoms that appear as unnegated literals in that
form. *)
fun atoms (Atom a) = [a]
 atoms (Disj(p,q)) = atoms p @ atoms q
 atoms _ = [];
(* The function negations takes as input a propositional form that is
a disjunct of literals and returns a list of the
atoms that appear as negated literals in the form*)
fun negations (Neg(Atom a)) = [a]
 negations (Disj(p,q)) = negations p @ negations q
 negations _ = [];
(* The function intersects takes two lists and returns true if they
have nonempty intersection*)
fun intersects(_,[])= false
 intersects([],_)=false
 intersects(p,q)=((hd p)=(hd q)) orelse intersects (p,tl q) orelse
intersects (tl p, q);
(*The function tautology takes as input a form that is in conjunction
normal form and determines if it is a tautology.
A conjunct in the conjunction normal form is a tautology if and only
if its atoms and negated atoms intersect nontrivially, that
is, if there both A and ~A occur in the same conjuct for some atom
A.*)
fun tautology (Conj(p,q)) = tautology p andalso tautology q
 tautology p = intersects(atoms p, negations p);
(*The function checker takes a propositional form as input, converts
it into conjunction normal form, and then determines using
tautology whether or not the form is a tautology*)
fun checker(p)= tautology (CNF (NNF p));
