Index of Basic Propositional Rules
| Name | Premises | Conclusion |
| MP | φ, φ→ψ | ψ |
| MT | ¬ψ, φ→ψ | ¬φ |
| DNE | ¬¬φ | φ |
| DNI | φ | ¬¬φ |
| S | φ∧ψ | φ |
| S | φ∧ψ | ψ |
| ADJ | φ, ψ | φ∧ψ |
| MTP | φ∨ψ, ¬φ | ψ |
| MTP | φ∨ψ, ¬ψ | φ |
| ADD | φ | φ∨ψ |
| ADD | ψ | φ∨ψ |
| BC | ψ↔φ | ψ→φ |
| BC | ψ↔φ | φ→ψ |
| CB | ψ→φ, φ→ψ | φ↔ψ |
Index of Basic Predicate Rules
| Name | Premises | Conclusion |
| UI | ∀xφx | φx(c) |
| EG | φx(c) | ∃xφx |
Index of Derived Rules
The Propositional Rule Builder
The First-Order Rule Builder