About

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.

Syntax

Sequents are inputted as follows: A, B, ... --> C, D, ... The following connectives and quantifiers are available:

	Symbol	In text
Logical NOT	¬	¬	~	-
Logical AND	∧	/\	&	&&	*	.
Logical OR	∨	\/	\/	+	|	||	,
Conditional	→	->	>	=>
Biconditional	↔	<->	=	<>	<=>
Falsum	⊥	#	_|_
Universal quantifier	∀	A	@
Existential quantifier	∃	E
Relation	A—Z	A—Z
Variable/Constant	a—z	a—z

Conventions

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:

• mostly resembling (at the time of writing) Wikipedia's article on node calculus (LK).
• But without the cut rule (which is, of course, not strictly required for completeness).
• Eigen-variables are distinguished from bound variables, and both are different from constants.
• To keep things clean, lists of formulas are treated as sets, and structural rules are skipped.

Author