Quine's method
Author Message
Quine's method

I am studying propositional logic and one of our assignments is to
implement Quine's method in Scheme.

The input consists of a well-formed formula with the usual logic symbols
replaced by and, or, not, etc.  The wff is fully parenthesized

The output is either true or false, depending on whether the wff is a
tautology.

Whereas I can determine a tautology on paper, developing a Scheme
program to do so has been perplexing. My idea was to transform all
implications into their equivalences, and then make the true/false
substitutions. Then, Scheme (DrScheme) would be able to evaluate
things from there. I am hung up with the parentheses and priorities.
Does anyone have any ideas, words of wisdom, or suggestions that might
help?  I am, by no means, an expert in Scheme, or in logic, for that
matter. I would have posted what code I have so far, but it is no where
near to doing what it should and I am thinking of starting over
entirely.

Since this is a homework assignment, I would feel more comfortable with
receiving conceptual help rather than a completely coded program. But
any assistance would be appreciated.

Warren

Sent via Deja.com http://www.*-*-*.com/

Mon, 01 Jul 2002 03:00:00 GMT
Quine's method

Quote:

> The input consists of a well-formed formula with the usual logic symbols
> replaced by and, or, not, etc.  The wff is fully parenthesized

A few example, please, so that we can know what you are talking about?

While I guess most of us have some logic course in our past, your
article was too vague to tell me exactly what you are trying to do.

The phrase "well-formed formula" means that the formula are composed
"according to the rules", but _what_ rules?  That depends on the
unknown context.

Quote:
> Whereas I can determine a tautology on paper, developing a Scheme
> program to do so has been perplexing.

Because you don't know Scheme or because you don't really know the method?

Quote:
> My idea was to transform all implications into their equivalences,
> and then make the true/false substitutions. Then, Scheme (DrScheme)
> would be able to evaluate things from there.

"implications"?  Are you talking about (implies ... ...) forms here?
If so you might want to just define a function by that name.

You might also want to write your own "eval" that only handles these
forms.  A bit of work, but it gives you all sorts of possibilities
afterwards.

Quote:
> I am hung up with the parentheses and priorities.

What you mean by this sentence?

Stig Hemmer,

Tue, 02 Jul 2002 03:00:00 GMT
Quine's method

Quote:

> I am studying propositional logic and one of our assignments is to
> implement Quine's method in Scheme.

> Whereas I can determine a tautology on paper, developing a Scheme
> program to do so has been perplexing. My idea was to transform all
> implications into their equivalences, and then make the true/false
> substitutions.

That would be the general idea. You can use a binary tree to represent your
formula, and, while traversing the tree, substitute T or F for the
propositional variables, using the 12 simplifying rules provided by Quine's
algorithm.

You could see the algorithm as a kind of "Rewriting" based on those rules

Quote:
> Then, Scheme (DrScheme) would be able to evaluate
> things from there. I am hung up with the parentheses and priorities.

You should not be concerned with "parentheses and priorities". A recursive
formulation of the rewriting problem should do the job. If you're not
familiar with formulas/tree manipulation, you should find in many textbooks
example programs i.e., for symbolic computation or converting infix to
prefix notation that will give you the general idea.

Marc

Fri, 05 Jul 2002 03:00:00 GMT

 Page 1 of 1 [ 3 post ]

Relevant Pages