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