Re: [mizar] instance checking procedure

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

On Fri, 10 Feb 2006, Michael Nedzelsky wrote:

> On Wed, 8 Feb 2006 10:20 pm, Josef Urban wrote:
> > Hi,
> >
> > I am forwarding here Bill McCune's pointers to an interesting instance (or
> > rather entailment) checking procedure that seems to be in some sense
> > stronger than the current Mizar checker (more exactly, its part called
> > "Unifier"). It seems to me that the treatment of existential
> > variables is "done right" there. Champeaux's article is online at
> > http://portal.acm.org/citation.cfm?doid=6490.6491 , the procedure is
> > called INSTANCE there.
>
> It seems that this article is available only for subscribers (or you must
> purchase it). Is it possible get it for free?

Ooops, seems we have IP-based subscription there. The MoMM page 
of certain unnamed wiki might however be sufficient :-).

Josef