Generalized Modus Ponens
<atomic sentence> := <relational sentence>
<literal> := <atomic sentence> | (not <atomic sentence>)
Substitution - Set of pairs of term expressions
Subst(?, S) result of applying substitution ? to sentence S
E.g., Subst({?x/Sam, ?y/Pam}, (Likes ?x ?y)) = (Likes Sam Pam)
Inference rule
For literals p1,
, pn, p1,
, pn, and q; and
substitution ? of term expressions for variables such that
Subst(?, p1) = Subst(?, p1),
, Subst(?, pn) = Subst(?, pn):
p1,
, pn, (=> p1
pn q)
-----------------
Subst(?, q)