Muutke küpsiste eelistusi

Intelligent Computer Mathematics: International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings. 2015 ed. [Pehme köide]

Edited by , Edited by , Edited by , Edited by , Edited by
  • Formaat: Paperback / softback, 359 pages, kõrgus x laius: 235x155 mm, kaal: 5796 g, 84 Illustrations, black and white; XXI, 359 p. 84 illus., 1 Paperback / softback
  • Sari: Lecture Notes in Computer Science 9150
  • Ilmumisaeg: 29-Jun-2015
  • Kirjastus: Springer International Publishing AG
  • ISBN-10: 3319206141
  • ISBN-13: 9783319206141
  • Pehme köide
  • Hind: 48,70 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Tavahind: 57,29 €
  • Säästad 15%
  • Raamatu kohalejõudmiseks kirjastusest kulub orienteeruvalt 2-4 nädalat
  • Kogus:
  • Lisa ostukorvi
  • Tasuta tarne
  • Tellimisaeg 2-4 nädalat
  • Lisa soovinimekirja
  • Formaat: Paperback / softback, 359 pages, kõrgus x laius: 235x155 mm, kaal: 5796 g, 84 Illustrations, black and white; XXI, 359 p. 84 illus., 1 Paperback / softback
  • Sari: Lecture Notes in Computer Science 9150
  • Ilmumisaeg: 29-Jun-2015
  • Kirjastus: Springer International Publishing AG
  • ISBN-10: 3319206141
  • ISBN-13: 9783319206141
This book constitutes the refereed proceedings of the International Conference on Intelligent Computer Mathematics, CICM 2015, held in Washington, DC, USA, in July 2015. The 16 full papers and 9 short papers presented together with two invited talks plus one abstract were carefully reviewed and selected from a total of 43 submissions. The papers are organized in topical sections following the tracks of the conference: Invited Talks; Calculemus; Digital Mathematics Libraries; Mathematical Knowledge Management; Projects and Surveys; Systems and Data.
Invited Talks
Mining the Archive of Formal Proofs
3(15)
Jasmin Christian Blanchette
Maximilian Haslbeck
Daniel Matichuk
Tobias Nipkow
Math Search for the Masses: Multimodal Search Interfaces and Appearance-Based Retrieval
18(21)
Richard Zanibbi
Awelemdy Orakwue
Calculemus
Towards Formal Fault Tree Analysis Using Theorem Proving
39(16)
Waqar Ahmed
Osman Hasan
Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
55(16)
Luis Cruz-Filipe
Peter Schneider-Kamp
A First Class Boolean Sort in First-Order Theorem Proving and TPTP
71(16)
Evgenii Kotelnikov
Laura Kovacs
Andrei Voronkov
Type Inference for ZFH
87(15)
Steven Obua
Jacques Fleuriot
Phil Scott
David Aspinall
Generic Literals
102(16)
Florian Rabe
Ranking/Unranking of Lambda Terms with Compressed de Bruijn Indices
118(19)
Paul Tarau
Digital Mathematics Libraries
A Flexiformal Model of Knowledge Dissemination and Aggregation in Mathematics
137(18)
Mihnea Iancu
Michael Kohlhase
Mathematical Knowledge Management
Structure Formation in Large Theories
155(16)
Serge Autexier
Dieter Hutter
Formal Logic Definitions for Interchange Languages
171(16)
Fulya Horozal
Florian Rabe
Math Literate Knowledge Management via Induced Material
187(16)
Mihnea Iancu
Michael Kohlhase
Strategies for Parallel Markup
203(8)
Bruce R. Miller
Readable Formalization of Euler's Partition Theorem in Mizar
211(16)
Karol Pak
Automating Change of Representation for Proofs in Discrete Mathematics
227(16)
Daniel Raggi
Alan Bundy
Gudmund Grov
Alison Pease
Performance Evaluation and Optimization of Math-Similarity Search
243(18)
Qun Zhang
Abdou Youssef
Projects and Surveys
Mizar: State-of-the-Art and Beyond
261(19)
Grzegorz Bancerek
Czeslaw Bylinski
Adam Grabowski
Artur Kornilowicz
Roman Matuszewski
Adam Naumowicz
Karol Pak
Josef Urban
Growing the Digital Repository of Mathematical Formulae with Generic LATEX Sources
280(8)
Howard S. Cohl
Moritz Schubotz
Marjorie A. McClain
Bonita V. Saunders
Cherry Y. Zou
Azeem S. Mohammed
Alex A. Danoff
Formalizing Physics: Automation, Presentation and Foundation Issues
288(8)
Cezary Kaliszyk
Josef Urban
Umair Siddique
Sanaz Khan-Afshar
Cvetan Dunchev
Sofiene Tahar
A Survey on Retrieval of Mathematical Knowledge
296(20)
Ferruccio Guidi
Claudio Sacerdoti Coen
Towards the Formalization of Fractional Calculus in Higher-Order Logic
316(9)
Umair Siddique
Osman Hasan
Sofiene Tahar
LeoPARD --- A Generic Platform for the Implementation of Higher-Order Reasoners
325(8)
Max Wisniewski
Alexander Steen
Christoph Benzmuller
Systems and Data
TIP: Tons of Inductive Problems
333(5)
Koen Claessen
Moa Johansson
Dan Rosen
Nicholas Smallbone
Semantic Enrichment of Mathematics via `tooltips'
338(5)
Ross Moore
Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
343(5)
Kazuhisa Nakasho
Yasunari Shidama
Tools for MML Environment Analysis
348(5)
Adam Naumowicz
Enabling Symbolic and Numerical Computations in HOL Light
353(6)
Ons Seddiki
Cvetan Dunchev
Sanaz Khan-Afshar
Sofiene Tahar
Author Index 359