Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics (CICM 2016), Bialystok, Poland, July 25-29, 2016
Andrea Kohlhase, Paul Libbrecht, Bruce R. Miller, Adam Naumowicz, Walther Neuper, Pedro Quaresma, Frank Wm. Tompa, Martin Suda (Editors)
- Anthology ID:
- 2016.cikm_workshop-2016fm4m
- Year:
- 2016
- Venue:
- cikm_workshop
- Publisher:
- CEUR-WS.org
- URL:
- https://ceur-ws.org/Vol-1785
- DBLP:
- conf/cikm/2016fm4m
Invited talk: Developments, Libraries and Automated Theorem Provers
Chad Brown
Invited talk: On Differences in Proofs Between Intuitionistic and Classical Logic
Aleksy Schubert
Tarski's Geometry and the Euclidean Plane in Mizar
Adam Grabowski
|
Roland Coghetto
Formalization of the prime number theorem and Dirichlet's theorem
Mario Carneiro
Topological Foundations for a Formal Theory of Manifolds
Karol Pak
Registrations vs Redefinitions in Mizar
Artur Kornilowicz
Linking to Compound Conditions in Mizar
Adam Naumowicz
Towards Visual Type Theory as a Mathematical Tool and Mathematical User Interface
Lucius Schoenbaum
Understanding Mathematical Expressions: An Eye-Tracking Study
Andrea Kohlhase
|
Michael Fürsich
The plain text trap when copying mathematical formulae
Paul Libbrecht
|
Matija Lokar
Proposal for Coexistence of Mathematical Handwritten and Keyboard Input in a WYSIWYG Expression Editor
Juan Lao-Tebar
|
Francisco Alvaro
|
Daniel Marques
KAT: an Annotation Tool for STEM Documents
Tom Wiesing
|
Felix Schmoll
Notation-based Semantification
Ion Toloaca
|
Michael Kohlhase
Lucas-Interpretation from Users' Perspective
Walther Neuper
Rigor of TP in Educational Engineering Software
Walther Neuper
Automated theorem proving for elementary geometry
Marek Janasz
Knowledge Management across Formal Libraries
Dennis Müller
Augmenting Mathematical Formulae for More Effective Querying & Presentation
Moritz Schubotz
Design and development of a tool based on Coq to write and format mathematical proofs
Théo Zimmermann
swMATH - Challenges, Next Steps, and Outlook
Hagen Chrapary
|
Wolfgang Dalitz
|
Wolfram Sperber
Formalization of Polynomially Bounded and Negligible Functions Using the Computer-Aided Proof-Checking System Mizar
Hiroyuki Okazaki
|
Yuichi Futa
A Smooth Transition to Modern mathoid-based Math Rendering in Wikipedia with Automatic Visual Regression Testing
Moritz Schubotz
|
Alan P. Sexton
Getting the units right
Moritz Schubotz
|
David Veenhuis
|
Howard S. Cohl
Lemma Extraction Criteria Based on Properties of Theorem Statements
Karol Pak
The impact of proof steps sequence on proof readability - experimental setting
Karol Pak
|
Aleksy Schubert
Models for Metamath
Mario Carneiro
A first step towards automated conjecture-making in higher arithmetic geometry
Andreas Holmstrom
Initial Experiments with Statistical Conjecturing over Large Formal Corpora
Thibault Gauthier
|
Cezary Kaliszyk
|
Josef Urban
A Standard for Aligning Mathematical Concepts
Cezary Kaliszyk
|
Michael Kohlhase
|
Dennis Müller
|
Florian Rabe
FrameIT Reloaded: Serious Math Games from Modular Math Ontologies
Denis Rochau
|
Michael Kohlhase
|
Dennis Müller