[mizar] clusters of predicates

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi,

there are now some 1000 predicates in MML (depending on what you count 
exactly), and it seems to me that there is now both a good occasion and 
good reason(s) to implement some more automation for them.

By the good occasion I mean the recent reimplementation of the cluster 
mechanisms, which seem to work nicely, and already now allow attributes 
with hidden arguments to be clustered. The implementation for predicates 
could be very similar, e.g.

registration 
 let T be TopStruct, A,B be Subset of T;
 cluster A,B are_separated -> A misses B;
 coherence by CONNSP_1:2;
end;

The reasons are
1. Such predicate hierarchies seem quite natural, both in mathematics and 
   in natural language. If our position is that the automations in Mizar 
   are designed to capture the "implicit knowledge" (background, context, 
   or however we call that) that the system should use at some point 
   without being explicitly mentioned, we should allow facts like
   CONNSP_1:2 to be automated.

2. Already now, there are predicate redefinitions, but they only allow 
   much weaker automations. On the other hand, the strong mechanisms used 
   for attributes could eventually lead to "smuggling" of the attributes 
   even to places, where they (at least linguistically or esthetically) do 
   not belong.

3. As noted, the implementation could be quite cheap.



Josef