Intelligent computer mathematics : 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011 : proceedings

Annotation This book constitutes the joint refereed proceedings of three international events, namely the 18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2011, the 10th International Conference on Mathematical Knowledge Management, MKM 2011, and a new track on Systems and Projects descriptions that span both the Calculemus and MKM topics, all held in Bertinoro, Italy, in July 2011. All 51 submissions passed through a rigorous review process. A total of 15 papers were submitted to Calculemus, of which 9 were accepted. Systems and Projects track 2011 there have been 12 papers selected out of 14 submissions while MKM 2011 received 22 submissions, of which 9 were accepted for presentation and publication. The events focused on the use of AI techniques within symbolic computation and the application of symbolic computation to AI problem solving; the combination of computer algebra systems and automated deduction systems; and mathematical knowledge management, respectively Front Matter....Pages - Enumeration of AG-Groupoids....Pages 1-14 Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System Framework....Pages 15-29 Incidence Simplicial Matrices Formalized in Coq/SSReflect....Pages 30-44 Proof Assistant Decision Procedures for Formalizing Origami....Pages 45-57 Using Theorema in the Formalization of Theoretical Economics....Pages 58-73 View of Computer Algebra Data from Coq....Pages 74-89 Computer Certified Efficient Exact Reals in Coq ....Pages 90-106 A Foundational View on Integration Problems....Pages 107-122 Efficient Formal Verification of Bounds of Linear Programs....Pages 123-132 Large Formal Wikis: Issues and Solutions....Pages 133-148 Licensing the Mizar Mathematical Library....Pages 149-163 Workflows for the Management of Change in Science, Technologies, Engineering and Mathematics....Pages 164-179 Parsing and Disambiguation of Symbolic Mathematics in the Naproche System....Pages 180-195 Interleaving Strategies....Pages 196-211 Combining Source, Content, Presentation, Narration, and Relational Representation....Pages 212-227 Indexing and Searching Mathematics in Digital Libraries....Pages 228-243 Isabelle as Document-Oriented Proof Assistant....Pages 244-259 Towards Formal Proof Script Refactoring....Pages 260-275 mizar-items : Exploring Fine-Grained Dependencies in the Mizar Mathematical Library....Pages 276-277 Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita....Pages 278-280 Project EuDML – A First Year Demonstration....Pages 281-284 A Symbolic Companion for Interactive Geometric Systems....Pages 285-286 MathScheme: Project Description....Pages 287-288 Project Abstract: Logic Atlas and Integrator (LATIN)....Pages 289-291 The LaTeXML Daemon: Editable Math on the Collaborative Web....Pages 292-294 A System for Computing and Reasoning in Algebraic Topology....Pages 295-297 Learning2Reason....Pages 298-300 A Formal ization of the C99 Standard in HOL, Isabelle and Coq....Pages 301-303 Krextor - An Extensible Framework for Contributing Content Math to the Web of Data....Pages 304-306 System Description: EgoMath2 As a Tool for Mathematical Searching on Wikipedia.org....Pages 307-309 Back Matter....Pages -