Generalized Modus Ponens http://www.ksl.stanford.edu/software/IW/registry/SRC/IW-TEAM.daml Fri Jan 17 17:59:44 PST 2003 Thu Apr 03 15:55:19 PST 2003 For atomic sentences si, si' and r, where there is a substitution T such that subst(T,si')=subst(T,si) for all i: s1',s2',...,sn',(s1^s2^...^sn => r) implies subst(T,r) (and (= @V1 (vars @S1)) (subst @V1 (values @U1) @S1)) (and @SS1) (=> (and @SS1) @S1) (and (item @S2 @SS1) (item @S3 @SS1) (= @V2 (vars @S2)) (= @V3 (vars @S3)) ((= (subst @V2 (values @U1) @V2) (subst @V3 (values @U1) @V3)))