[mizar] Skordev device

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Piotr Rudnicki wrote:

>
> I have never met Dimiter Skordev although I heard of his "device" from you but
> I cannot say that I ever understood its signifcance.

Yes, I was wrong. We discussed a proof in Baby Mizar so it must be rather around
1983, and probably you were already in Canada. The proof discussed:

      (ex x st P[x] implies Q[]) & (ex x st Q[] implies P[x])
           implies ex x st P[x] iff Q[]
     proof
        given x1 such that
G1:    P[x1] implies Q[];
        given x2 such that
G2:    Q[] implies P[x2];
A:       now assume
Z:          Q[];
            take x2;  thus thesis by Z,G2;
          end;
          now assume
Z:         not Q[];
           take x1;  thus thesis by Z,G1;
         end;
       hence thesis by A;
     end;

Prof. Skordev proposed to change the proof to:

      (ex x st P[x] implies Q[]) & (ex x st Q[] implies P[x])
           implies ex x st P[x] iff Q[]
     proof
        given x1 such that
G1:    P[x1] implies Q[];
        given x2 such that
G2:    Q[] implies P[x2];
         Q[] or not Q[];
       hence thesis by G1,G2;
     end;

and, to my surprise, it worked.


The significance:

     for x st P[x] holds Q[x]
     for x st Q[x] holds R[x]
          P[a]
   ----------------------------
          R[a]

is not, as you quite well know, obvious for the CHECKER, but

     for x st P[x] holds Q[x]
     for x st Q[x] holds R[x]
      Q[a] or not Q[a]
          P[a]
   ----------------------------
          R[a]

is: we press the CHECKER to verify two cases and it copes with both. So generating
such disjunctions enables using several universal sentences as the main premise
(different in different cases). Several sentences or the same sentence with
different substitutions (it may cause the undecidability). The heuristic is quite
obvious, we try to find
a common substitution for two atomic sentences in two universal sentences, of course
one of them must occur positively and the other negatively. If such a substitution
exists, the corresponding disjunction is included into premises.
It is not exactly resolution, or rather it is, but using common pattern matching
instead of unification.

I like it because it is easy to control complexity. Let us allow for it only if the
number of generated disjunctions is smaller
than a constant, let's say DisjNbr. Of course if DisjNbr = 10, that CHECKER would be
slower by three orders.
Let us do a very rough estimation:
But if DisjNbr = 1 than proofs (linked steps using simple justification) will be
twice shorter, one step instead of two.
The gain is 50%.
If DisjNbr = 2 then three times shorter, the gain in the comparison to the previous
case is 1/6 of the length
If DisjNbr = 3 - four times shorter, the gain wrt the previous case - 1/12 of the
length.
Because of growing time complexity, I believe that is: 2 or 3.

All the best,
Andrzej