<!-- For best results, you should include the HTML-coded --> <!-- metadata that you find further down the page --> <!-- (below the line) in the <HEAD></HEAD>-tag of your --> <!-- page. This will simplify correct indexing by robots. --> <!-- ---------------------------------------------------- --> <META NAME="DC.Title" CONTENT="Mathematical Knowledge Management in Mizar"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#title"> <META NAME="DC.Creator" CONTENT="Andrzej Trybulec"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#creator"> <META NAME="DC.Creator.2" CONTENT="Piotr Rudnicki"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#creator"> <META NAME="DC.Subject" CONTENT="formalization of mathematics"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#subject"> <META NAME="DC.Subject" CONTENT="proof-checking"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#subject"> <META NAME="DC.Subject" CONTENT="Mizar system"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#subject"> <META NAME="DC.Type" CONTENT="Text.Proceedings"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#type"> <META NAME="DC.Identifier" SCHEME="URL" CONTENT="http://www.risc.uni-linz.ac.at/conferences/MKM2001/Proceedings"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#identifier"> <META NAME="DC.Language" SCHEME="ISO639-1" CONTENT="en"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#language"> <META NAME="DC.Date.X-MetadataLastModified" SCHEME="ISO8601" CONTENT="2001-10-25"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#date">