Re: Re: Urelements?

On Mon, Mar 12, 2012 at 7:14 PM, Jesse Alama <[email protected]> wrote:
> 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).

Thanks for the machine learning propaganda :-). I think AI belongs to
proof finding (and we have it there with ATPs), not to proof checking.

best,
Josef


>
> Jesse Alama <[email protected]> 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 <[email protected]> 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  <[email protected]>:
>>>> 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/