This tool uses inversion principle to automatically find proofs of sequents, in a language without function symbols. It performs a tiny bit of automated guidance by bookkeeping instantiation times etc., but is not very smart, and will probably take too long for complex formulas.
Sequents are inputted as follows: A, B, ... --> C, D, ... The following connectives and quantifiers are available:
Note that relational symbols (including propositions) are limited in length to one character. Letters 'A' and 'E' can be used for propositions (0-ary relations), but it might be confusing. However, this tool will correctly detemine whether Ax is universal quantification or an atomic formula, assuming there are no typos in the starting formula.
You should put brackets everywhere, except when it doesn't matter. The only predefined precedence is that all unary operators (including quantifiers) have higher priority than binary operators.
Rules for the system: