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.

   
KEYBOARD   MODELS   COUNTERMODELS  
p q r   p q r p q r   p q r
       
UNSAT
       
TAUT
       
CONTG
       
ILL-FD

Instructions

You can write a propositional formula using the above keyboard. You can use the propositional atoms p,q and r, the "NOT" operatior (for negation), the "AND" operator (for conjunction), the "OR" operator (for disjunction), the "IMPLIES" operator (for implication), and the "IFF" operator (for bi-implication), and the parentheses to state the precedence of the operators. For example, the formula:

will be written as follows:

"NOT"   "("   "q"   "IFF"   "("   "p"   "IMPLIES"   "("   "r"   "OR"   "p"   ")"   ")"   ")"  

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