![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
CICM 2015: Washington, DC, USA
- Manfred Kerber, Jacques Carette
, Cezary Kaliszyk
, Florian Rabe, Volker Sorge:
Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings. Lecture Notes in Computer Science 9150, Springer 2015, ISBN 978-3-319-20614-1
Invited Talks
- Jasmin Christian Blanchette, Max W. Haslbeck
, Daniel Matichuk, Tobias Nipkow
:
Mining the Archive of Formal Proofs. 3-17 - Richard Zanibbi
, Awelemdy Orakwue:
Math Search for the Masses: Multimodal Search Interfaces and Appearance-Based Retrieval. 18-36
Calculemus
- Waqar Ahmad, Osman Hasan
:
Towards Formal Fault Tree Analysis Using Theorem Proving. 39-54 - Luís Cruz-Filipe
, Peter Schneider-Kamp
:
Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof. 55-70 - Evgenii Kotelnikov, Laura Kovács
, Andrei Voronkov:
A First Class Boolean Sort in First-Order Theorem Proving and TPTP. 71-86 - Steven Obua, Jacques D. Fleuriot
, Phil Scott, David Aspinall:
Type Inference for ZFH. 87-101 - Florian Rabe
:
Generic Literals. 102-117 - Paul Tarau:
Ranking/Unranking of Lambda Terms with Compressed de Bruijn Indices. 118-133
Digital Mathematics Libraries
- Mihnea Iancu, Michael Kohlhase
:
A Flexiformal Model of Knowledge Dissemination and Aggregation in Mathematics. 137-152
Mathematical Knowledge Management
- Serge Autexier
, Dieter Hutter
:
Structure Formation in Large Theories. 155-170 - Feryal Fulya Horozal, Florian Rabe
:
Formal Logic Definitions for Interchange Languages. 171-186 - Mihnea Iancu, Michael Kohlhase
:
Math Literate Knowledge Management via Induced Material. 187-202 - Bruce R. Miller:
Strategies for Parallel Markup. 203-210 - Karol Pak
:
Readable Formalization of Euler's Partition Theorem in Mizar. 211-226 - Daniel Raggi, Alan Bundy, Gudmund Grov, Alison Pease
:
Automating Change of Representation for Proofs in Discrete Mathematics. 227-242 - Qun Zhang, Abdou Youssef:
Performance Evaluation and Optimization of Math-Similarity Search. 243-257
Projects and Surveys
- Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski
, Artur Kornilowicz
, Roman Matuszewski, Adam Naumowicz
, Karol Pak
, Josef Urban:
Mizar: State-of-the-art and Beyond. 261-279 - Howard S. Cohl
, Moritz Schubotz
, Marjorie A. McClain, Bonita V. Saunders, Cherry Y. Zou, Azeem S. Mohammed, Alex A. Danoff:
Growing the Digital Repository of Mathematical Formulae with Generic Sources. 280-287 - Cezary Kaliszyk
, Josef Urban, Umair Siddique
, Sanaz Khan Afshar, Cvetan Dunchev, Sofiène Tahar:
Formalizing Physics: Automation, Presentation and Foundation Issues. 288-295 - Ferruccio Guidi
, Claudio Sacerdoti Coen
:
A Survey on Retrieval of Mathematical Knowledge. 296-315 - Umair Siddique
, Osman Hasan
, Sofiène Tahar:
Towards the Formalization of Fractional Calculus in Higher-Order Logic. 316-324 - Max Wisniewski, Alexander Steen
, Christoph Benzmüller
:
LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners. 325-330
Systems and Data
- Koen Claessen, Moa Johansson, Dan Rosén, Nicholas Smallbone:
TIP: Tons of Inductive Problems. 333-337 - Ross Moore
:
Semantic Enrichment of Mathematics via 'tooltips'. 338-342 - Kazuhisa Nakasho, Yasunari Shidama:
Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library. 343-347 - Adam Naumowicz
:
Tools for MML Environment Analysis. 348-352 - Ons Seddiki, Cvetan Dunchev, Sanaz Khan Afshar, Sofiène Tahar:
Enabling Symbolic and Numerical Computations in HOL Light. 353-358
![](https://dblp.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.