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
dwt-ga
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
rbnn-ga
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
dwt-ga
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
rbnn-ga
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 un-negated 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 non-empty 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));
|
,
0 Comments
)