| Command | Section |
|---|---|
| Add Premise | 2.1 |
| Add Conclusion | 2.1 |
| Close Path | 2.6, 3.5.3, 4.4, 6.1 |
| Close Table | 2.7, 4.4 |
| Edit Title | 1.6 |
| Edit Comment | 1.6 |
| Remove Title | 1.6 |
| Remove Comment | 1.6 |
| List Unbridged Subtables | 2.7 |
| Command | Section |
|---|---|
| Decompose Conjunction | 2.5 |
| Decompose Disjunction | 2.5 |
| Decompose Conditional | 2.5 |
| Decompose Biconditional | 2.5 |
| Remove Double Denial | 2.5 |
| Alter Denied Conjunction | 2.5 |
| Alter Denied Disjunction | 2.5 |
| Alter Denied Conditional | 2.5 |
| Alter Denied Biconditional | 2.5 |
| Modus Ponens | 2.5 |
| Law Of Excluded Middle | 3.5.2 |
| Command | Section |
|---|---|
| Perform Substitution | 3.5.1 |
| Instantiate Universal Variable | 3.3 |
| Instantiate Existential Variable | 3.3 |
| Alter Denied Quantifier | 3.3 |
| Command | Section |
|---|---|
| Decompose Necessity | 4.3 |
| Decompose Possibility | 4.3 |
| Decompose Box-Arrow | 5.3 |
| Decompose Diamond-Arrow | 5.3 |
| Alter Denied Modal | 4.3 |
| Alter Denied Nonmonotonic | 5.3 |
| Box-Definition | 5.3 |
| Diamond-Definition | 5.3 |
| Modal Law Of Excluded Middle | 4.5 |
| Command | Key Combination |
|---|---|
| ¬ | Option-shift-hyphen |
| ∨ | Option-v |
| → | Option-e, a |
| ↔ | Option-i, a |