[Note] Currently only propositional (0th Order) logic is implemented. See below the current operators and rules.
- Line Number
- Statement
- Arguments
- Rule
Use the Up and Down arrow keys to move up and down a line respectively.
Pressing 'Enter' moves down a line and creates a new line when pressed on the last line.
In the statement section you can type in a statement using variables and operators.
- If the inputted statement is correct, the background of that line will turn green.
- If the inputted statement is incorrect (does not match rule), the background of that line will turn red.
- If the inputted statement is invalid (statement format not obeyed), the background of that line will turn dark red.
Inputting the '|' character will start a new sub proof and deleting it will exit the subproof.
Inputting Rules
A rule consists of two parts: The arguments and the rule itself.
- <line>, <line>,... - Inputting individual lines
- <line>-<line> - Inputting range of lines
Rules can be chosen using the drop down on the far right of the line.
In the menu bar at the top of the application, under 'File' there are the options to Import and Export files.
Exported files are in .txt format. It is possible to modify the exported proof text file, however, it is not recommended.
- ^ - Conjunction (AND)
- v - Disjunction (OR)
- ¬ - Negation (NOT)
- => - Implication
- <=> - Bi-Implication
- Hyp - Hypothesis
- Sub-Hyp - Sub hypothesis
- Copy - Copy Line
- ^E1 - Conjunction Elimination 1
- ^E2 - Conjunction Elimination 2
- ^I - Conjunction Introduction
- vE - Disjunction Elimination
- vI1 - Disjunction Introduction 1
- v2 - Disjunction Introduction 2
- =>E - Implication Elimination
- =>I - Implication Introduction
- <=>E1 - Bi-Implication Elimination 1
- <=>E2 - Bi-Implication Elimination 2
- <=>I - Bi-Implication Introduction