Inference Rules
Transitivity of Equal ? Unit Resolution
(= T1 T2), (= T1 T3) (or S1 S2), (not S1)
---------------- ---------------
(= T2 T3) S2
Modus Tollens ? Universal Elimination
(=> S1 S2), (not S2) (forall ?var S)
--------------- --------------
(not S1) Subst({?var/g}, S)
And Elimination ? And Introduction
(and S1 … Sn) S1, …, Sn
------------ ------------
Si (and S1 … Sn)
Existential Introduction
Given sentence S in which variable ?var does not occur:
S
------------------------
(exists ?var Subst({?var/C}, S)