You must enable JavaScript to use this site
  • Programme Overview (tentative, subject to change)

    Detailed schedule by day: Monday, Tuesday , Wednesday , Thursday, Friday.

    25. July
    26. July
    27. July
    28. July
    29. July
    9:00FM4M Invited Talk: [F1]
    Chad Brown. Invited talk: Developments, Libraries and Automated Theorem Provers (Slides)

    Chair: Naumowicz
    C. Sacerdoti Coen
    Claudio Sacerdoti Coen. Towards Extensible Algorithmic Mathematical Knowledge (Slides)

    Chair: Kohlhase
    John Harrison
    John Harrison. TBA

    Chair: Brown
    Nicolas Thiery
    Nicolas Thierry. Infrastructure for generic code in SageMath: categories, axioms, constructions (Slides)

    Chair: Sacerdoti Coen
    9:00-11:00: Language Design in MMT
    Florian Rabe, Mihnea Iancu, Dennis Müller. Language Design in MMT (Slides)
    10:30Doctoral Program
    Marek Janasz. Automated theorem proving for elementary geometry
    Dennis Müller. Knowledge Management across Formal Libraries
    Moritz Schubotz. Augmenting Mathematical Formulae for More Effective Querying & Presentation (Slides)
    Théo Zimmermann. Design and development of a tool based on Coq to write and format mathematical proofs
    Lucius Schoenbaum. Towards Visual Type Theory as Mathematical Tool and Mathematical User Interface
    Andrea Kohlhase and Michael Fürsich. Understanding Mathematical Expressions: An Eye-Tracking Study
    Adam Grabowski. Tarski's geometry and Euclidean plane in Mizar
    Mario Carneiro. Formalization of the prime number theorem and Dirichlet's theorem (Slides)
    Karol Pąk. Topological Foundations for a Formal Theory of Manifolds
    Adam Naumowicz and Radosław Piliszek. Accessing the Mizar Library with a Weakly Strict Mizar Parser
    Chad Brown and Josef Urban. Extracting Higher-Order Goals from the Mizar Mathematical Library (Slides)
    Karol Pąk. Lemma Extraction Criteria Based on Properties of Theorem Statements
    Karol Pąk and Aleksy Schubert. The impact of proof steps sequence on proof readability – experimental setting
    Chair: Farmer
    Projects & Surveys
    Paul-Olivier Dehaye, Mihnea Iancu, Michael Kohlhase, Alexander Konovalov, Samuel Lelièvre, Dennis Müller, Markus Pfeiffer, Florian Rabe, Nicolas M. Thiéry and Tom Wiesing. Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach
    Waqar Ahmed, Osman Hasan and Sofiene Tahar. Formal Dependability Modeling and Analysis: A Survey (Slides)
    Chair: Ion
    Alexander Maletzky. Mathematical Theory Exploration in Theorema: Reduction Rings
    Ken'Ichi Kuga, Manabu Hagiwara and Mitsuharu Yamamoto. Formalization of Bing's shrinking method in geometric topology
    Erika Ábrahám, Bernd Becker, James H. Davenport and Pascal Fontaine. SC-square: Satisfiability Checking meets Symbolic Computation
    Muhammad Qasim, Osman Hasan, Maissa Elleuch and Sofiene Tahar. Formalization of Normal Random Variables in HOL (Slides)
    Chair: Naumowicz
    Mizar HandsOn Tutorial
    9:00-11:00: Language Design in MMT
    Florian Rabe, Mihnea Iancu, Dennis Müller. Language Design in MMT (Slides)
    11:00-12:30: Application Design with MMT
    Florian Rabe, Mihnea Iancu, Dennis Müller. Application Design with MMT (Slides)
    11:30Systems & Data
    Jan Jakubuv and Josef Urban. Extending E Prover with Similarity Based Clause Selection Strategies
    Artur Kornilowicz. Enhancement of Mizar Texts with Transitivity Property of Predicates
    Chair: Ion
    Agenda, Standards Discussion
    Michael Kohlhase. The 29th OpenMath Workshop, Agenda/Planning
    Tom Wiesing. An Overview over SCSCP
    Paul Libbrecht and Matija Lokar. The plain text trap when copying mathematical formulae
    Juan Lao-Tebar, Francisco Alvaro and Daniel Marqus. Proposal for Coexistence of Mathematical Handwritten and Keyboard Input in a WYSIWYG Expression Editor
    Invited Talk: [F6]
    Aleksy Schubert. Invited talk: On Differences in Proofs Between Intuitionistic and Classical Logic

    Walther Neuper. Lucas-Interpretation from Users’ Perspective (Slides)
    William Farmer. Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics (Slides)
    Mario Carneiro. Models for Metamath (Slides)
    Andreas Holmstrom. A first step towards automated conjecture-making in higher arithmetic geometry
    Chair: Rabe
    Olaf Teschke and Fabian Müller. Progress of self-archiving within the DML corpus, with a view toward community dynamics
    Wolfram Sperber, Hagen Chrapary and Wolfgang Dalitz. swMATH - challenges, next steps, and outlook (Slides)
    Hiroyuki Okazaki and Yuichi Futa. Formalization of Polynomially Bounded and Negligible Functions using the Computer-Aided Proof-Checking System Mizar
    Chair: Davenport
    Mizar HandsOn Tutorial
    Bruce Miller. Drafting DLMF Content Dictionaries
    Michael Kohlhase. Towards OpenMath 2.1 or 3; Issues and Criteria
    Michael Kohlhase. Sequence Variables in OpenMath
    Tom Wiesing and Felix Schmoll. KAT: an Annotation Tool for STEM Documents
    Ion Toloaca and Michael Kohlhase. Notation-based Semantification
    Walther Neuper. Rigor of TP in Educational Engineering Software (Slides)
    Artur Korniłowicz. Registrations vs Redefinitions in Mizar
    Adam Naumowicz. Linking to Compound Conditions in Mizar
    Thibault Gauthier, Cezary Kaliszyk and Josef Urban. Initial Experiments with Statistical Conjecturing over Large Formal Corpora
    Cezary Kaliszyk, Michael Kohlhase, Dennis Müller and Florian Rabe. A Standard for Aligning Mathematical Concepts
    Denis Rochau, Michael Kohlhase and Dennis Müller. FrameIT Reloaded: Serious Math Games from Modular Math Ontologies
    Chair: Urban
    Moritz Schubotz, David Veenhuis and Howard Cohl. Getting the units right (Slides)
    Moritz Schubotz and Alan Sexton. A Smooth Transition to Modern mathoid-based Math Rendering in Wikipedia with Automatic Visual Regression Testing (Slides)
    Chair: Sorge
    Mizar HandsOn Tutorial
    17:30General MeetingTrack Meetings?Business Meeting
    CICM Invited TalkCALCULEMUSDigital Mathematical Libraries (DML)Doctoral ProgramFormal Mathematics for Mathematicians (FM4M)TutorialMathematical Knowledge Management (MKM)MathUIProjects & SurveysSystems & DataTetrapodTheorem Provers Components for Educational Software (ThEdu)
  • News

Last modified: December 19 2016 18:05:35 CET