10. MKM / 18. Calculemus 2011: Bertinoro, Italy

James H. Davenport, William M. Farmer, Josef Urban, Florian Rabe (Eds.): Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings. Lecture Notes in Computer Science 6824 Springer 2011, ISBN 978-3-642-22672-4

Calculemus 2011

Andreas Distler, Muhammad Shah, Volker Sorge:
Enumeration of AG-Groupoids. 1-14
Gabriel Dos Reis, David Matthews, Yue Li:
Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System Framework. 15-29
Jónathan Heras, María Poza, Maxime Dénès, Laurence Rideau:
Incidence Simplicial Matrices Formalized in Coq/SSReflect. 30-44
Cezary Kaliszyk, Tetsuo Ida:
Proof Assistant Decision Procedures for Formalizing Origami. 45-57
Manfred Kerber, Colin Rowat, Wolfgang Windsteiger:
Using Theorema in the Formalization of Theoretical Economics. 58-73
Vladimir Komendantsky, Alexander Konovalov, Steve Linton:
View of Computer Algebra Data from Coq. 74-89
Robbert Krebbers, Bas Spitters:
Computer Certified Efficient Exact Reals in Coq. 90-106
Florian Rabe, Michael Kohlhase, Claudio Sacerdoti Coen:
A Foundational View on Integration Problems. 107-122
Alexey Solovyev, Thomas C. Hales:
Efficient Formal Verification of Bounds of Linear Programs. 123-132

Jesse Alama, Kasper Brink, Lionel Mamane, Josef Urban:
Large Formal Wikis: Issues and Solutions. 133-148
Jesse Alama, Michael Kohlhase, Lionel Mamane, Adam Naumowicz, Piotr Rudnicki, Josef Urban:
Licensing the Mizar Mathematical Library. 149-163
Serge Autexier, Catalin David, Dominik Dietrich, Michael Kohlhase, Vyacheslav Zholudev:
Workflows for the Management of Change in Science, Technologies, Engineering and Mathematics. 164-179
Marcos Cramer, Peter Koepke, Bernhard Schröder:
Parsing and Disambiguation of Symbolic Mathematics in the Naproche System. 180-195
Bastiaan Heeren, Johan Jeuring:
Interleaving Strategies. 196-211
Fulya Horozal, Alin Iacob, Constantin Jucovschi, Michael Kohlhase, Florian Rabe:
Combining Source, Content, Presentation, Narration, and Relational Representation. 212-227
Petr Sojka, Martin Líska:
Indexing and Searching Mathematics in Digital Libraries - Architecture, Design and Scalability Issues. 228-243
Makarius Wenzel:
Isabelle as Document-Oriented Proof Assistant. 244-259
Iain Whiteside, David Aspinall, Lucas Dixon, Gudmund Grov:
Towards Formal Proof Script Refactoring. 260-275

Jesse Alama:
mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library. 276-277
Andrea Asperti, Maria Emilia Maietti, Claudio Sacerdoti Coen, Giovanni Sambin, Silvio Valentini:
Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita. 278-280
José Luis Borbinha, Thierry Bouche, Aleksander Nowinski, Petr Sojka:
Project EuDML - A First Year Demonstration. 281-284
Francisco Botana:
A Symbolic Companion for Interactive Geometric Systems. 285-286
Jacques Carette, William M. Farmer, Russell O'Connor:
MathScheme: Project Description. 287-288
Mihai Codescu, Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe:
Project Abstract: Logic Atlas and Integrator (LATIN). 289-291
Deyan Ginev, Heinrich Stamerjohanns, Bruce R. Miller, Michael Kohlhase:
The LaTeXML Daemon: Editable Math on the Collaborative Web. 292-294
Jónathan Heras, Vico Pascual, Julio Rubio:
A System for Computing and Reasoning in Algebraic Topology. 295-297
Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes:
Learning2Reason. 298-300
Robbert Krebbers, Freek Wiedijk:
A Formalization of the C99 Standard in HOL, Isabelle and Coq. 301-303
Christoph Lange:
Krextor - An Extensible Framework for Contributing Content Math to the Web of Data. 304-306
Jozef Misutka, Leo Galambos:
System Description: EgoMath2 As a Tool for Mathematical Searching on Wikipedia.org. 307-309

Last update Fri May 25 08:27:10 2012 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page