<!-- 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="Distributed Assertion Retrieval"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#title"> <META NAME="DC.Creator" CONTENT="Christoph Benzmueller"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#creator"> <META NAME="DC.Creator.2" CONTENT="Andreas Meier"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#creator"> <META NAME="DC.Creator.3" CONTENT="Volker Sorge"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#creator"> <META NAME="DC.Subject" CONTENT="Mathematical Knowledge Management"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#subject"> <META NAME="DC.Subject" CONTENT="Data Retrieval"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#subject"> <META NAME="DC.Subject" CONTENT="Blackboard Architecture"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#subject"> <META NAME="DC.Description" CONTENT="We suggest a technique to separate the search for applicable assertions in theorem proving from the main proving process and to supersede database dependencies by general search criterions. Our approach, which employs the O-ANTS blackboard mechanism, serves for both automated and interactive theorem proving. The idea is to view the applicability tests as little independent and resource bounded processes that run in parallel in the background."> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#description"> <META NAME="DC.Date" SCHEME="ISO8601" CONTENT="2001-09-24"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#date"> <META NAME="DC.Type" CONTENT="Text.Article"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#type"> <META NAME="DC.Format" SCHEME="IMT" CONTENT="application/pdf"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#format"> <LINK REL=SCHEMA.imt HREF="http://sunsite.auc.dk/RFC/rfc/rfc2046.html"> <META NAME="DC.Format" SCHEME="IMT" CONTENT="application/postscript"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#format"> <LINK REL=SCHEMA.imt HREF="http://sunsite.auc.dk/RFC/rfc/rfc2046.html"> <META NAME="DC.Format.X-Carrier" CONTENT="printed material"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#format"> <META NAME="DC.Identifier" SCHEME="URL" CONTENT="http://www.risc.uni-linz.ac.at/conferences/MKM2001/Proceedings%20"> <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="EULER.Event.Location" CONTENT="A-4232 Schloss Hagenberg "> <LINK REL=SCHEMA.dc HREF="http://www.lub.lu.se/EULER/partners/april99-metadatacreator.html"> <META NAME="EULER.Event.Date" SCHEME="ISO8601" CONTENT="2001-09-24"> <LINK REL=SCHEMA.dc HREF="http://www.lub.lu.se/EULER/partners/april99-metadatacreator.html"> <META NAME="EULER.Event.Name" CONTENT="MKM 2001, First International Workshop on Mathematical Knowledge Management"> <LINK REL=SCHEMA.dc HREF="http://www.lub.lu.se/EULER/partners/april99-metadatacreator.html"> <META NAME="DC.Date.X-MetadataLastModified" SCHEME="ISO8601" CONTENT="2001-10-26"> <LINK REL=SCHEMA.dc HREF="http://purl.org/metadata/dublin_core_elements#date">