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