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