Function that checks for the application of Modus Ponens, a Rule of
Implication, of the following form:
(i) p; (ii) p -> q; (iii) q
The rule has two cited lines, so we first identify the shorter vs. longer
one, then check whether the antecedent of the longer proposition matches the
shorter proposition, and the consequent matches the target proposition.
Function that checks for the application of Modus Ponens, a Rule of Implication, of the following form: (i) p; (ii) p -> q; (iii) q The rule has two cited lines, so we first identify the shorter vs. longer one, then check whether the antecedent of the longer proposition matches the shorter proposition, and the consequent matches the target proposition.