List of Events

Invited Talks

• [I1] Yannis Haralambous. Text Mining Methods Applied to Mathematical Texts (Slides) (Tuesday, 9:00-10:00, Lecture Hall, Research III)
• [I2] Conor McBride. A Prospection for Reflection (Thursday, 9:00-10:00, Lecture Hall, Research III)
• [I3] Cezar Ionescu. Increasingly correct scientific programming (Slides) (Friday, 9:00-10:00, Lecture Hall, Research III)
• [M12] Michael Trott. Mathematical Search (Sunday, 14:00-15:30, Lecture Hall, Research III)

Regular papers

• [R1] Czeslaw Bylinski and Jesse Alama. New developments in parsing Mizar (DOI) (Thursday, 15:30-17:00, Room 50, Research III)
• [R2] Jónathan Heras, María Poza and Julio Rubio. Verifying an algorithm computing Discrete Vector Fields for digital imaging (Slides) (DOI) (Thursday, 10:30-11:00, Lecture Hall, Research III)
• [R3] Stefan Hetzl. Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP) (DOI) (Tuesday, 16:00-18:00, Room 50, Research III)
• [R4] Kevin Kofler and Arnold Neumaier. DynGenPar - A Dynamic Generalized Parser for Common Mathematical Language (DOI) (Monday, 10:30-11:00, Lecture Hall, Research III)
• [R5] Andrea Asperti. Proof, message and certification (Slides) (DOI) (Tuesday, 14:00-14:30, Lecture Hall, Research III)
• [R6] Filip Maric, Miodrag Zivkovic and Bojan Vuckovic. Formalizing Frankl's Conjecture: FC-families (Slides) (DOI) (Thursday, 14:30 - 15:00, Lecture Hall, Research III)
• [R7] Mladen Nikolic and Predrag Janicic. CDCL-Based Abstract State Transition System for Coherent Logic (Slides) (DOI) (Thursday, 11:00-11:30, Lecture Hall, Research III)
• [R8] Paul Libbrecht, Sandra Rebholz, Daniel Herding, Wolfgang Müller and Felix Tscheulin. Understanding the Learners' Actions when using Mathematics Learning Tools (Slides) (DOI) (Tuesday, 14:30-15:00, Lecture Hall, Research III)
• [R9] Michael Kohlhase. The Planetary Project: Towards eMath3.0 (DOI) (Tuesday, 16:00-18:00, Room 50, Research III)
• [R10] Jacques Carette and Russell O'Connor. Theory Expression Combinators (Slides) (DOI) (Thursday, 11:30-12:00, Lecture Hall, Research III)
• [R11] Makarius Wenzel. Isabelle/jEdit -- a Prover IDE within the PIDE framework (DOI) (Thursday, 15:30-17:00, Room 50, Research III)
• [R12] Artur Kornilowicz. Tentative Experiments with Ellipsis in Mizar (DOI) (Tuesday, 16:00-18:00, Room 50, Research III)
• [R13] Timothy Bourke, Matthias Daum, Gerwin Klein and Rafal Kolanski. Challenges and Experiences in Managing Large-Scale Proofs (Slides) (DOI) (Monday, 14:00-14:30, Lecture Hall, Research III)
• [R14] Mnacho Echenim and Nicolas Peltier. Reasoning on Schemata of Formulae (DOI) (Friday, 14:00-14:30, Lecture Hall, Research III)
• [R15] Muhammad Taimoor Khan and Wolfgang Schreiner. On Formal Specification of Maple Programs (DOI) (Thursday, 15:30-17:00, Room 50, Research III)
• [R16] Muhammad Taimoor Khan and Wolfgang Schreiner. Towards Formal Specification and Verification of Maple Programs (Slides) (DOI) (Friday, 11:00-11:30, Lecture Hall, Research III)
• [R17] Catalin David, Constantin Jucovschi, Andrea Kohlhase and Michael Kohlhase. Semantic Alliance: A Framework for Semantic Allies (DOI) (Monday, 15:00-15:30, Lecture Hall, Research III)
• [R18] Andrea Asperti and Wilmer Ricciotti. A Web Interface for Matita (Slides) (DOI) (Tuesday, 16:00-18:00, Room 50, Research III)
• [R19] Carst Tankink, Christoph Lange and Josef Urban. Point-and-write -- Documenting Formal Mathematics by Reference (Slides) (DOI) (Monday, 17:00-17:30, Lecture Hall, Research III)
• [R20] Vadim Mazalov and Stephen Watt (presented by Rui Hu). Writing on Clouds (DOI) (Monday, 11:00-11:30, Lecture Hall, Research III)
• [R21] Constantin Jucovschi. Cost-Effective Integration of MKM Semantic Services into Editing Environments (Slides) (DOI) (Tuesday, 12:00-12:30, Lecture Hall, Research III)
• [R22] Iain Whiteside, David Aspinall and Gudmund Grov. An Essence of SSReflect (DOI) (Tuesday, 10:30-11:00, Lecture Hall, Research III)
• [R23] Fulya Horozal, Michael Kohlhase and Florian Rabe. Extending MKM Formats at the Statement Level (Slides) (DOI) (Monday, 16:00-16:30, Lecture Hall, Research III)
• [R24] David Wilson, Russell Bradford and James Davenport. Speeding-up Cylindrical Algebraic Decomposition by Gröbner Bases (Slides) (DOI) (Friday, 10:30-11:00, Lecture Hall, Research III)
• [R25] Vesna Marinkovic and Predrag Janicic. Towards Understanding Triangle Construction Problems (Slides) (DOI) (Tuesday, 15:00-15:30, Lecture Hall, Research III)
• [R26] Christoph Lange, Patrick Ion, Anastasia Dimou, Charalampos Bratsas, Joseph Corneli, Wolfram Sperber, Michael Kohlhase and Ioannis Antoniou. Reimplementing the Mathematics Subject Classification (MSC) as a Linked Open Dataset (Poster) (DOI) (Tuesday, 16:00-18:00, Room 50, Research III)
• [R27] Christoph Lange, Oliver Kutz, Till Mossakowski and Michael Grüninger. The Distributed Ontology Language (DOL): Ontology Integration and Interoperability Applied to Mathematical Formalization (Poster) (DOI) (Tuesday, 16:00-18:00, Room 50, Research III)
• [R28] Mihnea Iancu and Florian Rabe. Management of Change in Declarative Languages (Slides) (DOI) (Friday, 16:30-17:00, Lecture Hall, Research III)
• [R29] Grant Passmore, Lawrence Paulson and Leonardo De Moura. Real Algebraic Strategies for MetiTarski Proofs (Slides) (DOI) (Friday, 14:30-15:00, Lecture Hall, Research III)
• [R30] Florian Rabe. A Query Language for Formal Mathematical Libraries (Slides) (DOI) (Tuesday, 11:00-11:30, Lecture Hall, Research III)
• [R31] Rui Hu, Vadim Mazalov and Stephen Watt. A Streaming Digital Ink Framework for Multi-Party Collaboration (DOI) (Monday, 16:30-17:00, Lecture Hall, Research III)
• [R32] Alan Sexton. Abramowitz and Stegun -- A Resource for Mathematical Document Analysis (DOI) (Tuesday, 11:30-12:00, Lecture Hall, Research III)
• [R33] Gabriel Dos Reis. A System for Axiomatic Programming (DOI) (Friday, 16:00-16:30, Lecture Hall, Research III)
• [R34] Josef Baker, Alan Sexton and Volker Sorge. Maxtract: Converting PDF to LATEX, MathML and Text (DOI) (Tuesday, 16:00-18:00, Room 50, Research III)
• [R35] Phil Scott and Jacques Fleuriot. A Combinator Language for Theorem Discovery (DOI) (Friday, 17:00-17:30, Lecture Hall, Research III)
• [R36] Jesse Alama, Lionel Mamane and Josef Urban. Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar (Slides) (DOI) (Monday, 14:30-15:00, Lecture Hall, Research III)
• [R37] Michael Kohlhase and Corneliu-Claudiu Prodescu. MathWebSearch 0.5 Scaling an Open Formula Search Engine (Slides) (DOI) (Friday, 15:00-15:30, Lecture Hall, Research III)
• [R38] Xiaoyu Chen, Wei Li, Jie Luo and Dongming Wang. Open Geometry Textbook: A Case Study of Knowledge Acquisition via Collective Intelligence (DOI) (Tuesday, 16:00-18:00, Room 50, Research III)
• [M2] Tsuyoshi Murata and Kenichi Otagiri. Searching and Ranking Mathematical Formulas (Sunday, 17:12-17:32, Lecture Hall, Research III)
• [M3] Giovanni Yoko Kristianto, Minh-Quoc Nghiem, Nobuo Inui, Goran Topic and Akiko Aizawa. Annotating Mathematical Expression Definitions for Automatic Detection (Sunday, 16:20-16:40, Lecture Hall, Research III)
• [M4] Magdalena Wolska. Building a POS-annotated Corpus of Scientific Papers in Mathematics (Sunday, 16:00-16:20, Lecture Hall, Research III)
• [M5] Michael Kohlhase and Mihnea Iancu. Searching Induced Formulae; Get Out More Than You Put In! (Slides) (Sunday, 9:25-9:50, Lecture Hall, Research III)
• [M6] Mohamed Ali Ibrahim Alkalai and Volker Sorge. Issues in Mathematical Table Recognition (Sunday, 16:40-17:00, Lecture Hall, Research III)
• [M8] Martin Líška, Petr Sojka and Michal Růžička. Latest Development of MIaS, Math Indexer and Searcher (Slides) (Sunday, 9:50-10:10, Lecture Hall, Research III)
• [M10] Moritz Schubotz. Using LaTeXML and MathWeb Search to Make Enable Mathematical Search in MediaWiki (Sunday, 10:10-10:30, Lecture Hall, Research III)
• [M13] Petr Sojka. MIR.fi.muni.cz: Past, Present and Future (Slides) (Sunday, 9:00-9:25, Lecture Hall, Research III)

Work in progress

• [WIP1] Pedro Quaresma. A XML-Format for Conjectures in Geometry (Slides) (Monday, 17:30-17:45, Lecture Hall, Research III)
• [WIP2] Joseph Corneli and Mircea Alexandru Dumitru. PlanetMath/Planetary (Monday, 17:45-18:00, Lecture Hall, Research III)
• [WIP3] Wolfgang Windsteiger. Theorema 2.0: A Graphical User Interface for a Mathematical Assistant System (Thursday, 15:30 - 17:00, Room 50, Research III)
• [WIP4] Radim Hatlapatka. JBIG2 Supported by OCR (Slides) (Monday, 9:20-9:40, Lecture Hall, Research III)
• [WIP5] David Formánek, Martin Líška, Michal Růžička and Petr Sojka. Normalization of Digital Mathematics Library Content (Monday, 9:40-10:00, Lecture Hall, Research III)

Panel Discussions, Teaser Talks, Special Addresses, etc.

• [C1] Stephen Wolfram. Special Address (Video) (Wednesday, 19:00-20:00, Campus Center/IRC, Library, 5th Floor)
• [Teasers1] Teaser talks for posters/demos R12, R3, R18, R38, R26, R9, R27, and R34 (Tuesday, 15:30-15:50, Lecture Hall, Research III)
• [Teasers2] Teaser talks for posters/demos R1, R11, R15, WIP3 in the next session (Thursday, 15:00 - 15:15, Lecture Hall, Research III)
• [P1] Jiří Rákosník (DML-CZ, EuDML), Patrick Ion (Mathematical Reviews), Alan Sexton (University of Birmingham), Wolfram Sperber (Zentralblatt Math), possibly others (to be confirmed). Towards World DML: Are We on the Right Track? (Monday, 11:30-12:30, Lecture Hall, Research III)

  Abstract:There are continuation efforts ongoing with the dream of WDML in mind: EuDML, recent Washington meeting, projects granted by Sloan, etc. However, these are not coordinated, some views how to proceed differ. Some decisions have already been done in ongoing projects like EuDML, and were discussed at DML panel last year. It is time now to stop for a while, and raise questions whether do we do well and ask for feedback from the community. So, are we on right track as far as a) business model (which strategies, methods, partners); b) digital infrastructures and tools and c) sustainability of WDML services and `librarianship' curation is concerned?

Overview Talks

• [M1] Michael Kohlhase and Petr Sojka. MIR wrap-up and overview (Slides) (Monday, 9:05-9:20, Lecture Hall, Research III)
• [M7] Akiko Aizawa, Michael Kohlhase and Iadh Ounis. An Overview of NTCIR-10 Math Pilot Task (Sunday, 17:32-17:50, Lecture Hall, Research III)
• [M9] Wolfram Siegmund Sperber. A Short Report about Information services of Zentralblatt Math (Sunday, 17:00-17:12, Lecture Hall, Research III)
• [M11] All. General MIR Discussion (Sunday, 17:50-18:00, Lecture Hall, Research III)

Workshop Mathematical User Interfaces (MathUI)

• [MUI1] Hans Cuypers and Jan Willem Knopper. MathDox Select: A tool for creating SCORM packages from existing exercises (Wednesday, 14:00-14:30, West Hall 1)
• [MUI2] Andrea Kohlhase. Navigation in Mathematical Documents (Wednesday, 14:30-15:00, West Hall 1)
• [MUI3] Paul Libbrecht. Skills Text Box A Tool to Access Resources by Mathematical Concepts (Wednesday, 15:00-15:30, West Hall 1)

OpenMath Workshop

• [OM0] Welcome and general discussion (Wednesday, 10:30-10:45, West Hall 1)
• [OM1] Ken Wenzel and Heiner Reinhardt. Mathematical Computations for Linked Data Applications with OpenMath (Wednesday, 10:45-11:15, West Hall 1)
• [OM2] Olga Caprotti and Jordi Saludes. The Gf Mathematical Grammar Library (Wednesday, 11:15-11:45, West Hall 1)
• [OM3] OpenMath Society Business Meeting (open to all workshop participants) (Wednesday, 11:45-12:30, West Hall 1)

Workshop User Interfaces in Theorem Proving (UITP)

• [uitp1] Wolfgang Windsteiger. Theorema 2.0: A Graphical User Interface for a Mathematical Assistant System (Wednesday, 9:00-9:30, West Hall 2)
• [uitp2] Makarius Wenzel. READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking (Wednesday, 10:30-11:00, West Hall 2)
• [uitp3] Mikheil Rukhaia, Cvetan Dunchev, Alexander Leitsch, Tomer Libal, Martin Riener, Daniel Weller and Bruno Woltzenlogel Paleo. ProofTool: GUI for the GAPT Framework (Wednesday, 9:30-10:00, West Hall 2)
• [uitp4] Vincent Rahli. Interfacing with Proof Assistants for Domain Specific Programming Using EventML (Wednesday, 11:00-11:30, West Hall 2)
• [uitp5] Andrei Lapets, Richard Skowyra, Christine Bassem, Assaf Kfoury and Azer Bestavros. Towards an Infrastructure for Integrated Accessible Formal Reasoning Environments (Wednesday, 11:30-12:00, West Hall 2)
• [uitp7] Mihnea Iancu and Florian Rabe. An MMT-Based User-Interface (Wednesday, 12:00-12:30, West Hall 2)

Doctoral Programme

• [DP2] Randa Almomen. Semantic Understanding of Mathematical Formulae in Documents (Wednesday, 16:30-17:00, West Hall 2)
• [DP3] Fulya Horozal. Representing Declarative Languages and their Translations (Wednesday, 15:00-15:30, West Hall 2)
• [DP4] Rui Hu. Pen-Based Collaboration Tools for Mathematics (Wednesday, 14:00-14:30, West Hall 2)
• [DP5] Alin Iacob. Knowledge Management Integration in Computer-Aided Design (Wednesday, 14:30-15:00, West Hall 2)
• [DP6] Moritz Schubotz. Content based Formula Search (Wednesday, 16:00-16:30, West Hall 2)
• [DP7] David Wilson. Real Geometry and Connectedness via Triangular Descriptions (Wednesday, 17:00-17:30, West Hall 2)

Business Meetings

• [B1] Calculemus Business meeting (Slides) (Friday, 11:30-12:30, Lecture Hall, Research III)
• [B2] MKM Business meeting (Slides) (Monday, 18:30-19:00, Lecture Hall, Research III)
• [B3] CICM Business meeting (Slides) (Thursday, 17:00-18:00, Room 50, Research III)
• [B4] DML Business meeting (Monday, 18:00-18:30, Lecture Hall, Research III)

Social Events

• [S1] Bremen Old City Centre Tour (Tuesday, 18:15 -- 19:45)
• [S2] Conference Dinner at "Kaffee Mühle" (Tuesday, 20:00 -- )
• [S3] Excursion (Thursday, 18:00 -- 19:45)
• [S4] Conference Dinner at "Zur Gläsernen Werft" (Thursday, 20:00 -- )