Automated Modal Reasoner

This program takes lists of formalized sentences and checks them for consistency or validity in Propositional Modal Logic (S5 Axiom System)

Since modal logic extends non-modal logic, this program can also be used for non-modal propositional logic.

Quanitifers like 'all' and 'some' are not supported at this time.

Behind the scenes, the program converts your input to Polish notation, for ease of use by the computer. You don't need to worry about that.

Instructions

Add your formulas all at once, separated by spaces. When checking validity, the last formula is treated as the conclusion.

Use infix notation. An atomic formula should be a single lowercase letter. The symbols used for connectives are shown in the table below. Do not include spaces within a formula. Use parentheses to prevent ambiguity when using multiple connectives.

For example, if you want to test the following argument for validity:

1) p and (q or r)

2) not q

3) not r

So) not p

You would enter this in the text box: p&(qVr) ~q ~r ~p

Then hit the Check Validity button. For more in-depth examples, see the Examples page.

Prefix Key

Check Consistency Check Validity Clear Formulas

Entered:

Formulas in Polish Notation:

Result:

Model: