Declarative Rule

• Name: ND Modus Pones with Unification
• Rule Specification: p; '(implies ' r q ')' |- q[s];; (Sent p q) (= s mgu(p,r))
• Specification Language: Proof Protocol for Deductive Reasoning (PPDR)

(Registration details...)

Copyright 2009 Inference Web group.
All Rights Reserved.