cikm 2017 论文列表

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.

FrameIT Reloaded: Serious Math Games from Modular Math Ontologies.
A Standard for Aligning Mathematical Concepts.
Initial Experiments with Statistical Conjecturing over Large Formal Corpora.
A first step towards automated conjecture-making in higher arithmetic geometry.
Models for Metamath.
The impact of proof steps sequence on proof readability - experimental setting.
Lemma Extraction Criteria Based on Properties of Theorem Statements.
Getting the units right.
A Smooth Transition to Modern mathoid-based Math Rendering in Wikipedia with Automatic Visual Regression Testing.
Formalization of Polynomially Bounded and Negligible Functions Using the Computer-Aided Proof-Checking System Mizar.
swMATH - Challenges, Next Steps, and Outlook.
Design and development of a tool based on Coq to write and format mathematical proofs.
Augmenting Mathematical Formulae for More Effective Querying & Presentation.
Knowledge Management across Formal Libraries.
Automated theorem proving for elementary geometry.
Rigor of TP in Educational Engineering Software.
Lucas-Interpretation from Users' Perspective.
Notation-based Semantification.
KAT: an Annotation Tool for STEM Documents.
Proposal for Coexistence of Mathematical Handwritten and Keyboard Input in a WYSIWYG Expression Editor.
The plain text trap when copying mathematical formulae.
Understanding Mathematical Expressions: An Eye-Tracking Study.
Towards Visual Type Theory as a Mathematical Tool and Mathematical User Interface.
Linking to Compound Conditions in Mizar.
Registrations vs Redefinitions in Mizar.
Topological Foundations for a Formal Theory of Manifolds.
Formalization of the prime number theorem and Dirichlet's theorem.
Tarski's Geometry and the Euclidean Plane in Mizar.
Invited talk: On Differences in Proofs Between Intuitionistic and Classical Logic.
Invited talk: Developments, Libraries and Automated Theorem Provers.