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

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

    Monday
    25. July
    Tuesday
    26. July
    Wednesday
    27. July
    Thursday
    28. July
    Friday
    29. July
    8:30RegistrationRegistrationRegistrationRegistrationRegistration
    Room20482001AulaAulaAulaAula2001Aula2048
    9:00FM4M Invited Talk: [F1]
    Chad Brown. Invited talk: Developments, Libraries and Automated Theorem Provers (Slides)

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

    Chair: Kohlhase
    John Harrison
    [I1]
    John Harrison. TBA

    Chair: Brown
    Nicolas Thiery
    [I3]
    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:00CoffeeCoffeeCoffeeCoffeeCoffee
    10:30Doctoral Program
    [DP1]
    Marek Janasz. Automated theorem proving for elementary geometry
    [DP2]
    Dennis Müller. Knowledge Management across Formal Libraries
    [DP3]
    Moritz Schubotz. Augmenting Mathematical Formulae for More Effective Querying & Presentation (Slides)
    [DP4]
    Théo Zimmermann. Design and development of a tool based on Coq to write and format mathematical proofs
    MathUI
    [M1]
    Lucius Schoenbaum. Towards Visual Type Theory as Mathematical Tool and Mathematical User Interface
    [M2]
    Andrea Kohlhase and Michael Fürsich. Understanding Mathematical Expressions: An Eye-Tracking Study
    FM4M
    [F2]
    Adam Grabowski. Tarski's geometry and Euclidean plane in Mizar
    [F3]
    Mario Carneiro. Formalization of the prime number theorem and Dirichlet's theorem (Slides)
    [F4]
    Karol Pąk. Topological Foundations for a Formal Theory of Manifolds
    MKM
    [R5]
    Adam Naumowicz and Radosław Piliszek. Accessing the Mizar Library with a Weakly Strict Mizar Parser
    [R19]
    Chad Brown and Josef Urban. Extracting Higher-Order Goals from the Mizar Mathematical Library (Slides)
    [W33]
    Karol Pąk. Lemma Extraction Criteria Based on Properties of Theorem Statements
    [W47]
    Karol Pąk and Aleksy Schubert. The impact of proof steps sequence on proof readability – experimental setting
    Chair: Farmer
    Projects & Surveys
    [R21]
    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
    [R39]
    Waqar Ahmed, Osman Hasan and Sofiene Tahar. Formal Dependability Modeling and Analysis: A Survey (Slides)
    Chair: Ion
    CALCULEMUS
    [R4]
    Alexander Maletzky. Mathematical Theory Exploration in Theorema: Reduction Rings
    [R11]
    Ken'Ichi Kuga, Manabu Hagiwara and Mitsuharu Yamamoto. Formalization of Bing's shrinking method in geometric topology
    [R31]
    Erika Ábrahám, Bernd Becker, James H. Davenport and Pascal Fontaine. SC-square: Satisfiability Checking meets Symbolic Computation
    [R36]
    Muhammad Qasim, Osman Hasan, Maissa Elleuch and Sofiene Tahar. Formalization of Normal Random Variables in HOL (Slides)
    Chair: Naumowicz
    OpenMath
    Mizar HandsOn Tutorial
    MMT
    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
    [R18]
    Jan Jakubuv and Josef Urban. Extending E Prover with Similarity Based Clause Selection Strategies
    [R42]
    Artur Kornilowicz. Enhancement of Mizar Texts with Transitivity Property of Predicates
    Chair: Ion
    12:30LunchLunchLunchLunchLunch
    14:00OpenMath
    Agenda, Standards Discussion
    [O0]
    Michael Kohlhase. The 29th OpenMath Workshop, Agenda/Planning
    [O1]
    Tom Wiesing. An Overview over SCSCP
    MathUI
    [M3]
    Paul Libbrecht and Matija Lokar. The plain text trap when copying mathematical formulae
    [M4]
    Juan Lao-Tebar, Francisco Alvaro and Daniel Marqus. Proposal for Coexistence of Mathematical Handwritten and Keyboard Input in a WYSIWYG Expression Editor
    FM4M/ThEdu
    Invited Talk: [F6]
    Aleksy Schubert. Invited talk: On Differences in Proofs Between Intuitionistic and Classical Logic

    [T1]
    Walther Neuper. Lucas-Interpretation from Users’ Perspective (Slides)
    MKM
    [R8]
    William Farmer. Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics (Slides)
    [W1]
    Mario Carneiro. Models for Metamath (Slides)
    [W44]
    Andreas Holmstrom. A first step towards automated conjecture-making in higher arithmetic geometry
    Chair: Rabe
    DML
    [R32]
    Olaf Teschke and Fabian Müller. Progress of self-archiving within the DML corpus, with a view toward community dynamics
    [W10]
    Wolfram Sperber, Hagen Chrapary and Wolfgang Dalitz. swMATH - challenges, next steps, and outlook (Slides)
    [W38]
    Hiroyuki Okazaki and Yuichi Futa. Formalization of Polynomially Bounded and Negligible Functions using the Computer-Aided Proof-Checking System Mizar
    Chair: Davenport
    Tetrapod
    Mizar HandsOn Tutorial
    15:30CoffeeCoffeeCoffeeCoffee
    16:00OpenMath
    [O2]
    Bruce Miller. Drafting DLMF Content Dictionaries
    [O3][O4][O5]
    Michael Kohlhase. Towards OpenMath 2.1 or 3; Issues and Criteria
    [O6]
    Michael Kohlhase. Sequence Variables in OpenMath
    MathUI
    [M5]
    Tom Wiesing and Felix Schmoll. KAT: an Annotation Tool for STEM Documents
    [M6]
    Ion Toloaca and Michael Kohlhase. Notation-based Semantification
    FM4M/ThEdu
    [T2]
    Walther Neuper. Rigor of TP in Educational Engineering Software (Slides)
    [F5]
    Artur Korniłowicz. Registrations vs Redefinitions in Mizar
    [F7]
    Adam Naumowicz. Linking to Compound Conditions in Mizar
    MKM
    [W23]
    Thibault Gauthier, Cezary Kaliszyk and Josef Urban. Initial Experiments with Statistical Conjecturing over Large Formal Corpora
    [W24]
    Cezary Kaliszyk, Michael Kohlhase, Dennis Müller and Florian Rabe. A Standard for Aligning Mathematical Concepts
    [W50]
    Denis Rochau, Michael Kohlhase and Dennis Müller. FrameIT Reloaded: Serious Math Games from Modular Math Ontologies
    Chair: Urban
    DML
    [W45]
    Moritz Schubotz, David Veenhuis and Howard Cohl. Getting the units right (Slides)
    [W48]
    Moritz Schubotz and Alan Sexton. A Smooth Transition to Modern mathoid-based Math Rendering in Wikipedia with Automatic Visual Regression Testing (Slides)
    Chair: Sorge
    Tetrapod
    Mizar HandsOn Tutorial
    17:30General MeetingTrack Meetings?Business Meeting
    19:00
    LegendFree
    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