Intelligent computer mathematics. 11th international conference, AISC 2012, 19th symposium, Calculemus 2012, 5th international workshop, DML 2012, 11th international conference, MKM 2012, systems and projects, held as part of CICM 2012, Bremen, Germany, July 8–13, 2012. Proceedings. (English) Zbl 1245.68013

Lecture Notes in Computer Science 7362. Lecture Notes in Artificial Intelligence. Berlin: Springer (ISBN 978-3-642-31373-8/pbk). xviii, 473 p. (2012).

Show indexed articles as search result.

The articles of this volume will be reviewed individually. For AISC 2010 see [Zbl 1194.68011]; for Calculemus 2011 and MKM 2011 see [Zbl 1218.68014].
Indexed articles:
Alama, Jesse; Mamane, Lionel; Urban, Josef, Dependencies in formal mathematics: applications and extraction for Coq and Mizar, 1-16 [Zbl 1335.68221]
Asperti, Andrea, Proof, message and certificate, 17-31 [Zbl 1359.68245]
Bourke, Timothy; Daum, Matthias; Klein, Gerwin; Kolanski, Rafal, Challenges and experiences in managing large-scale proofs, 32-48 [Zbl 1359.68264]
David, Catalin; Jucovschi, Constantin; Kohlhase, Andrea; Kohlhase, Michael, Semantic alliance: a framework for semantic allies, 49-64 [Zbl 1278.68298]
Horozal, Fulya; Kohlhase, Michael; Rabe, Florian, Extending MKM formats at the statement level, 65-80 [Zbl 1278.68293]
Hu, Rui; Mazalov, Vadim; Watt, Stephen M., A streaming digital ink framework for multi-party collaboration, 81-95 [Zbl 1359.68284]
Jucovschi, Constantin, Cost-effective integration of MKM semantic services into editing environments, 96-110 [Zbl 1359.68285]
Libbrecht, Paul; Rebholz, Sandra; Herding, Daniel; Müller, Wolfgang; Tscheulin, Felix, Understanding the learners’ actions when using mathematics learning tools, 111-126 [Zbl 1359.97006]
Marinković, Vesna; Janičić, Predrag, Towards understanding triangle construction problems, 127-142 [Zbl 1359.68265]
Rabe, Florian, A query language for formal mathematical libraries, 143-158 [Zbl 1359.68272]
Sexton, Alan P., Abramowitz and Stegun – a resource for mathematical document analysis, 159-168 [Zbl 1360.68823]
Tankink, Carst; Lange, Christoph; Urban, Josef, Point-and-write – documenting formal mathematics by reference, 169-185 [Zbl 1360.68824]
Whiteside, Iain; Aspinall, David; Grov, Gudmund, An essence of SSReflect, 186-201 [Zbl 1360.68770]
Carette, Jacques; O’Connor, Russell, Theory presentation combinators, 202-215 [Zbl 1360.68802]
Heras, Jónathan; Poza, María; Rubio, Julio, Verifying an algorithm computing discrete vector fields for digital imaging, 216-230 [Zbl 1360.68880]
Khan, Muhammad Taimoor; Schreiner, Wolfgang, Towards the formal specification and verification of Maple programs, 231-247 [Zbl 1360.68590]
Marić, Filip; Živković, Miodrag; Vučković, Bojan, Formalizing Frankl’s conjecture: FC-families, 248-263 [Zbl 1360.68758]
Nikolić, Mladen; Janičić, Predrag, CDCL-based abstract state transition system for coherent logic, 264-279 [Zbl 1360.68761]
Wilson, David J.; Bradford, Russell J.; Davenport, James H., Speeding up cylindrical algebraic decomposition by Gröbner bases, 280-294 [Zbl 1360.68959]
Dos Reis, Gabriel, A system for axiomatic programming, 295-309 [Zbl 1360.68360]
Echenim, Mnacho; Peltier, Nicolas, Reasoning on schemata of formulæ, 310-325 [Zbl 1360.68746]
Iancu, Mihnea; Rabe, Florian, Management of change in declarative languages, 326-341 [Zbl 1360.68809]
Kohlhase, Michael; Matican, Bogdan A.; Prodescu, Corneliu-Claudiu, MathWebSearch 0.5: scaling an open formula search engine, 342-357 [Zbl 1278.68296]
Passmore, Grant Olney; Paulson, Lawrence C.; de Moura, Leonardo, Real algebraic strategies for MetiTarski proofs, 358-370 [Zbl 1360.68764]
Scott, Phil; Fleuriot, Jacques, A combinator language for theorem discovery, 371-385 [Zbl 1360.68766]
Kofler, Kevin; Neumaier, Arnold, DynGenPar – a dynamic generalized parser for common mathematical language, 386-401 [Zbl 1360.68812]
Mazalov, Vadim; Watt, Stephen M., Writing on clouds, 402-416 [Zbl 1360.68736]
Asperti, Andrea; Ricciotti, Wilmer, A web interface for Matita, 417-421 [Zbl 1360.68739]
Baker, Josef B.; Sexton, Alan P.; Sorge, Volker, MaxTract: converting PDF to LaTeX, MathML and text, 422-426 [Zbl 1360.68882]
Bylinski, Czesław; Alama, Jesse, New developments in parsing Mizar, 427-431 [Zbl 1360.68743]
Chen, Xiaoyu; Li, Wei; Luo, Jie; Wang, Dongming, Open geometry textbook: a case study of knowledge acquisition via collective intelligence (project description), 432-437 [Zbl 1360.68804]
Hetzl, Stefan, Project presentation: algorithmic structuring and compression of proofs (ASCOP), 438-442 [Zbl 1360.68752]
Khan, Muhammad Taimoor; Schreiner, Wolfgang, On formal specification of Maple programs, 443-447 [Zbl 1360.68939]
Kohlhase, Michael, The Planetary project: towards eMath3.0, 448-452 [Zbl 1278.68339]
Korniłowicz, Artur, Tentative experiments with ellipsis in Mizar, 453-457 [Zbl 1360.68755]
Lange, Christoph; Ion, Patrick; Dimou, Anastasia; Bratsas, Charalampos; Corneli, Joseph; Sperber, Wolfram; Kohlhase, Michael; Antoniou, Ioannis, Reimplementing the mathematics subject classification (MSC) as a linked open dataset, 458-462 [Zbl 1257.68135]
Lange, Christoph; Kutz, Oliver; Mossakowski, Till; Grüninger, Michael, The distributed ontology language (DOL): ontology integration and interoperability applied to mathematical formalization, 463-467 [Zbl 1360.68814]
Wenzel, Makarius, Isabelle/jEdit – a prover IDE within the PIDE framework, 468-471 [Zbl 1360.68769]


68-06 Proceedings, conferences, collections, etc. pertaining to computer science
68Txx Artificial intelligence
00B25 Proceedings of conferences of miscellaneous specific interest


Maple; Coq; MSC; Mizar
Full Text: DOI