M(ost|uch) of M(izar|ath) Matches (MoMM)


  • The treatment of existential variables is a bit hacked now. Bill McCune? has pointed to Champeaux's procedure (the paper attached here), however it requires (anti)skolemization for each pair of tested formulas, so I'll have to think how to do efficient indexing (possibly cheaply in E) for this. The procedure however seems directly usable instead of the Mizar Unifier (see AndrzejTrybulec?'s description of that at http://www.cs.ru.nl/~freek/mizar/by.ps.gz).
-- JosefUrban - 07 Jan 2005

TopicClassification MizarTools

ImplementationDate? N/A
Topic attachments
I Attachment Action Size Date Who Comment
pdfpdf Champeaux.pdf manage 1748.0 K 2006-02-10 - 09:09 JosefUrban Champeaux's paper
Topic revision: r7 - 2008-05-12 - 12:52:52 - JosefUrban
Mizar TWiki
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback