Modus Ponens generalized

This page describes the design of a tactic replacing a predicate $P$ in either an hypothesis or a goal by $\btrue$ (respectively $\bfalse$ ) if $P$ (respectively $\lnot P$) is an hypothesis. That tactic is slightly different from the one requested : Feature Request #3137918

Objective

A sequent can be simplified by finding every occurrence of an hypothesis in the others hypothesis or goal, and replacing it by $\btrue$ or $\bfalse$ as explained below:

$\frac{P,\varphi(\btrue) \vdash G}{P,\varphi(P) \vdash G} \qquad \frac{P,\varphi(\bfalse) \vdash G}{\lnot P,\varphi(P) \vdash G} \qquad \frac{P \vdash \varphi(\btrue)}{P \vdash \varphi(P)} \qquad \frac{P \vdash \varphi(\bfalse)}{\lnot P \vdash \varphi(P)}$

Contrary to the Feature Request, the rule is applied on every occurrence of $P$ and not only on the one appearing in a disjunctive form. Also, not to make explode the analyzing-time of a sequent, only goal and visible (or selected, it is still in discussion) hypothesis can be re-written, using every hypothesis (global and local). The analyzing-time performance of a sequent can be problematic since every predicate of goal and visible (or selected) hypothesis are checked. But it is still worthy because it may simplify a lot, and so make proof obligation more legible to humans.

Legacy

There already exists a reasoner that does a part of that tactic : autoImpF (ImpE automatic). It looks for implicative hypothesis in a sequent. Among the predicates computed by breaking possible conjunctions in the left side of the implication, it checks if some appear in selected hypothesis. In that case, every predicates which are hypothesis (global or local) are removed from the left-sided-predicate of the implication. If it remains no predicates, then the right side of the implication is re-written as a list of conjunction, else implication is re-written without the removed predicates (possibly none).

Then this reasoner can be considered as "intelligent" because it finds itself the positions where apply, which infer a code hard to read. On the contrary, as reasoners are in the trust-base, they should be easily understandable.

Modifications are provided to make it more legible.

Design Decision

The main drawback of this tactic is its execution time. Indeed, each (actually it is not the case but it helps to see how greedy this tactics can be) sub-predicate of each goal and visible (or selected) hypothesis is compared to the others hypothesis (global and local). Several strategies can be applied in order to reduce that execution-time :

• Each hypothesis must be scanned only once to avoid accumulating predicate's running time. From that point of view, two decisions can be inferred :
  • A given predicate is compared once to every hypothesis. For instance, we do not try to find every occurrence of an hypothesis among the goal and the visible (or selected) hypothesis. In that case, each predicate would be scanned many times, accumulating execution time.
  • That tactic apply the rules specified here-above everywhere it is possible. Thus, from this set of hypothesis :
    • $\lnot P_1$
    • $P_1 \limp P_2$
    • $(P_1 \limp P_2) \limp P_3$

1. We will reach immediatly :
   • $\lnot P_1$
   • $\bfalse \limp P_2$
   • $\btrue \limp P_3$
2. Which will be re-written to :
   • $\lnot P_1$
   • $\btrue$
   • $P_3$

1. Instead of writing :
   • $\lnot P_1$
   • $\bfalse \limp P_2$
   • $(P_1 \limp P_2) \limp P_3$
2. Re-written :
   • $\lnot P_1$
   • $\btrue$
   • $(P_1 \limp P_2) \limp P_3$
3. And then :
   • $\lnot P_1$
   • $\btrue$
   • $(\bfalse \limp P_2) \limp P_3$
4. Re-written :
   • $\lnot P_1$
   • $\btrue$
   • $P_3$

• When a predicate match an hypothesis, its children must not be analyzed.

$\lnot P_1$

$P_1 \limp P_2$

$(P_1 \limp P_2) \limp P_3$

In that example, the sub-predicate $(P_1 \limp P_2)$ of the third predicate match to the second one. It has to be replaced by $\btrue$, and all its children have to be not analyzed (even if $P_1$ could have been replaced by $\bfalse$ because of the first predicate).

• In the case of n-ary predicates, each possibility is not tested.

$P \lor Q$

$P \lor R \lor Q \lor S \lor T$

$\lnot P \land \lnot Q \limp R$

In that example, $P \lor Q$ could be replaced by $\btrue$ in the second predicate. In order not to add more calculation time, this kind of replacement is not computed.

That reasoner can be considered as "intelligent", similarly to autoImpF because it computes by its own where it has to apply the rules.

Implementation

In this part is explained how the previous choices have been implemented with Java. To do so, a new re-writer has been created : EquivalenceRewriter. For a given predicate, it substitutes every occurrence of a predicate by another one. Those two last are parameters of the re-writer.

1. First, every hypothesis of the sequent is stocked in a Set called hypSet. If the hypothesis is a negation (e.g. $\lnot P$) then its child ($P$) is actually the predicate stored in the set.
2. • Then the goal is analyzed, i.e. each sub-predicate is compared to the predicates contained in hypSet (the set of hypotheses). If there is a match, the predicate is stored in a set (modifGoalSet), else, children of the sub-predicate are analyzed in the same way. Finally, the set contains all the sub-predicate that can be replaced in the goal. But, the goal itself cannot be contained in that set. If it was the case, it would mean that the goal (or its negation) is an hypothesis, and a tactic already process that case. Also, if the goal is a negation, then the first child cannot be contained in the set for the same reasons.
   • Visible (or selected) hypotheses are analyzed like the goal. The only difference is that information are stored in a map (modifHypMap) : the key is the hypothesis to be re-written, the value is a set of all the sub-predicate that can be replaced. As for the goal, the hypothesis (or its child if the hypothesis is a negation) cannot be contained in that set.
3. • Afterwards, goal is re-written using the equivalenceRewriter. For each predicate in the set modifGoalSet, we check if it is (or its negation) actually an hypothesis of the sequent. If so, we replace it by $\btrue$ (or $\bfalse$). Then, we catch the re-written goal and the hypotheses needed to achieve it.
   • We proceed the same for hypothesis of the map modifHypMap. At the end, all IHypAction are stored in a List.
4. Finally, the proof rule is made. There are 4 cases :
   • the goal is re-written but not the hypotheses : an antecedent is created with no IHypAction, and the IProofRule is made with the needed hypotheses.
   • the goal and hypotheses are re-written : an antecedent is created with the IHypAction computed, and the IProofRule is made with the needed hypotheses.
   • hypotheses are re-written but not the goal : the IProofRule is made with the IHypAction computed.
   • nothing has been re-written : the tactic is no more applicable.

Currently, that implementation has few drawbacks.

• The most important is that the tactic is not deterministic after one execution. It is due to the EquivalenceRewriter. We don't choose exactly where to apply the substitution.
  • So, for the following predicates :
    • $\lnot P_1$
    • $P_1 \limp P_2$
    • $(P_1 \limp P_2) \limp P_1$
  • it can be re-written either as here-below if we first replace $P_1$ in the third predicate :
    • $\lnot P_1$
    • $\bfalse \limp P_2$
    • $(\bfalse \limp P_2) \limp \bfalse$
  • or like this if we first replace $P_1 \limp P_2$ :
    • $\lnot P_1$
    • $\bfalse \limp P_2$
    • $\btrue \limp \bfalse$
• Moreover, when there are multiple negation (e.g. $\lnot\lnot\lnot P$), that tactic does not work well:
  • So, for the following predicates, no replacement will be proceeded :
    • $\lnot\lnot P_1$
    • $P_1$
  • whereas for those one, replacement can be proceeded on the second one :
    • $\lnot\lnot P_1$
    • $\lnot P_1$
  • re-written as following :
    • $\lnot\lnot P_1$
    • $\bfalse$
  • Thus, with those two predicates, there is no re-writing possible.
    • $\overbrace{\lnot ... \lnot}^{n}P$
    • $\overbrace{\lnot ... \lnot}^{n-2}P$
  • Whereas with these two re-writing is possible.
    • $\overbrace{\lnot ... \lnot}^{n}P$
    • $\overbrace{\lnot ... \lnot}^{n-1}P$

That's all folks !