Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDCICM 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
a service of 
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.
last updated on 2023-06-07 21:55 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
