


default search action
CICM 2020: Bertinoro, Italy
- Christoph Benzmüller

, Bruce R. Miller
:
Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings. Lecture Notes in Computer Science 12236, Springer 2020, ISBN 978-3-030-53517-9
Invited Talks
- Christian Szegedy:

A Promising Path Towards Autoformalization and General Artificial Intelligence. 3-20
Full Papers
- Reynald Affeldt

, Jacques Garrigue
, Takafumi Saikawa
:
Formal Adventures in Convex and Conical Spaces. 23-38 - Katja Bercic

, Michael Kohlhase
, Florian Rabe
:
Towards a Heterogeneous Query Language for Mathematical Knowledge. 39-54 - Jacques Carette, William M. Farmer, Yasmine Sharoda:

Leveraging the Information Contained in Theory Presentations. 55-70 - Mario Carneiro

:
Metamath Zero: Designing a Theorem Prover Prover. 71-88 - Ciarán Dunne

, J. B. Wells, Fairouz Kamareddine:
Adding an Abstraction Barrier to ZF Set Theory. 89-104 - Yassmeen Elderhalli, Osman Hasan

, Sofiène Tahar:
A Framework for Formal Dynamic Dependability Analysis Using HOL Theorem Proving. 105-122 - Márton Hajdú, Petra Hozzová, Laura Kovács

, Johannes Schoisswohl, Andrei Voronkov:
Induction with Generalization in Superposition Reasoning. 123-137 - Cezary Kaliszyk

, Florian Rabe
:
A Survey of Languages for Formalizing Mathematics. 138-156 - Alexander Kirillovich

, Olga Nevzorova
, Marina V. Falileeva
, Evgeny K. Lipachev
, Liliana R. Shakirova
:
OntoMathEdu: A Linguistically Grounded Educational Mathematical Ontology. 157-172 - Michael Kohlhase

, Benjamin Bösl, Richard Marcus
, Dennis Müller
, Denis Rochau, Navid Roux
, John Schihada
, Marc Stamminger:
FrameIT: Detangling Knowledge Management from Game Design in Serious Games. 173-189 - Laura Kovács

, Hanna Lachnitt, Stefan Szeider
:
Formalizing Graph Trail Properties in Isabelle/HOL. 190-205 - Dennis Müller

, Florian Rabe
, Colin Rothgang
, Michael Kohlhase
:
Representing Structural Language Features in Formal Meta-languages. 206-221 - Leonard Schmitz

, Viktor Levandovskyy:
Formally Verifying Proofs for Algebraic Identities of Matrices. 222-236 - Moritz Schubotz, Philipp Scharpf, Olaf Teschke

, Andreas Kühnemund, Corinna Breitinger, Bela Gipp
:
AutoMSC: Automatic Assignment of Mathematics Subject Classification Labels. 237-250 - Floris van Doorn

, Gabriel Ebner
, Robert Y. Lewis
:
Maintaining a Library of Formal Mathematics. 251-267
System Descriptions and Datasets
- Lasse Blaauwbroek, Josef Urban, Herman Geuvers:

The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq. 271-277 - Thibault Gauthier:

Tree Neural Networks in HOL4. 278-283 - Adrian De Lon, Peter Koepke, Anton Lorenzen:

Interpreting Mathematical Texts in Naproche-SAD. 284-289 - Richard Marcus

, Michael Kohlhase
, Florian Rabe
:
TGView3D: A System for 3-Dimensional Visualization of Theory Graphs. 290-296 - Yutaka Nagashima

:
Simple Dataset for Proof Method Recommendation in Isabelle/HOL. 297-302 - Adam Naumowicz

:
Dataset Description: Formalization of Elementary Number Theory in Mizar. 303-308 - Bartosz Piotrowski, Josef Urban:

Guiding Inferences in Connection Tableau by Recurrent Neural Networks. 309-314 - Josef Urban, Jan Jakubuv:

First Neural Conjecturing Datasets and Experiments. 315-323 - Abdou Youssef, Bruce R. Miller:

A Contextual and Labeled Math-Dataset Derived from NIST's DLMF. 324-330

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














