Welcome to the expression evaluator.

This page in Romanian Translated by Aleksandra Seremina and hosted by azoft)

In general, if anyone wants to translate my pages, and provides pointers in the translation back to my pages, I'm not opposed to my putting in pointers to the translations.

- Expression evaluator (Basic boolean expressions, without quantifiers or predicates)
- Simple World evaluator (Predicates and quantification over a simple example world)
- Frog World evaluator (Predicates and quantification over some statements from a frogs point of view)

- nil world (Basic boolean expressions, without quantifiers or predicates)
- Simple World (Predicates and quantification over a simple example world)
- Frog World (Predicates and quantification over some statements from a frogs point of view)

You may freely download the Source Code, for non-commercial, educational, or personal use.

Don't sell it, but feel free to use it as an example.

Just download the Source Code, and look at the Instructions to define Worlds.

These evaluators are just toys, but they get the idea across, I hope.

They may be of use to beginning students.

If you find these useful or interesting, then write me. Feedback will determine whether or not other diversions like this are written.

The evaluator is a CGI program written in Perl.

It was written as a quick hack... and it shows it.

If you are really interested, you can get a copy of the source code for the program.

The program basicly just parses an expression, and then evaluates the resulting tree with each possible combination of values for the free variables and logic values.

As an aid to users, Existential quantifiers at top level return a list of the objects for which it is true. If a universal quantifier at top level is false, it returns a list of the objects that make it false.

Since the general decision procedure for quantified logic is undecidable, the only obvious way to have quantifiers was to restrict the domain to a small enumerable world.

Another simplification was to force an interpretation that just had the two traditional truth values.

These decisions both allow for simple procedures to decide true of expressions by enumeration.

I secretly believe in N-ary functions, and I've gone back and forth on whether functions here are binary or not. At the moment some are (equals) and some are not ('and', 'or'). For truth function tests it doesn't really make much difference.

If I were to do this over again I'd probably make the code that enumerates for quantifiers do all enumeration. This could be done by assuming a "forall" around the expression for each free variable.

A side affect of doing this is that the values that x has to range over HAVE to include true and false themselves. I have mixed feelings about this.

Doing so also poses problems if one ever wanted to extend this to Modal logics, since you don't always get the same result bolting modal operators to that system than you do bolting it to standard predicate calculus.

In worlds without objects exists(x,true) currently returns false, on the grounds that there exist no x. If our quantifiers also range over the traditional truth values, then this comes out true instead. (Because some objects exist.) It is bizarre to me that my intuition would lead me to this mess.

I am interested in corresponding with anyone that is interested in discussing these issues.

Worlds are read from a file, so the evaluator can handle alternate worlds.

I'm accepting suggestions for alternate worlds...

Here are Instructions to define Worlds

This page is http://www.cc.utah.edu/~nahaj/logic/evaluate/

© Copyright 1999-2011 by John Halleck, All Rights Reserved.

This page was last modified on October 26th, 2011.