Intelligent Computer Mathematics
18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011, Proceedings
Published on 18. July 2011
XIII, 312 pages
978-3-642-22673-1 (ISBN)
Description
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.
More details
Other editions
Additional editions
James H. Davenport | William M. Farmer | Florian Rabe
Intelligent Computer Mathematics
18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011, Proceedings
Book
07/2011
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Calculemus 2011
- Enumeration of AG-Groupoids
- Introduction
- Background
- Constructing AG-Groupoids
- CSP and Minion
- Symmetry Breaking and GAP
- Search
- Classification of AG-Groupoids
- Conclusions
- References
- Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System Framework
- Introduction
- The OpenAxiom and Poly/ML Systems
- OpenAxiom
- Poly/ML
- Spad Program Representation
- Poly/ML Codetrees
- Generating Poly/ML Codetree from OIL
- Implementation
- Example
- Related Work
- Conclusion and Future Work
- References
- Incidence Simplicial Matrices Formalized in Coq/SSReflect
- Introduction
- Mathematical Preliminaries
- The Theorem Formalized and Its Context
- SSReflect Basics
- Formal Development
- Conclusions and Further Work
- References
- Proof Assistant Decision Procedures for Formalizing Origami
- Introduction
- Computational Origami
- Computer Algebra functionality in Proof Assistants
- Contents
- Formalizing a Proof Document
- Equilateral Triangle Construction
- Equations Solving Tactic
- Evaluation
- Inequalities
- Related Work
- Outlook
- Future Work
- References
- Using Theorema in the Formalization of Theoretical Economics
- Introduction
- A Brief Introduction to Pillage Games
- Formalizations in Theorema
- Lemma 1: Representation
- Lemma 2: Domination
- Lemma 3: The Core
- Pseudo-Code and Its Computational Content
- Added Value-Price Paid
- Conclusion
- References
- View of Computer Algebra Data from Coq
- Introduction
- Views of Computer Algebra Data
- SCSCP and the Working Example
- Term Internalisation
- Term Externalisation
- An Advanced Example
- Related Work
- Conclusions and Possible Directions
- References
- Computer Certified Efficient Exact Reals in Coq
- Introduction
- The Coq-System
- Metric Spaces
- Abstract Interfaces Using Type Classes
- Order Theory
- Basic Operations
- Decision Procedures
- Approximate Rationals
- Power Series
- Square Root
- Benchmarks
- Conclusions and Related Work
- References
- A Foundational View on Integration Problems
- Introduction
- The MMT Language
- Integration Challenges
- A Framework for System Integration
- Partial Theory Morphisms in MMT
- Integration via Partial Theory Morphisms
- Related Work
- Conclusion
- References
- Efficient Formal Verification of Bounds of Linear Programs
- Introduction
- Verification of Bounds of Linear Programs
- Finding a Dual Solution
- Formal Verification
- Optimization
- Integer Arithmetic
- Faster Low Precision Arithmetic in HOL Light
- Performance Tests
- References
- Mathematical Knowledge Management 2011
- Large Formal Wikis: Issues and Solutions
- Overview
- Introduction: Developing Formal Math Wikis
- The Generalized Formal Wiki Architecture, and Its Coq and CoRN Instance
- HTML Presentation of Coq Content with Coqdoc
- Batch-Mode Processing and Dependency Analysis with Coq
- New CoRN Development with SSReflect
- Using Fine-Grained Dependency Information for a Large Formal Wiki
- Speeding Up (re)verification
- Delimited Editing
- Scaling Up
- Many Users, Many Branches
- Multiple Wiki Servers and Their Synchronization
- Conclusion and Further Issues
- References
- Licensing the Mizar Mathematical Library
- Introduction - Formal Mathematics and Its Roots
- What Is a Formal Math Library?
- Historical Background of the MML
- Two Aspects of Formal Mathematics: Code and Text
- Code and Text Licenses
- Patents
- Related Licensing Models
- Licensing Models of Formal Libraries
- Issues and Their Solutions
- Features Required from the License
- Linking and Adaptation
- Why Open-Source Copyleft License?
- Why Keep the Copyright Ownership with SUM?
- Enforcing FLOSS
- What Are Reasonable Conditions for Copyright Ownership?
- Conclusion and Future Work
- References
- Workflows for the Management of Change in Science, Technologies, Engineering and Mathematics
- Introduction
- The Planetary System
- A Planetary Workflow
- DocTIP
- Change Impact Analysis
- Change Impact Analysis Workflow
- System Architecture
- Example Revisited
- Related Work
- Conclusion
- References
- Parsing and Disambiguation of Symbolic Mathematics in the Naproche System
- Introduction
- The Naproche System
- Symbolic Mathematics
- Possible Approaches to Disambiguation
- A Type System for Symbolic Mathematics
- Syntactic Types
- Normal Formula Grammar
- Operator Priorities
- Defaultness of the Syntactic Type Classical
- Predefined Variables
- Kinds of Variables
- Coverage of the Formula Grammar
- Quantterm Grammar
- Disambiguating Quantterms
- Disambiguation after Parsing
- Related Work
- Conclusion
- References
- Interleaving Strategies
- Introduction
- Examples
- Interleaving and Rewrite Strategies
- Interleaving Sentences
- Interleaving Sets
- Atomicity
- Interleaving Strategies
- Implementing Interleaving Strategies
- Defining Empty
- Defining Firsts
- Dealing with Administrative Rules
- Labels in Strategies
- Navigation Actions
- Examples Revisited
- Applying Tautologies
- Solving Polynomial Equations of a Higher-Degree
- Conclusions and Related Work
- References
- Combining Source, Content, Presentation, Narration, and Relational Representation
- Introduction
- Structured Document Collections
- The LATIN Logic Atlas
- Computer Science Lecture Notes in Planetary
- A Multi-dimensional Knowledge Representation
- Dimensions of Knowledge
- A Mathematical Archive Format
- Catalog Services
- The Author's Perspective
- Multi-dimensional Knowledge in an IDE
- Added-Value Services
- The Reader's Perspective
- Discussion
- Conclusion
- References
- Indexing and Searching Mathematics in Digital Libraries
- Introduction
- Approaches to Searching Mathematics
- DesignofMIaS
- SystemWorkflow
- Indexing
- Tokenization
- Formulae Modifications
- Ordering
- Unification of Variables
- Unification of Constants
- FormulaeWeighting
- Searching
- Evaluation
- Implementation
- Corpus ofMathematical Documents MREC
- Results
- Scalability Testing and Efficiency
- Open Issues, Future Work
- Conclusions
- References
- Isabelle as Document-Oriented Proof Assistant
- Introduction
- TextwithMarkup
- Text Encoding and Rendering
- Markup via Text Addressing
- YXML Transfer Syntax
- XMLContent
- Typed Views on Untyped Data
- Augmented Oppen Pretty-Printing
- Document Reconstruction
- Conclusion and Related Work
- References
- Towards Formal Proof Script Refactoring
- Introduction
- Background
- Proof Scripts
- Proof Script Refactoring
- A Declarative Proof Language
- Example
- Refactorings
- Rename Lemma
- Swap Objects
- Transform Proof
- Backward Proof to Forward Proof
- Extract Subproof
- Example Refactoring
- Related Work and Conclusions
- References
- CICM Systems and Projects
- mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
- References
- Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita
- References
- Project EuDML-A First Year Demonstration
- References
- A Symbolic Companion for Interactive Geometric Systems
- References
- MathScheme: Project Description
- References
- Project Abstract: Logic Atlas and Integrator (LATIN)
- References
- The LaTeXML Daemon: Editable Math on the Collaborative Web
- References
- A System for Computing and Reasoning in Algebraic Topology
- References
- Learning2Reason
- References
- A Formalization of the C99 Standard in HOL, Isabelle and Coq
- References
- Krextor - An Extensible Framework for Contributing Content Math to the Web of Data
- Problem Statement: No Math on the Web of Data Yet
- The Krextor XMLRDF Extraction Library
- Publishing the OpenMath CDs as Linked Data
- Coverage of the System Demo
- References
- System Description: EgoMath2 As a Tool for Mathematical Searching on Wikipedia.org
- Introduction
- New Features and Architecture Changes in EgoMath2
- Adjusting Wikipedia for EgoMath2 and vice versa
- Conclusion and Availability
- References
- Author Index
