Introduction

This help page is meant to describe this online deductive system logic.html. The system is written entirely using dynamic HTML and JavaScript and is based on the method put forth in Manna and Waldinger, The Deductive Foundations Of Computer Programming. This help page is not meant as a tutorial for learning logic, only as a guide to the features or bugs in this implementation.

The requirements for using this system is a reasonably new browser that at least supports style sheets and JavaScript. I did my testing on Netscape 4.61 running on a Linux system and it runs great on it. However some basic testing with the same version of Netscape on other platforms and with Internet Explorer show quite a few problems mostly in the area of stylesheets, so use at your own risk. If you can get by the problem of the messed up user interface, the results you'll get will be fine.

The initial window is the window that contains all the code and data driving the system. If this window is closed, all data that has been generated, including any tableau is lost.

The main window consists of several parts, each of which is described below.

Tableau

The tableau is the main unit of data that you will work with. It consists of rows that contain either assertions or goals. To complete a proof, it is necessary to end up with either true for a goal, or false for an assertion.

To display or redraw the current tableau, click on refresh in the main window. The tableau window can be safely closed, thrown around, or mutilated, and the tableau data will remain safe.

Adding the initial assertions and/or goals can be done from the main window. See the section on entering expressions below for more information about the input format used by the system.

Naming the tableau does nothing but put that name into the title of the tableau window, which could be useful if you are printing the tableau or saving the tableau, or if you're just vain and want to see your name on a web page.

Undo allows you to remove the last row(s) added by the last rule applied. See the rules below.

Selecting Subexpressions

Different rules require a different number of subexpressions to be selected. Selecting subexpressions is done in the tableau window. There are two different levels of selection, since rules like resolution require that there be two groups of expressions.

Expressions will be highlighted when the mouse passes over them. To actually make the selection, press the left mouse button. Repeated selection of the same subexpression will cycle the background color to indicate the type of the selection. By default, light blue is used to indicate that a subexpression is in group 1 and light pink is used to indicate group 2. See the customization section for how to change these colors if you so desire.

Control clicking will increase the selection range. Shift clicking will reverse the direction that the colors cycle. Note this currently only seems to work under Netscape.

Passing the mouse over a rule will select the subexpressions that the rule was applied to.

Clicking the deselect all button will deselect everything currently selected.

Polarity

The polarity of all selected subexpressions is by default automatically displayed. This can be useful, but it can also be annoying so there is an option to hide all polarities and to never show them. This can save you some valuable space in your tableau.

Printing/Saving

To print a tableau, use your browser's print command to print the page displaying the tableau.

Saving and restoring a tableau is more difficult since this is a complete online system. The current method is as follows: you click save and a new window is opened. Then tell your browser to save that document to wherever you wish. When you want to restore a tableau, just reopen that document in your browser.

Note: There seems to be a problem at least with Netscape. As soon as you click on one of the links to restore the tableau, all data stored in the document is lost. So, if you want to save your tableau, the best idea is to immediately save the document to disk. However, if you are only interested in merging tableau (see below), then you don't need to save to disk. Of course, if you reload the tableau, you can always resave at any time.

There are two options for restoring a tableau. You can restore it as a standalone tableau, which just means a new window will be opened and your tableau will be loaded into it. The other option is to restore the tableau into a shared window. This allows for the joining of tableaux. If you have two tableaux which you wish to join together, save both tableau, and restore them both into a shared tableau.

Entering Expressions

Expressions are entered when adding the initial assertions and goals. The format follows largely that of Manna and Waldinger. The assumptions about whether identifiers are functions, predicates, etc, are as follow: Any identifier that begins with 'a' through 'c' or 'f' through 'h' are treated as functions, variables begin with 'u' through 'z' and anything else is treated as a predicate. Note that case is not significant here when determining the type of an identifier but is significant in general. That is, 'x' and 'X' are both variables but stand for different variables. Note that there is no constant type. A constant is simply a function with no arguments.

The default type of an identifier can be changed using one of several syntactical constructs. An identifier can be prefixed by one of '$', '@', and '?' to force an identifier to be treated as a variable, function, or predicate respectively.

The syntax of expressions mostly follows that of Manna and Waldinger with the following exceptions:

There is no conditional operator, the if-then-else construct
if-then is written a p -> q (or something else for the -> if customized)

Here are some examples of valid expressions:

p and q or not r
p and p <-> p
(forall x)p(x)
(forall x, y)(p(f(x, y), b) -> (exists z)q(z))

Whitespace is not significant except around identifiers and alphanumeric keywords. The keywords used to recognize the logic symbols in parsing can be customized. See the customization section below.

Rules

This section allows you to interactively apply rules to rows in the tableau.

Simplification

All simplifications are performed automatically.

Rewriting

Make sure only one expression is selected. If any rewrite rules are applicable, the drop down list will contain expressions that can be used to rewrite the selection. Select the rewrite desired and a new row will appear in the tableau.

Splitting

Select one top level expression that can be split. There are three splits allowed: 'AND' split for assertions, 'OR' split for goals and, 'IF-THEN' split for goals.

Skolemization

This rule is used to remove quantifiers from expressions. Select a row or quantifier and all quantifiers in that expression that can be eliminated will be automatically removed. Note that this only works on quantifiers of either strict universal or existential force, and a quantifier of existential force must not be in the scope of another quantifier of universal force.

Resolution

Resolution requires two groups to be selected from two rows. All the expressions in group one will be replaced by false and all the expressions in group two will be replaced by true. Note that the polarity strategy as put forth in Manna and Waldinger need not be followed, although a warning will be given.

Equivalence/Equality Rule

These two are extremely similar rules. Like resolution, they require the selection of two groups from two rows. This is probably best explained with an example. Suppose you had an assertion of p <-> q and a goal of p. You could click once on the p from the assertion to put it into group one. Then you would click twice on the p from the goal to put it into group two. You would then apply the equivalence rule, which would replace the equivalence with false, replace the p from the goal with q and finally add a goal of q to the tableau after simplification.

The equality rule is exactly the same with the equivalence operator replaced by equality and predicates replaced by terms.

Unification

Unification is performed automatically for the resolution, equivalence and equality rules. The unifier used is displayed under the rule in the tableau.

Customizations

Due to the limits of text input and text output, there are many possible ways of displaying a particular logic symbol. This section allows you to give a list of strings that will be recognized as valid input for a particular logic symbol, or to define the string that will be used as output for a logic symbol. The basic rule is that symbols should consist entirely of non-alphanumeric characters (i.e '->') or consist entirely of alphanumeric characters (i.e. 'and').

You can also change the highlighting color used to display selections in the tableau. The value here can be any valid JavaScript color or hexadecimal RGB color value.

Finally, by default, when you leave the page or when you create a new tableau, it asks you if you wish to save the tableau. You can turn that off by unchecking the confirm actions checkbox.

Bugs and Other Comments

The biggest problem I had was that I couldn't get dynamic HTML to do anything reasonably dynamic. I'm sure some of the most noticeable problems are with the user interface screwing up. One that I've seen is that selections don't quite work for text that is wrapped to the next line. The best solution right now seems to be expanding the width of the window to the maximum that you can. Problems seem to only come up when the text from a single row spans multiple lines.

Actually I have just performed some tests on different browsers and platforms and all I can say is that I give up. It works fine on my system and I don't have the time to figure out how to write platform independent and browser independent dynamic HTML (which takes up only a very small fraction of the code, yet is the most visible thing).

Why did I write this program? No reason really. Do I think this is really that useful? Not really. Am I crazy? Quite probably.

Acknowledgements

I would like to thank Professor Zohar Manna for teaching me everything I know about logic. I would also like to ask the guys who developed these web browsers what they were thinking when they added "features" that aren't compatible with any browsers, even their own running on a different machine.

Questions, comments? Contact me.

Austin Che
email