Schedule per day| Sunday | |
| 9:00-10:00 | Chair: Akiko Aizawa, Lecture Hall, Research III MIR systems introductions | | 10:00-10:30 | Coffee | | 10:30-12:30 | Chair: Michael Kohlhase, Lecture Hall, Research III MIR Happening (formulae search, document search and open search categories) | | 12:30-14:00 | Lunch | | 14:00-15:30 | Chair: Petr Sojka, Lecture Hall, Research III- (Invited Talk) Michael Trott. Mathematical Search (14:00-15:30)
MIR Invited videolecture | | 15:30-16:00 | Coffee | | 16:00-18:00 | Chair: Bruce Miller, Lecture Hall, Research III MIR Workshop papers II and other announcements, discussions, demos, position papers | | |
| Monday | |
| 9:00-10:00 | Chair: Jiří Rákosník, Lecture Hall, Research III | | 10:00-10:30 | Coffee | | 10:30-12:30 | Chair: Petr Sojka, Lecture Hall, Research III- Kevin Kofler and Arnold Neumaier. DynGenPar - A Dynamic Generalized Parser for Common Mathematical Language (10:30-11:00) (DOI)
- Vadim Mazalov and Stephen Watt (presented by Rui Hu). Writing on Clouds (11:00-11:30) (DOI)
- 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? (11:30-12:30)
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?
| | 12:30-14:00 | Lunch | | 14:00-15:30 | Chair: Christoph Lüth, Lecture Hall, Research III- Timothy Bourke, Matthias Daum, Gerwin Klein and Rafal Kolanski. Challenges and Experiences in Managing Large-Scale Proofs (14:00-14:30) (Slides) (DOI)
- Jesse Alama, Lionel Mamane and Josef Urban. Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar (14:30-15:00) (Slides) (DOI)
- Catalin David, Constantin Jucovschi, Andrea Kohlhase and Michael Kohlhase. Semantic Alliance: A Framework for Semantic Allies (15:00-15:30) (DOI)
| | 15:30-16:00 | Coffee | | 16:00-18:00 | Chair: Alan Sexton, Lecture Hall, Research III | | Lecture Hall, Research III- DML Business meeting (18:00-18:30)
- MKM Business meeting (18:30-19:00) (Slides)
|
| Tuesday | |
| 9:00-10:00 | Chair: Petr Sojka, Lecture Hall, Research III- (Invited Talk) Yannis Haralambous. Text Mining Methods Applied to Mathematical Texts (9:00-10:00) (Slides)
| | 10:00-10:30 | Coffee | | 10:30-12:30 | Chair: Andrea Asperti, Lecture Hall, Research III | | 12:30-14:00 | Lunch | | 14:00-15:30 | Chair: David Aspinall, Lecture Hall, Research III | | 15:30-16:00 | Chair: Volker Sorge, Lecture Hall, Research III- Teaser talks for posters/demos R12, R3, R18, R38, R26, R9, R27, and R34 (15:30-15:50)
Coffee | | 16:00-18:00 | Chair: Volker Sorge, Room 50, Research III- Artur Kornilowicz. Tentative Experiments with Ellipsis in Mizar (DOI)
- Stefan Hetzl. Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP) (DOI)
- Andrea Asperti and Wilmer Ricciotti. A Web Interface for Matita (Slides) (DOI)
- Xiaoyu Chen, Wei Li, Jie Luo and Dongming Wang. Open Geometry Textbook: A Case Study of Knowledge Acquisition via Collective Intelligence (DOI)
- 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)
- Michael Kohlhase. The Planetary Project: Towards eMath3.0 (DOI)
- 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)
- Josef Baker, Alan Sexton and Volker Sorge. Maxtract: Converting PDF to LATEX, MathML and Text (DOI)
| | |
| Wednesday | |
| 9:00-10:00 | UITP WorkshopChair: Cezary Kaliszyk, West Hall 2 | Unrelated | | 10:00-10:30 | UnrelatedCoffee | UnrelatedCoffee | | 10:30-12:30 | UITP WorkshopChair: Christoph Lüth, West Hall 2 | OpenMath WorkshopWest Hall 1 | | 12:30-14:00 | Lunch | | 14:00-15:30 | Doctoral ProgrammeChair: Serge Autexier, West Hall 2- Rui Hu. Pen-Based Collaboration Tools for Mathematics (14:00-14:30)
- Alin Iacob. Knowledge Management Integration in Computer-Aided Design (14:30-15:00)
- Fulya Horozal. Representing Declarative Languages and their Translations (15:00-15:30)
| MathUI WorkshopChair: Paul Libbrecht, West Hall 1 | | 15:30-16:00 | UnrelatedCoffee | UnrelatedCoffee | | 16:00-18:00 | Doctoral ProgrammeChair: Serge Autexier, West Hall 2- Moritz Schubotz. Content based Formula Search (16:00-16:30)
- Randa Almomen. Semantic Understanding of Mathematical Formulae in Documents (16:30-17:00)
- David Wilson. Real Geometry and Connectedness via Triangular Descriptions (17:00-17:30)
| Unrelated | | this conferenceChair: Michael Kohlhase, Campus Center/IRC, Library, 5th Floor- Stephen Wolfram. Special Address (19:00-20:00) (Video)
| this conferenceChair: Michael Kohlhase, Campus Center/IRC, Library, 5th Floor- Stephen Wolfram. Special Address (19:00-20:00) (Video)
|
| Thursday | |
| 9:00-10:00 | Chair: Johan Jeuring, Lecture Hall, Research III- (Invited Talk) Conor McBride. A Prospection for Reflection
| | 10:00-10:30 | Coffee | | 10:30-12:30 | Chair: James Davenport, Lecture Hall, Research III | | 12:30-14:00 | Lunch | | 14:00-15:30 | Chair: Gabriel Dos Reis, Lecture Hall, Research III | | 15:30-16:00 | Coffee | | 16:00-18:00 | Chair: Christoph Lange, Room 50, Research III | | |
| Friday | |
| 9:00-10:00 | Chair: Johan Jeuring, Lecture Hall, Research III- (Invited Talk) Cezar Ionescu. Increasingly correct scientific programming (Slides)
| | 10:00-10:30 | Coffee | | 10:30-12:30 | Chair: Makarius Wenzel, Lecture Hall, Research III | | 12:30-14:00 | Lunch | | 14:00-15:30 | Chair: Jacques Carette, Lecture Hall, Research III- Mnacho Echenim and Nicolas Peltier. Reasoning on Schemata of Formulae (14:00-14:30) (DOI)
- Grant Passmore, Lawrence Paulson and Leonardo De Moura. Real Algebraic Strategies for MetiTarski Proofs (14:30-15:00) (Slides) (DOI)
- Michael Kohlhase and Corneliu-Claudiu Prodescu. MathWebSearch 0.5 Scaling an Open Formula Search Engine (15:00-15:30) (Slides) (DOI)
| | 15:30-16:00 | Coffee | | 16:00-18:00 | Chair: John Campbell, Lecture Hall, Research III- Gabriel Dos Reis. A System for Axiomatic Programming (16:00-16:30) (DOI)
- Mihnea Iancu and Florian Rabe. Management of Change in Declarative Languages (16:30-17:00) (Slides) (DOI)
- Phil Scott and Jacques Fleuriot. A Combinator Language for Theorem Discovery (17:00-17:30) (DOI)
End of CICM 2012 | | |
|
