Generalized Modus Ponens
<atomic sentence> := <relational sentence> | <equation>
<literal> := <atomic sentence> |
(not <atomic sentence>) | <inequality>
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,
where there is a substitution ? such that
Subst(?, p1) = Subst(?, p1),
, Subst(?, pn) = Subst(?, pn):
p1,
, pn, (=> p1
pn q)
---------------------
Subst(?, q)