Atjaunināt sīkdatņu piekrišanu

Intelligent Computer Mathematics: 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011, Proceedings [Mīkstie vāki]

Edited by , Edited by , Edited by , Edited by
  • Formāts: Paperback / softback, 312 pages, height x width: 235x155 mm, weight: 498 g, XIII, 312 p., 1 Paperback / softback
  • Sērija : Lecture Notes in Artificial Intelligence 6824
  • Izdošanas datums: 18-Jul-2011
  • Izdevniecība: Springer-Verlag Berlin and Heidelberg GmbH & Co. K
  • ISBN-10: 3642226728
  • ISBN-13: 9783642226724
  • Mīkstie vāki
  • Cena: 46,91 €*
  • * ši ir gala cena, t.i., netiek piemērotas nekādas papildus atlaides
  • Standarta cena: 55,19 €
  • Ietaupiet 15%
  • Grāmatu piegādes laiks ir 3-4 nedēļas, ja grāmata ir uz vietas izdevniecības noliktavā. Ja izdevējam nepieciešams publicēt jaunu tirāžu, grāmatas piegāde var aizkavēties.
  • Daudzums:
  • Ielikt grozā
  • Piegādes laiks - 4-6 nedēļas
  • Pievienot vēlmju sarakstam
  • Formāts: Paperback / softback, 312 pages, height x width: 235x155 mm, weight: 498 g, XIII, 312 p., 1 Paperback / softback
  • Sērija : Lecture Notes in Artificial Intelligence 6824
  • Izdošanas datums: 18-Jul-2011
  • Izdevniecība: Springer-Verlag Berlin and Heidelberg GmbH & Co. K
  • ISBN-10: 3642226728
  • ISBN-13: 9783642226724
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.
Calculemus 2011
Enumeration of AG-Groupoids
1(14)
Andreas Distler
Muhammad Shah
Volker Sorge
Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System Framework
15(15)
Gabriel Dos Reis
David Matthews
Yue Li
Incidence Simplicial Matrices Formalized in Coq/SSReflect
30(15)
Jonathan Heras
Maria Poza
Maxime Denes
Laurence Rideau
Proof Assistant Decision Procedures for Formalizing Origami
45(13)
Cezary Kaliszyk
Tetsuo Ida
Using Theorema in the Formalization of Theoretical Economics
58(16)
Manfred Kerber
Colin Rowat
Wolfgang Windsteiger
View of Computer Algebra Data from Coq
74(16)
Vladimir Komendantsky
Alexander Konovalov
Steve Linton
Computer Certified Efficient Exact Reals in Coq
90(17)
Robbert Krebbers
Bas Spitters
A Foundational View on Integration Problems
107(16)
Florian Rabe
Michael Kohlhase
Claudio Sacerdoti Coen
Efficient Formal Verification of Bounds of Linear Programs
123(10)
Alexey Solovyev
Thomas C. Hales
Mathematical Knowledge Management 2011
Large Formal Wikis: Issues and Solutions
133(16)
Jesse Alama
Kasper Brink
Lionel Mamane
Josef Urban
Licensing the Mizar Mathematical Library
149(15)
Jesse Alama
Michael Kohlhase
Lionel Mamane
Adam Naumowicz
Piotr Rudnicki
Josef Urban
Workflows for the Management of Change in Science, Technologies, Engineering and Mathematics
164(16)
Serge Autexier
Catalin David
Dominik Dietrich
Michael Kohlhase
Vyacheslav Zholudev
Parsing and Disambiguation of Symbolic Mathematics in the Naproche System
180(16)
Marcos Cramer
Peter Koepke
Bernhard Schroder
Interleaving Strategies
196(16)
Bastiaan Heeren
Johan Jeuring
Combining Source, Content, Presentation, Narration, and Relational Representation
212(16)
Fulya Horozal
Alin Iacob
Constantin Jucovschi
Michael Kohlhase
Florian Rabe
Indexing and Searching Mathematics in Digital Libraries: Architecture, Design and Scalability Issues
228(16)
Petr Sojka
Martin Liska
Isabelle as Document-Oriented Proof Assistant
244(16)
Makarius Wenzel
Towards Formal Proof Script Refactoring
260(16)
Iain Whiteside
David Aspinall
Lucas Dixon
Gudmund Grov
CICM Systems and Projects
mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
276(2)
Jesse Alama
Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita
278(3)
Andrea Asperti
Maria Emilia Maietti
Claudio Sacerdoti Coen
Giovanni Sambin
Silvio Valentini
Project EuDML A First Year Demonstration
281(4)
Jose Borbinha
Thierry Bouche
Aleksander Nowinski
Petr Sojka
A Symbolic Companion for Interactive Geometric Systems
285(2)
Francisco Botana
MathScheme: Project Description
287(2)
Jacques Carette
William M. Farmer
Russell O'Connor
Project Abstract: Logic Atlas and Integrator (LATIN)
289(3)
Mihai Codescu
Fulya Horozal
Michael Kohlhase
Till Mossakowski
Florian Rabe
The LaTeXML Daemon: Editable Math on the Collaborative Web
292(3)
Deyan Ginev
Heinrich Stamerjohanns
Bruce R. Miller
Michael Kohlhase
A System for Computing and Reasoning in Algebraic Topology
295(3)
Jonathan Heras
Vico Pascual
Julio Rubio
Learning2Reason
298(3)
Daniel Kuhlwein
Josef Urban
Evgeni Tsivtsivadze
Herman Geuvers
Tom Heskes
A Formalization of the C99 Standard in HOL, Isabelle and Coq
301(3)
Robbert Krebbers
Freek Wiedijk
Krextor - An Extensible Framework for Contributing Content Math to the Web of Data
304(3)
Christoph Lange
System Description: EgoMath2 as a Tool for Mathematical Searching on Wikipedia.org
307(4)
Jozef Misutka
Leo Galambos
Author Index 311