Intelligent Computer Mathematics

Name: 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
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

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

Johan Jeuring John Campbell Jacques Carette Gabriel Dos Reis Petr Sojka Makarius Wenzel Volker Sorge(Herausgeber*in)

Springer (Verlag)

Erschienen am 25. Juni 2012

XVIII, 473 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-31374-5 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken