default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDCICM 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
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 2025-06-27 18:36 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:
