Intelligent Computer Mathematics
11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012, Proceedings
Published on 25. June 2012
XVIII, 473 pages
978-3-642-31374-5 (ISBN)
Description
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.
More details
Other editions
Additional editions
Johan Jeuring | John Campbell | Jacques Carette
Intelligent Computer Mathematics
11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012, Proceedings
Book
06/2012
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Mathematical Knowledge Management 2012
- Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar
- Introduction
- Dependencies: What Depends on What?
- Dependency Extraction in Coq
- Dependency Availability, Format, and Protocol
- Coverage and Limitations
- Dependency Extraction in Mizar
- Comparison of the Methods
- Evaluation, Experiments, and Applications
- Dependency Extraction for CoRN and MML
- Dependency Analysis for AI-Based Proof Assistance
- Interactive Editing with Fine-Grained Dependencies
- Learning Dependencies
- Related Work
- Conclusion and Future Work
- References
- Proof, Message and Certificate
- Introduction
- Message and Certificate
- A Social Process
- Declarative vs. Procedural
- A Complex Problem
- References
- Challenges and Experiences in Managing Large-Scale Proofs
- Introduction
- Challenges
- New Proof Engineer Joins the Project
- Expert Proof Engineer during Main Development
- Proof Maintenance
- Social and Management Aspects
- Tool Support for Moving Lemmas
- Design and Implementation Choices
- Experience and Related Work
- Summary
- References
- Semantic Alliance: A Framework for Semantic Allies
- Introduction
- The Semantic Alliance Framework
- Invasive Design via Semantic Illustration
- The Semantic Alliance Framework as a Mashup Enabler
- Building on Open APIs
- A Validation of the Semantic Alliance Framework
- Sissi: An Implementation of Semantic Alliance
- Discussion
- Related Work
- Conclusion and Future Work
- References
- Extending MKM Formats at the Statement Level
- Introduction
- MMT/OMDoc
- A Framework for Language Extensions
- Representing Extension Principles
- Syntax Extensions and Surface Languages
- OMDoc Concrete Syntax for EL Declarations
- Pragmatic Surface Syntax
- Conclusion and Future Work
- References
- A Streaming Digital Ink Framework for Multi-party Collaboration
- Introduction
- Portability of the Framework
- Portability of Software
- Portability of Digital Ink Data
- Architecture
- The Collaboration Extension
- The Training Extension
- The Mathematical Recognition Extension
- The Compression Extension
- The Rendering Extension
- The Archival Extension
- Implementation
- User Interface
- Collaboration
- Training
- Mathematical Recognition
- Discussion
- Scenarios
- Lessons Learnt
- Conclusion and Future Work
- References
- Cost-Effective Integration of MKM Semantic Services into Editing Environments
- Introduction
- Aims and Scope of Integration
- Targeted Authoring Services
- Levels of Integration
- Comparison to Other MKM Integrations
- Editor Service Integration Architecture
- The Real-Time Document Synchronization and Service Broker
- Document Model and Changesets
- Time Consuming vs. Reactive Services
- User Interaction Model
- Architecture Implementation
- Implemented Semantic Services
- Libraries and APIs
- Evaluation of Integration Costs
- Conclusion and Future Work
- References
- Understanding the Learners' Actions when Using Mathematics Learning Tools
- Learners' Actions and the Perception of Teachers
- State of the Art in Logging User Actions
- Standards for Integrating Learning Tools
- Research Around Log Collections
- Conclusions from Literature Review
- The SMALA Architecture
- Software Components and Their Interactions
- Log Objects Knowledge Structure
- Availability
- Making the Learning Tools Available
- Types of Log Views and Their Usage
- Session Views
- Requests for Help
- Summary Views
- Evaluation of Learning Tools Using SMALA-Logging
- Feature Usage Statistics
- Technical Challenges
- Conclusion
- Open Questions
- References
- Towards Understanding Triangle Construction Problems
- Introduction
- Constructions by Straightedge and Compass
- Wernick's Problems
- Underlying Geometry Knowledge
- Definitions
- Lemmas
- Primitive Constructions
- Search Algorithm
- Output
- Proving Constructions Correct
- Re-evaluation
- Future Work
- Conclusions
- References
- A Query Language for Formal Mathematical Libraries
- Introduction and Related Work
- The QMT Query Language
- Syntax
- Semantics
- Predefined Symbols
- Definable Queries
- Querying MMT Libraries
- Implementation
- Conclusion and Future Work
- References
- Abramowitz and Stegun - A Resource for Mathematical Document Analysis
- Introduction
- Abramowitz and Stegun
- Rescan and Analysis
- Connected Components and Geometric Moments
- Special Clips
- Conclusions
- References
- Point-and-Write - Documenting Formal Mathematics by Reference
- Introduction
- Describing and Including Formal Text
- Use Case
- Alternatives for Inclusion
- Syntax for Referring
- Requirements on Syntax
- Resulting Syntax
- Annotation of Types and Content
- The Type Vocabulary of the OMDoc Ontology
- Datasets for Content Annotation
- Annotating Formal Texts
- System: Agora
- Conclusions and Future Work
- References
- An Essence of SSReflect
- Introduction
- Background
- Underlying Logic of eSSence
- The eSSence Language
- Giving Meaning to eSSence Scripts
- Refactoring eSSence
- Conclusions
- References
- Calculemus 2012
- Theory Presentation Combinators
- Introduction
- The Problem
- Contributions
- Plan of Paper
- Motivation for Theory Presentation Combinators
- Category of Contexts
- Semantics of Theory Presentation Combinators
- Discussion
- Related Work
- Conclusion
- References
- Verifying an Algorithm Computing Discrete Vector Fields for Digital Imaging
- Introduction
- Mathematics to Formalize
- A Non Deterministic Algorithm in SSReflect
- An Effective Implementation: From Haskell to Coq
- The Romero-Sergeraert Algorithm
- A Haskell Program
- Testing with QuickCheck
- Formalization in Coq /SSReflect
- Experimental Results
- Application to Biomedical Images
- Conclusions and Further Work
- References
- Towards the Formal Specification and Verification of Maple Programs
- Introduction
- State of the Art
- MiniMaple
- A Type System for MiniMaple
- Design
- Formalization
- Application
- A Formal Specification Language for MiniMaple
- Formal Semantics of MiniMaple
- Conclusions and Future Work
- References
- Formalizing Frankl's Conjecture: FC-Families
- Introduction
- Frankl's Families
- Union Closed Families
- The Frankl's Condition
- Family Isomorphisms
- FC Characterization by Weight Functions and Shares
- Combinatorial Search
- Efficient Implementation
- Uniformnkm-Families
- FC-Families Verified
- Conclusions and Further Work
- References
- CDCL-Based Abstract State Transition System for Coherent Logic
- Introduction
- Background
- Abstract State Transition System for CL
- Properties of CL Transition Systems
- Generation of Readable Proofs
- Related Work
- Conclusions and Future Work
- References
- Speeding Up Cylindrical Algebraic Decomposition by Gr¨obner Bases
- Introduction
- Examples in This Paper
- BuchbergerHong1991
- Chenetal2009d
- Two Spheres and a Cylinder
- Prior Art
- Buchberger-Hong
- Phisanbut
- Further Developments
- =G with &R
- =G with =C
- =G with Inequalities in &R
- Choice of Method
- The Metric TNoI
- TNoI Data
- What Is TNoI Measuring?
- Conclusions
- References
- Artificial Intelligence and Symbolic Computation 2012
- A System for Axiomatic Programming
- Introduction
- Axiomatic Programming
- Axioms and Concepts
- Associated Types and Values
- Implementation
- Structure of the Liz System
- Type Checking
- Code Generation
- Related Work and Conclusion
- References
- Reasoning on Schemata of Formulæ
- Introduction
- A Logic for Iterated Schemata
- Proof Procedure
- Properties of the Proof Procedure
- Conclusion
- References
- Management of Change in Declarative Languages
- Introduction
- The MMT Language
- Related Work
- A Theory of Changes
- A Data Structure for Changes
- A Data Structure for Dependencies
- Change Propagation
- A Generic Change Management API
- Conclusion
- References
- MathWebSearch 0.5: Scaling an Open Formula Search Engine
- Introduction
- Querying Mathematics by Unification
- The MathWebSearch System, Version 0.5
- Substitution Tree Indexing in MathWebSearch
- Search Front Ends and Embeddings
- Evaluation
- Distributing MathWebSearch
- A Distributable Substitution Tree
- Architectural Overview
- Conclusion and Future Work
- Additional Corpora
- Extending the Indexing
- Result Ranking
- Advanced Search Services
- References
- Real Algebraic Strategies for MetiTarski Proofs
- Introduction
- Motivating Hypotheses
- Overview of Contributions
- Model Sharing
- MetiTarski Proof Search in More Detail
- Univariate Factorisations
- Experimental Results
- Future Work
- Conclusion
- References
- A Combinator Language for Theorem Discovery
- Introduction
- Incidence Reasoning in the Foundations of Geometry
- Stream Discoverers
- The Stream Monad
- Case-Analysis
- Trees
- Additional Primitives and Derived Discoverers
- Case-Splitting
- Filtering
- Deduction
- Integration
- The Problem Revisited
- Results
- Conclusion and Further Work
- References
- Digital Mathematics Libraries 2012
- DynGenPar - A Dynamic Generalized Parser for Common Mathematical Language
- Introduction
- State of the Art
- The DynGenPar Algorithm
- Design Considerations
- The Initial Graph
- Operations
- Example
- Analysis
- Implementation
- Technologies and Licensing
- Integration into FMathL Concise
- Implementation Considerations
- Predictive Parsing
- Efficient Exhaustive Parsing
- Rule Labels
- Custom Parse Actions
- Token Sources
- Natural Language
- Next Token Constraints
- Interoperability with GF
- Results
- Conclusion
- References
- Writing on Clouds
- Introduction
- Preliminaries and Related Work
- Recognition Aspects
- Architectural Aspects
- Related Work
- Clouds Serving Clouds
- Recognition Flow
- Manipulation of Clouds
- Implementation
- Initial Training
- Implementation of the Application
- Attractive Display of Recognized Characters
- Experimental Evaluation
- Setting
- Results
- Conclusion
- References
- Systems and Projects 2012
- A Web Interface for Matita
- References
- MaxTract: Converting PDF to LATEX, MathML and Text
- Introduction
- MaxTract Process
- Translation
- Basic Drivers
- Annotated PDF
- Layered PDF
- Accessibility Formats
- MaxTract Online Interface
- References
- New Developments in Parsing Mizar
- Introduction
- LayersofaMizar Text
- Normalizations of Mizar Texts
- Weakly Strict Mizar
- More Strict Mizar
- Applications
- Conclusion and Future Work
- References
- Open Geometry Textbook: A Case Study of Knowledge Acquisition via Collective Intelligence
- Motivations
- Objectives
- Methodologies
- Mechanisms
- Timelines
- References
- Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP)
- Introduction
- Theoretical Foundations
- Aims of the ASCOP-Project
- References
- On Formal Specification of Maple Programs
- Introduction
- A Type System for MiniMaple
- A Specification Language for MiniMaple
- Conclusions
- References
- The Planetary Project: Towards eMath3.0
- References
- Tentative Experiments with Ellipsis in Mizar
- Motivation
- Ellipsis
- Parsing
- Reasoning
- Verifying
- Applications in MML
- Conclusions and Future Work
- References
- Reimplementing the Mathematics Subject Classification (MSC) as a Linked Open Dataset
- References
- The Distributed Ontology Language (DOL): Ontology Integration and Interoperability Applied to Mathematical Formalization
- Distributed Ontologies for Interoperability
- The Distributed Ontology Language (DOL) - Overview
- Applications to Mathematical Formalization
- References
- Isabelle/jEdit - A Prover IDE within the PIDE Framework
- Overview
- Using the System
- Implemented Concepts
- References
- Author Index
