## The Propositional Logic Calculator |
||||

The Propositional Logic Calculator finds all the
models of a given propositional formula.

The only limitation for this calculator is that you have only three
atomic propositions to choose from: **p**,**q** and **r**.

will be written as follows:

To cancel the last input, just use the "DEL" button. Once you have typed in a formula, you can start the reasoning process by pressing "ENTER". In order to start again, press "CLEAR".

The outcome of the calculator is presented as the list of "**MODELS**", which are all the truth value
assignments making the formula true, and the list of "**COUNTERMODELS**", which are all the truth value
assignments making the formula false. The truth value assignments for the
propositional atoms **p**,**q** and **r** are denoted by a
sequence of **0** and **1**. For example, an assignment where **p**
and **r** are true and **q** is false, will be denoted as:

If the formula is true for every possible truth value assignment (i.e., it
is a tautology) then the green lamp **TAUT** will blink; if the formula
is false for every possible truth value assignment (i.e., it is
unsatisfiable) then the red lamp **UNSAT** will blink; the yellow lamp
will blink otherwise. If the formula is not grammatical, then the blue
lamp will blink.

Enrico Franconi, University of Manchester, Department of Computer Science, franconi@cs.man.ac.uk

Last modified: Sat Sep 30 20:04:45 BST 2000