I enjoyed researching this question and especially I enjoyed reading
the sample code. As a professional programmer, I normally have to use
languages much less elegant than ML. Thus, in the future, should you
have any ML code that needs to be written, please do not hesitate to
consider using Google Answers.
I have located a sample ML tautology checker, which seems to be
exactly what you are looking based on the description in the URL you
provided, here: http://www.cl.cam.ac.uk/users/lcp/MLbook/programs/sample4.sml.gz
.
I think the best way to navigate to this link is to go to
Sample programs for ML for the Working Programmer:
http://www.cl.cam.ac.uk/users/lcp/MLbook/programs/
Then click on "Chapter 4" . This link, however, is a zipped file. If
you are unable to unzip the file, just mention this and I would be
happy to upload an unzipped version of this file for you.
Note that the program in Chapter 4 uses the intersection program from
chapter 3, which is at the URL:
http://www.cl.cam.ac.uk/users/lcp/MLbook/programs/sample3.sml.gz .
This program is simple enough and small enough to include here:
fun inter([],ys) = []
| inter(x::xs, ys) =
if x mem ys then x::inter(xs, ys)
else inter(xs, ys);
Thus, in order to create the desired file checker.sml , just rename
the "taut" function in Chapter 4 sample program to "checker", include
the inter definition above, and you will be done.
I was actually hoping to be able to write you an ML program, because
ML is a very beautiful and elegant language, particularly for this
sort of application.
Unfortunately for me, though, it seems to me that the problem is
pretty much solved in the links above, so I do not think I can provide
added value by writing my own program here.
Note though I have not actually installed SML and tested these
programs, but they look simple and clear and should work.
Finally, as always, please remember that if you have any questions, or
if you have any difficulty viewing the URLs I mentioned, or any other
comments or concerns, please solicit clarification via the "Request
Clarification" button on your browser before rating this answer.
Search Strategy
--------------
I knew that a general search on ML and propositional logic would turn
up too many hits to be useful, but once I saw the question
clarification, I searched on "ml tautology" in google. I went through
five or six sites before finding, much to my surprise, that the exact
problem you described was solved at the URL given. |
Clarification of Answer by
rbnn-ga
on
02 Dec 2002 11:56 PST
I just realized that the "inter" function from the URL:
http://www.cl.cam.ac.uk/users/lcp/MLbook/programs/sample3.sml.gz
uses the earlier "mem" function, also from that URL, which is defined
there as:
infix mem;
fun x mem [] = false
| x mem (y::l) = (x=y) orelse (x mem l);
|
Clarification of Answer by
rbnn-ga
on
02 Dec 2002 16:26 PST
Thank you for the clarification request.
As requested, I have unzipped the files in the URLs listed above and
placed them at:
http://www.rbnn.com/google/ml/sample3.sml
and
http://www.rbnn.com/google/ml/sample4.sml
In addition, the relevant functions from both files have been
extracted and placed in the file
http://www.rbnn.com/google/ml/checker.sml
as well as taut being renamed.
I hope that this is helpful to you.
|
Request for Answer Clarification by
loeric18-ga
on
02 Dec 2002 21:26 PST
Thanks for your excellent job!!! I am going to code them and run if it
is work.
I want to know after I rate this question, can I still ask if there is
something wrong? anyway, thank you very much!!!
|
Clarification of Answer by
rbnn-ga
on
03 Dec 2002 02:16 PST
Yes, you can submit clarification requests after the question is rated.
|
Request for Answer Clarification by
loeric18-ga
on
03 Dec 2002 22:51 PST
hi, rbnn
I don't know how to appy the function checker in to the checker.sml
checker (
Disj (
Atom "A",
Neg (
Disj (
Conj (Atom "A", Neg (Atom "B")),
Conj (Neg (Atom "C"), Atom "C"))
)
)
)
I tried to applied to checker.sml and compiled it, but I couldn't.
Could you do me a favor? I know it is piece of cake for you. :P
|
Request for Answer Clarification by
loeric18-ga
on
04 Dec 2002 00:19 PST
sorry..please ignore the last request I did, it's my misunderstanding..... :P
|
Clarification of Answer by
rbnn-ga
on
04 Dec 2002 00:47 PST
It turns out that the function checker in the file checker.sml is
incorrect. The original function taut only works if its argument is in
conjunctive normal form.
The correct function checker is:
fun checker(p)= taut (cnf (nnf p));
where taut is as given in sample4.sml:
fun taut (Conj(p,q)) = taut p andalso taut q
| taut p = not (null (inter (positives p, negatives p)));
I have placed the revised version checker at:
http://www.rbnn.com/google/ml/checker.sml .
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
|
Request for Answer Clarification by
loeric18-ga
on
04 Dec 2002 16:57 PST
rbnn..YOU ARE GREAT!!!! I really appreciate it!!! :)
|
Clarification of Answer by
rbnn-ga
on
04 Dec 2002 18:14 PST
Thank you; your comments are appreciated.
|
Request for Answer Clarification by
loeric18-ga
on
19 Dec 2002 14:13 PST
hi,rynn. Do you know about Ada? I have a new question posted on, if
you are interested in it, please check it out:
https://answers.google.com/answers/main?cmd=threadview&id=127046
Please help me by tomorrow or tonight!!
|
Clarification of Answer by
rbnn-ga
on
19 Dec 2002 14:27 PST
Thank you for mentioning that to me. I would very much have liked to
tackle that question, but my brother is visiting for the next couple
of days and it is highly unlikely that I will have time.
By the way, if you wish you can put "for <researcher-name> only" in
the subject title of any question, and only that researcher will
answer it.
|
Request for Answer Clarification by
loeric18-ga
on
19 Dec 2002 17:41 PST
Hi, rbnn
I am sorry to bother you again, but I just really need some help.
The project got fixed is very important for my study. I saw nobody can
fix it, so I just rise the price to $100 (you can feel how the project
is important for me such a poor student!!) Please give it a try, you
don't need to make the project run 100% correct, but just at least can
be compiled by any way you modify. Thanks!!!
|
Clarification of Answer by
rbnn-ga
on
20 Dec 2002 11:57 PST
Fortunately, I see another researcher has answered the question.
|
,
0 Comments
)