From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 41D4CBCAE for ; Fri, 24 Jun 2005 11:28:35 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j5O9SJ6u023914 for ; Fri, 24 Jun 2005 11:28:20 +0200 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id LAA16554 for ; Fri, 24 Jun 2005 11:28:19 +0200 (MET DST) Received: from hermes.iu-bremen.de (hermes.iu-bremen.de [212.201.44.23]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j5O9SI1f032043 for ; Fri, 24 Jun 2005 11:28:18 +0200 Received: from localhost (demetrius.iu-bremen.de [212.201.44.32]) by hermes.iu-bremen.de (Postfix) with ESMTP id 78F64E8A3; Fri, 24 Jun 2005 11:28:17 +0200 (CEST) Received: from hermes.iu-bremen.de ([212.201.44.23]) by localhost (demetrius [212.201.44.32]) (amavisd-new, port 10024) with ESMTP id 12954-09; Fri, 24 Jun 2005 11:28:15 +0200 (CEST) Received: from [212.201.49.165] (kwarc.faculty.iu-bremen.de [212.201.49.165]) by hermes.iu-bremen.de (Postfix) with ESMTP id B913AD8B1; Fri, 24 Jun 2005 11:28:15 +0200 (CEST) Message-ID: <42BBD22F.5020105@iu-bremen.de> Date: Fri, 24 Jun 2005 11:28:15 +0200 From: Michael Kohlhase Reply-To: m.kohlhase@iu-bremen.de Organization: International University Bremen User-Agent: Mozilla Thunderbird 1.0.2 (X11/20050317) X-Accept-Language: en-us, en MIME-Version: 1.0 To: eapls@jiscmail.ac.uk, asl@vassar.edu, rewriting@ens-lyon.fr, mizar-forum@mizar.uwb.edu.pl, projects-mkm-ig@iu-bremen.de, omdoc@mathweb.org, om-announce@openmath.org, calculemus-ig@ags.uni-sb.de, ftp-community@logic.at, kgs@logic.tuwien.ac.at, theorem-provers@ai.mit.edu, qed@mcs.anl.gov, coq-club@pauillac.inria.fr, compulognet-parimp@dia.fi.upm.es, formal-methods@cs.uidaho.edu, info-hol@cs.uidaho.edu, isabelle-users@cl.cam.ac.uk, mizar-forum@mizar.uwb.edu.pl, pvs@csl.sri.com, acl2@cs.utexas.edu, nqthm-users@cs.utexas.edu, nuprl@cs.cornell.edu, nuprllist@cs.cornell.edu, CADEinc@cs.albany.edu, deducktion@intellektik.informatik.th-darmstadt.de, bra-types@cs.chalmers.se, rewriting@ens-lyon.fr, kgs@logic.tuwien.ac.at, ccl@ps.uni-sb.de, clp@comp.nus.edu.sg, complog@cs.nmsu.edu, comlab@comlab.ox.ac.uk, facs@lboro.ac.uk, kbcsl@uni-paderborn.de, ki-inf@uni-koblenz.de, kr@kr.org, lfcs-interest@dcs.ed.ac.uk, stp@dcs.gla.ac.uk, types@cis.upenn.edu, csp@carlit.toulouse.inra.fr, aiia@di.unito.it, members@fmeurope.org, siksleden@cs.ruu.nl, om@openmath.org, seworld@cs.colorado.edu, SymbolicNet@mcs.kent.edu, vdm-forum@mailbase.ac.uk, wollic@di.ufpe.br, mapledev@maplesoft.com, fom@cs.nyu.edu, caml-list@inria.fr, fg121@sunjessen46.informatik.tu-muenchen.de, ftp@logic.at, ed@mcs.anl.gov, www-math@w3.org, aisb@cogs.sussex.ac.uk, alp@doc.ic.ac.uk, compulog-deduction@cs.bham.ac.uk, dreamers@dai.ed.ac.uk, lprolog@cs.umn.edu, vki-list@dfki.de, zforum@prg.ox.ac.uk Subject: MKM 2005 Program and Final Call for Participation (Early Registration Deadline ends Monday) Content-Type: multipart/mixed; boundary="------------000903090403080302070007" X-Virus-Scanned: by amavisd-new 20030616p5 at demetrius.iu-bremen.de X-Miltered: at concorde with ID 42BBD233.002 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 42BBD232.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; intersection:01 formalized:01 algebra:01 unibo:01 translating:01 granularity:01 matrices:01 modular:01 granularity:01 dominik:01 literate:01 naylor:01 sacerdoti:01 coen:01 algebra:01 X-Attachments: name="MKM_2005_program.txt" name="MKM_2005_program.txt" X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: This is a multi-part message in MIME format. --------------000903090403080302070007 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit [Please post - apologies for multiple copies.] ============================================ MKM 2005 Fourth International Conference on MATHEMATICAL KNOWLEDGE MANAGEMENT http://www.mkm-ig.org/meetings/mkm05/ 15. - 17. July 2005 (Workshop: 14. July) Bremen --- Germany (organized by International University Bremen) FINAL CALL FOR PARTICIPATION Mathematical Knowledge Management is a new field in the intersection of mathematics and computer science. We need new techniques for managing the enormous volume of mathematical knowledge available in current mathematical sources and making it available through the new developments in information technology. A list of topics (to be understood as specialized to the realm of mathematical information) comprises but is not restricted to: Knowledge representation Repositories of formalized mathematics Metadata Deduction systems Data mining Computer Algebra Systems Digital libraries Authoring languages and tools Searching and retrieving Interactive learning Languages of mathematics Web presentation of mathematics Math assistants MathML- and XML-based standards INVITED SPEAKER: Tom Hale (University of Pittsburgh) MKM 2001, http://www.risc.uni-linz.ac.at/institute/conferences/MKM2001/ MKM 2003, http://www.cs.unibo.it/MKM03/ MKM 2004 http://www.mizar.org/MKM2004/ NA-MKM 2002, http://imps.mcmaster.ca/na-mkm-2002/ NA-MKM 2004, http://imps.mcmaster.ca/na-mkm-2004/ To become a member of the MKM Interest group go to the conference or subscribe to the MKM mailing list at http://lists.iu-bremen.de/mailman/admin/projects-mkm-ig -- ------------------------------------------------------------------------- Prof. Dr. Michael Kohlhase, Office: Research 1, Room 62 Professor for Computer Science Campus Ring 12, School of Engineering & Science D-28758 Bremen, Germany International University Bremen tel/fax: +49 421 200-3140/-493140 http://www.faculty.iu-bremen.de/mkohlhase -------------------------------------------------------------------------- _______________________________________________ projects-mkm-ig mailing list projects-mkm-ig@lists.iu-bremen.de http://lists.iu-bremen.de/mailman/listinfo/projects-mkm-ig --------------000903090403080302070007 Content-Type: text/plain; name="MKM_2005_program.txt" Content-Transfer-Encoding: 8bit Content-Disposition: inline; filename="MKM_2005_program.txt" Friday, 15. July 2005 Time Title/Speaker 09:00 - 09:15 Opening 09:15 - 10:15 Session I 9:15 - 9:45 A Proof-Theoretic Approach to Hierarchical Math Library Organization Kamal Aboul-Hosn and Terese Damhoej Andersen 9:45 - 10:15 An Exploration in the Space of Mathematical Knowledge Andrea Kohlhase and Michael Kohlhase 10:15 - 10:45 Coffee Break 10:45 - 12:15 Session II (Authoring) 10:45 - 11:15 Authoring Presentation for OpenMath Shahid Manzoor, Paul Libbrecht, Carsten Ullrich and Erica Melis 11:15 - 11:45 Translating Mathematical Vernacular into Knowledge Repositories Adam Grabowski and Christoph Schwarzweller 11:45 - 12:15 Assisted Proof Document Authoring David Aspinall, Christoph Lüth and Burkhart Wolff 12:15 - 14:00 Lunch 14:00 - 15:30 Session III (Representations) 14:00 - 14:30 A Tough Nut for Mathematical Knowledge Management Manfred Kerber and Martin Pollet 14:30 - 15:00 Textbook Proofs Meet Formal Logic -- The Problem of Underspecification and Granularity Serge Autexier and Armin Fiedler 15:00 - 15:30 Processing Textbook-style Matrices Alan Sexton and Volker Sorge 15:30 - 16:00 Coffee Break 16:00 - 17:30 Session IV (Proving) 16:00 - 16:30 A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity Serge Autexier, Christoph Benzmueller, Dominik Dietrich, Andreas Meier and Claus-Peter Wirth 16:30 - 17:00 Impasse-Driven Reasoning in Proof Planning Andreas Meier and Erica Melis 17:00 - 17:30 Literate proving: presenting and documenting formal proofs Paul Cairns and Jeremy Gow 17:30 - 18:30 MKM business meeting 19:00 - ??:?? Conference Dinner Saturday, 16. July 2005 Time Title/Speaker 09:00 - 10:00 Session V (Invited Talk) 9:15 - 9:45 The Jordan Curve Theorem, from a formal point of view Tom Hales 9:45 - 10:30 Coffee Break 10:30 - 12:30 Session VI (MKManagement Tools) 10:30 - 11:00 Semantic Matching for Mathematical Services William Naylor and Julian Padget 11:00 - 11:30 Organisational Tools for MKM in Theorema Florina Piroi, Bruno Buchberger, Camelia Rosenkranz and Tudor Jebelean 11:30 - 12:00 Mathematical Knowledge Browser with Automatic Hyperlink Detection Koji Nakagawa and Masakazu Suzuki 12:00 - 12:30 A Database of Glyphs for OCR of Mathematical Documents Alan Sexton and Volker Sorge 12:30 - 14:00 Lunch 14:00 - 15:30 Session VII (Documents) 14:00 - 14:30 Toward an Object-Oriented Structure for Mathematical Text Fairouz Kamareddine, Manuel Maarek and J. B Wells 14:30 - 15:00 Explanation in Natural Language of lambda-bar-mu-mu-tilde terms Claudio Sacerdoti Coen 15:00 - 15:30 Towards Consistent Mathematical Documents Achim Mahnke and Jan Scheffczyk 15:30 - 16:00 Coffee Break 16:00 - 17:00 Session VIII (MKM Case studies) 16:00 - 16:30 Computational Origami of a Morley's Triangle Tetsuo Ida, Mircea Marin and Hidekazu Takahashi 16:30 - 17:00 Designing diagrammatic catalogues of types of basic interval equation: A case study Zenon Kulpa 17:00 - 17:30 Gröbner Bases -- Theory Refinement in the Mizar System Christoph Schwarzweller Sunday, 17. July 2005 Time Title/Speaker 09:00 - 10:00 Session IX (Course Materials) 9:00 - 9:30 An Interactive Algebra Course with Formalised Proofs and Definitions Andrea Asperti, Herman Geuvers, Iris Loeb, Lionel Mamane and Claudio Sacerdoti Coen 9:30 - 10:00 Interactive Learning and Mathematical Calculus Arjeh M. Cohen, Hans Cuypers, Dorina Jibetean and Mark Spanbroek 10:00 - 11:00 Coffee Break 11:00 - 12:30 Session X (Migration) 10:30 - 11:00 XML-izing Mizar: making semantic processing and presentation of MML easy Josef Urban 11:00 - 11:30 Determining Empirical Characteristics of Mathematical Expression Use Clare So and Stephen Watt 11:30 - 12:00 Transformations of MML Database's Elements Robert Milewski 12:00 - 12:30 Translating a Fragment of Weak Type Theory into Type Theory with Open Terms Georgi Jojgov 12:15 - 14:00 Lunch --------------000903090403080302070007--