How to use the program


If you want to validate a formula, please type the formula in 'Latex' format.

Such as ( ( ( (A \to B) \land (B \to C) ) \land A ) \to ( B \land C ) )

Make sure to use an uppercase letter as an atom and insert enough braces.


The program works fine in IE, Opera, Safari, Chrome and several other browsers.

However, the script doesn't work in Firefox.

Technical Details

The input of our system is a propositional formula, but our project aims to validate a sequent in the form of x1, x2, ..., xn |- y, so first we need to convert the sequent to a propositional formula. For example, a sequent like x1, x2, ..., xn |- y will be convert to ( x1 \land x2 \land ... \land xn ) \to y. Then we assume the left part of the formula is True, if we could prove the right part is also True, then according to complete and soundness of propositional logic, we can say the sequent is valid.

Although we have conventions about the binding priorities of propositional relations. In our system, we require users to reinsert certain brackets so that it is easier for parsing process. The format of all binary relations should be like (A*B). The format of all unary relations should be like (*A). Another limitation is that we require the propositional atoms should be uppercase English letter from A to Z. Since if we create new nodes, we would like to use non-negative integer numbers as labels. In order to differentiate those nodes, we require the labels of propositional atoms as uppercase English letters.

To view our technical report, please click Here.