[mizar] Re: Urelements?

[Jesse Alama <jesse.alama@gmail.com>]

One could imagine a checker that has a (static) machine learing
component to it.  Imagine the checker has been trained so that it can
make a good guess, given a proposed inference, whether it is likely
that expansion is needed.  It could be trained on the whole MML.  (In
each release of Mizar one would need to redo the training on the new
MML.)  One could run the checker in either trained (fast, given
suitable background knowledge) or untrained mode (which is the status
quo).

Jesse Alama <jesse.alama@gmail.com> writes:

> I don't know exactly how the checker works, so this may be out of
> line, but here is one simple idea that doesn't even use heuristics.
> One could try a breadth-first approach to expansion: first don't do
> any definitional expansion, and try running the inference through the
> checker.  If that fails, uniformly expand once anything that could be
> expanded, and retry the inference with a bigger premise set.  And so
> forth.  That's how SAD, for example, handles definitions.  This
> preserves the complete/exhaustive property of the checker.  This would
> probably not deliver the big speedups that Artur finds when expansion
> is switched off, but it might help nonetheless.  And with this
> approach, one needn't to introduce a new primitive type.
>
> Jesse
>
> Josef Urban <josef.urban@gmail.com> writes:
>
>> Calling the basic object of set theory an "element" and preventing its
>> automated typing as "set" feels foundationally inventive.
>>
>> It seems that you want additional ad-hoc type/definitional-expansion
>> machinery for some particular sets. I would not do it ad-hoc for two
>> kinds of objects, but rather have a standard mechanism that allows to
>> mark a definition as something that should not be automatically
>> expanded by default (or in an environment). We faced a similar
>> situation some time ago with quaternions, and that had nothing to do
>> with foundations - just with having proper mechanisms for "knowledge
>> expansion".
>>
>> Josef
>>
>> 2012/3/12  <trybulec@math.uwb.edu.pl>:
>>> Let me make one thing clear:
>>>
>>> we do not propose to chang the foundations of MML. The chang eis rather
>>> related to type handling.
>>>
>>> The (quite old/brand new) TARSKI:1 will be
>>>
>>> for x being element holds x is set
>>>
>>>
>>> It now obvious that 2 is a set, I mean
>>>
>>>     2 is set;
>>>
>>> is accepted without any references. In new approach it will need
>>> justification:
>>>
>>>     2 is set by TARSKI:1;
>>>
>>> I used many times (and it must be revised)
>>>
>>>     1-sorted(#1, ... #)
>>>
>>> for 1-element 1-sorted. I even wanted to do a revision :-). With new
>>> approach
>>> one must write
>>>
>>>     1-sorted(#{0}, ...#)
>>>
>>> that means the same and it less tricky.
>>>
>>> Regards,
>>> Andrzej
>>>
>>>
>>>
>>>
>>
>
> --
> Jesse Alama
> http://centria.di.fct.unl.pt/~alama/
>

-- 
Jesse Alama
http://centria.di.fct.unl.pt/~alama/