Re: [mizar] instance checking procedure

[Michael Nedzelsky <MichaelNedzelsky@yandex.ru>]

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?

Regards,
  Michael Nedzelsky