MUFT Instructions

This is the Most User-Friendly Theorem Tester for propositional logic.

A row beginning with 'p:' contains a premise. A row beginning with 't:' provides a proposition to be tested. Rows beginning with neither are ignored. The program tests for each of the test propositions whether it follows from the given premises. If it does, the program says so. If it doesn't, the program provides a counterexample. The counterexample is given by stating all and only the true atomic propositions.

MUFT uses Reverse Polish Notation (RPN). This is very convenient when writing the program--not so convenient when using it! (Yes, the name of the program is ironic.)

Also, for ease of parsing, the following single characters are used for the logical connectives:

Negation:	~
Conjunction:	&
Disjunction:	|
Implication:	>
Equivalence:	=

As a propositional variable, any upper or lower case letter from the English alphabet can be used. (But at most 12 variables in any run. And a variable can only consist of a single letter.)

Here are som example logical expressions:

Normal	MUFT
A -> B	AB>
(P & Q) v R	PQ&R|
P & (Q v R)	PQR|&
(r -> s) <-> (~s -> ~r)	rs>s~r~>=