| Description |
1 online resource (xviii, 471 pages) : illustrations |
| Series |
Lecture notes in computer science, 1611-3349 ; 7362. Lecture notes in artificial intelligence |
|
LNCS sublibrary. SL 7, Artificial intelligence |
|
Lecture notes in computer science ; 7362. 1611-3349
|
|
Lecture notes in computer science. Lecture notes in artificial intelligence
|
|
LNCS sublibrary. SL 7, Artificial intelligence.
|
| Contents |
Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar / Jesse Alama, Lionel Mamane and Josef Urban -- Proof, Message and Certificate / Andrea Asperti -- Challenges and Experiences in Managing Large-Scale Proofs / Timothy Bourke, Matthias Daum, Gerwin Klein and Rafal Kolanski -- Semantic Alliance: A Framework for Semantic Allies / Catalin David, Constantin Jucovschi, Andrea Kohlhase and Michael Kohlhase -- Extending MKM Formats at the Statement Level / Fulya Horozal, Michael Kohlhase and Florian Rabe -- A Streaming Digital Ink Framework for Multi-party Collaboration / Rui Hu, Vadim Mazalov and Stephen M. Watt -- Cost-Effective Integration of MKM Semantic Services into Editing Environments / Constantin Jucovschi -- Understanding the Learners' Actions when Using Mathematics Learning Tools / Paul Libbrecht, Sandra Rebholz, Daniel Herding, Wolfgang Müller and Felix Tscheulin -- Towards Understanding Triangle Construction Problems / Vesna Marinković and Predrag Janičić -- A Query Language for Formal Mathematical Libraries / Florian Rabe -- Abramowitz and Stegun -- A Resource for Mathematical Document Analysis / Alan P. Sexton -- Point-and-Write -- Documenting Formal Mathematics by Reference / Carst Tankink, Christoph Lange and Josef Urban -- An Essence of SSReflect / Iain Whiteside, David Aspinall and Gudmund Grov -- Theory Presentation Combinators / Jacques Carette and Russell O'Connor -- Verifying an Algorithm Computing Discrete Vector Fields for Digital Imaging / Jónathan Heras, María Poza and Julio Rubio -- Towards the Formal Specification and Verification of Maple Programs / Muhammad Taimoor Khan and Wolfgang Schreiner -- Formalizing Frankl's Conjecture: FC-Families / Filip Marić, Miodrag Živković and Bojan Vučković -- CDCL-Based Abstract State Transition System for Coherent Logic / Mladen Nikolić and Predrag Janičić -- Speeding Up Cylindrical Algebraic Decomposition by Gröbner Bases / David J. Wilson, Russell J. Bradford and James H. Davenport -- A System for Axiomatic Programming / Gabriel Dos Reis -- Reasoning on Schemata of Formulæ / Mnacho Echenim and Nicolas Peltier -- Management of Change in Declarative Languages / Mihnea Iancu and Florian Rabe -- MathWebSearch 0.5: Scaling an Open Formula Search Engine / Michael Kohlhase, Bogdan A. Matican and Corneliu-Claudiu Prodescu -- Real Algebraic Strategies for MetiTarski Proofs / Grant Olney Passmore, Lawrence C. Paulson and Leonardo de Moura -- A Combinator Language for Theorem Discovery / Phil Scott and Jacques Fleuriot -- DynGenPar -- A Dynamic Generalized Parser for Common Mathematical Language / Kevin Kofler and Arnold Neumaier -- Writing on Clouds / Vadim Mazalov and Stephen M. Watt -- A Web Interface for Matita / Andrea Asperti and Wilmer Ricciotti -- MaxTract: Converting PDF to LATEX\LaTeX, MathML and Text / Josef B. Baker, Alan P. Sexton and Volker Sorge -- New Developments in Parsing Mizar / Czesław Bylinski and Jesse Alama -- Open Geometry Textbook: A Case Study of Knowledge Acquisition via Collective Intelligence / (Project Description) / Xiaoyu Chen, Wei Li, Jie Luo and Dongming Wang -- Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP) / Stefan Hetzl -- On Formal Specification of Maple Programs / Muhammad Taimoor Khan and Wolfgang Schreiner -- The Planetary Project: Towards eMath3.0 / Michael Kohlhase -- Tentative Experiments with Ellipsis in Mizar / Artur Korniłowicz -- Reimplementing the Mathematics Subject Classification (MSC) as a Linked Open Dataset / Christoph Lange, Patrick Ion, Anastasia Dimou, Charalampos Bratsas and Joseph Corneli, et al. -- The Distributed Ontology Language (DOL): Ontology Integration and Interoperability Applied to Mathematical Formalization / Christoph Lange, Oliver Kutz, Till Mossakowski and Michael Grüninger -- Isabelle/jEdit -- A Prover IDE within the PIDE Framework / Makarius Wenzel |
| Summary |
This book constitutes the joint refereed proceedings of the 11th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2012, 19th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2012, 5th International Workshop on Digital Mathematics Libraries, DML 2012, 11th International Conference on Mathematical Knowledge Management, MKM 2012, Systems and Projects, held in Bremen, Germany as CICM 2012, the Conferences on Intelligent Computer Mathematics. The 13 revised full papers out of 19 submissions for MKM 2012, 6 revised full papers out of 9 submissions for Calculemus 2012, 6 revised full papers out of 8 submissions for AISC 2012, 2 revised full papers out of 3 submissions for DML 2012, and 11 revised full papers out of 12 submissions for Systems and Project track presented were carefully reviewed and selected, resulting in 38 papers from a total of 52 submissions |
| Analysis |
Computer science |
|
Logic design |
|
Algebra -- Data processing |
|
Information storage and retrieval systems |
|
Symbolic and Algebraic Manipulation |
|
Artificial Intelligence (incl. Robotics) |
|
Math Applications in Computer Science |
|
Mathematical Logic and Formal Languages |
|
Logics and Meanings of Programs |
|
Information Storage and Retrieval |
| Bibliography |
Includes bibliographical references and author index |
| Notes |
Online resource; title from PDF title page (SpringerLink, viewed August 8, 2012) |
| Subject |
Computer science -- Mathematics -- Congresses
|
|
Artificial intelligence -- Mathematics -- Congresses
|
|
Informatique.
|
|
Artificial intelligence -- Mathematics
|
|
Computer science -- Mathematics
|
| Genre/Form |
proceedings (reports)
|
|
Conference papers and proceedings
|
|
Conference papers and proceedings.
|
|
Actes de congrès.
|
| Form |
Electronic book
|
| Author |
Jeuring, Johan, 1965-
|
|
Calculemus (Symposium) (19th : 2012 : Bremen, Germany)
|
|
DML 2012 (2012 : Bremen, Germany)
|
|
MKM 2012 (2012 : Bremen, Germany)
|
|
CICM (Conference) (5th : 2012 : Bremen, Germany)
|
| ISBN |
9783642313745 |
|
3642313744 |
|
