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