![](https://dblp1.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp1.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp1.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
default search action
14th CICM 2021: Timisoara, Romania
- Fairouz Kamareddine, Claudio Sacerdoti Coen
:
Intelligent Computer Mathematics - 14th International Conference, CICM 2021, Timisoara, Romania, July 26-31, 2021, Proceedings. Lecture Notes in Computer Science 12833, Springer 2021, ISBN 978-3-030-81096-2
Formalizations
- Chelsea Edmonds
, Lawrence C. Paulson
:
A Modular First Formalisation of Combinatorial Design Theory. 3-18 - Adrian De Lon
, Peter Koepke
, Anton Lorenzen
, Adrian Marti
, Marcel Schütz
, Erik Sturzenhecker:
Beautiful Formalizations in Isabelle/Naproche. 19-31 - Asta Halkjær From
, Agnes Moesgård Eschen, Jørgen Villadsen
:
Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL. 32-46 - Mohamed Abdelghany, Sofiène Tahar:
Formalization of RBD-Based Cause Consequence Analysis in HOL. 47-64
Automatic Theorem Proving and Machine Learning
- Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban:
Online Machine Learning Techniques for Coq: A Comparison. 67-83 - Krsto Prorokovic, Michael Wand, Jürgen Schmidhuber:
Improving Stateful Premise Selection with Transformers. 84-89 - Ruocheng Shan, Abdou Youssef:
Towards Math Terms Disambiguation Using Machine Learning. 90-106 - Edvard K. Holden
, Konstantin Korovin
:
Heterogeneous Heuristic Optimisation and Scheduling for First-Order Theorem Proving. 107-123 - Márton Hajdú
, Petra Hozzová
, Laura Kovács
, Johannes Schoisswohl
, Andrei Voronkov:
Inductive Benchmarks for Automated Reasoning. 124-129 - Tudor Jebelean:
A Heuristic Prover for Elementary Analysis in Theorema. 130-134
Search and Classification
- Yujin Song
, Xiaoyu Chen
:
Searching for Mathematical Formulas Based on Graph Representation Learning. 137-152 - Susanne Arndt, Patrick Ion, Mila Runnwerth, Moritz Schubotz, Olaf Teschke
:
10 Years Later: The Mathematics Subject Classification and Linked Open Data. 153-158 - Dávid Lupták
, Vít Novotný
, Michal Stefánik
, Petr Sojka
:
WebMIaS on Docker - Deploying Math-Aware Search in a Single Line of Code. 159-164
Teaching and Geometric Reasoning
- Jaroslav Macke
, Jirí Sedlár
, Miroslav Olsák
, Josef Urban
, Josef Sivic
:
Learning to Solve Geometric Construction Problems from Images. 167-184 - Petra Hozzová
, Laura Kovács
, Jakob Rath
:
Automated Generation of Exam Sheets for Automated Deduction. 185-196 - Abdullah Khan
, Alexei Lisitsa
, Alexei Vernitski
:
Gauss-Lintel, an Algorithm Suite for Exploring Chord Diagrams. 197-202
Logic and Systems
- Colin Rothgang
, Artur Kornilowicz
, Florian Rabe
:
A New Export of the Mizar Mathematical Library. 205-210 - Florian Rabe
:
A Language with Type-Dependent Equality. 211-227 - Ciarán Dunne
, J. B. Wells, Fairouz Kamareddine:
Generating Custom Set Theories with Non-set Structured Objects. 228-244 - Martin Líska, Dávid Lupták, Vít Novotný, Michal Ruzicka
, Boris Shminke, Petr Sojka
, Michal Stefánik
, Makarius Wenzel:
CICM'21 Systems Entries. 245-248
![](https://dblp1.uni-trier.de/img/cog.dark.24x24.png)
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.