Google Answers Logo
View Question
Q: Tuatology checker of ML Function ( Answered 5 out of 5 stars,   0 Comments )
Subject: Tuatology checker of ML Function
Category: Computers > Programming
Asked by: loeric18-ga
List Price: $5.00
Posted: 01 Dec 2002 22:34 PST
Expires: 31 Dec 2002 22:34 PST
Question ID: 117574
Where can I get the example scripts of Standard ML about "tuatology
checker" ? The ML function is about to check if a propositional formula is a
tautology. Thx

Request for Question Clarification by rbnn-ga on 01 Dec 2002 22:58 PST
I am not sure what you mean by "example scripts of ML about tautology

Are you looking for someone to write a program that performs ML
tautology checking? Are you looking for existing ML applications that
perform tautology checking?

If the former interpretation of your question is what is desired, then
I would need to know which compiler and platform you are using, what
efficiency constraints you are looking for (seeking clarity or
efficiency, for instance), and a precise function signature.  Because
it would require a lot of time for me to download a compiler and
refamiliarize myself with ML, the price as per would need to be much
higher for me to consider doing this, however.

Clarification of Question by loeric18-ga on 01 Dec 2002 23:29 PST
Hi, cuz I am a poor student ,so just looking for existing ML
applications that perform tautology checking. more info plz check the
By the way, how much would you consider to do such a program? :)
Subject: Re: Tuatology checker of ML Function
Answered By: rbnn-ga on 02 Dec 2002 11:53 PST
Rated:5 out of 5 stars
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:

I think the best way to navigate to this link is to go to 

Sample programs for ML for the Working Programmer:

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: .

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:

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:


In addition, the relevant functions from both files have been
extracted and placed in the file

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: .

Here is a sample run:

% sml.bat
Standard ML of New Jersey, Version 110.0.7, September 28, 2000
- use "checker.sml";
[opening checker.sml]
infix mem
val mem = fn : ''a * ''a list -> bool
GC #   (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 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:

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.
loeric18-ga rated this answer:5 out of 5 stars and gave an additional tip of: $5.00
Excellent job, and detailed explaination!!! Nice job!

There are no comments at this time.

Important Disclaimer: Answers and comments provided on Google Answers are general information, and are not intended to substitute for informed professional medical, psychiatric, psychological, tax, legal, investment, accounting, or other professional advice. Google does not endorse, and expressly disclaims liability for any product, manufacturer, distributor, service or service provider mentioned or any opinion expressed in answers or comments. Please read carefully the Google Answers Terms of Service.

If you feel that you have found inappropriate content, please let us know by emailing us at with the question ID listed above. Thank you.
Search Google Answers for
Google Answers  

Google Home - Answers FAQ - Terms of Service - Privacy Policy