Re: [mizar] weak types

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

Freek,

Freek Wiedijk wrote:

>
> I would like to experiment with a Mizar-like system where the
> rules of the logic are such that you will get extra proof
> obligations (like PVS' TCCs) that guarantee that the meaning
> of a function "outside its domain of well-definedness" will
> never matter.
>
> To give the foundations for such a system was the goal of my
> paper with Jan Zwanenburg at TPHOLs this year.
>
> As an example of what such a system would look like:
> If you would have a proof with a step
>
>         ...
>         A1: sqrt x > a by ...;
>         ...
>
> then the justification would not only have to justify the
> statement itself, but also the "assumptions of the functors"
> (in this case "x >= 0").

Sorry, I did not read the paper, but if you could answer one question:

Does it means, that the system generates the sentence
             x >= 0 & sqrt x > a

We experimented with something similar in seventies. Then for

   not sqrt x > a

we generated

    x >=0 implies not sqrt x > a

So we called it '& / implies' approach. General rule if the sentence
occurs positively the system generates
the conjunction ( 'guard & sentence' ), if negatively then implication (
'guard implies sentence' ). If I recall
Piotr, maybe you remember better?

Even if the implementation was easy, the results were discouraging -
nobody knew how the sentence looks like.
Particularly if you have a complicated formula and there is a lot of
guards and one should know if the sentence is negative or positive -
what about antonyms? And how to cope with the definitional expansion?

Andrzej