Intelligent Computer Mathematics

Name: Intelligent Computer Mathematics | 9th International Conference, CICM 2016, Bialystok, Poland, July 25-29, 2016, Proceedings
Brand: Springer
Price: 42.79 EUR
Availability: OnlineOnly

9th International Conference, CICM 2016, Bialystok, Poland, July 25-29, 2016, Proceedings

Michael Kohlhase Moa Johansson Bruce Miller Leonardo de Moura Frank Tompa(Editor)

Springer (Publisher)

Published on 11. July 2016

XIV, 163 pages

E-Book

PDF with digital watermarking

System requirements

978-3-319-42547-4 (ISBN)

€42.79incl. 7% vat

System requirements

for PDF with digital watermarking

E-Book Single Licence

Available for download

Description

More details

Other editions

Content

Intro
Preface
Organization
Contents
CALCULEMUS
Mathematical Theory Exploration in Theorema: Reduction Rings
1 Introduction
2 Gröbner Bases and Reduction Rings
2.1 Reduction Rings
2.2 Gröbner Bases
2.3 Contributions to the Theory
3 Buchberger's Algorithm
4 Structure of the Formalization
4.1 Elementary Theories
4.2 Reduction Ring Theory
5 New Tools
5.1 Interactive Proof Strategy
5.2 TheoryAnalyzer
6 Conclusion
References
Formalization of Bing's Shrinking Method in Geometric Topology
1 Introduction
2 Formalization
2.1 Bing Shrinking Criterion
2.2 Baire Category Theorem
3 Relation to Some Theorems in Geometric Topology
3.1 Proof Sketch of the GST Using Bing's Shrinking Method
3.2 Abstract Property of Disks Necessary for Shrinking Arguments
3.3 Future Plan
4 Conclusion
References
SC2: Satisfiability Checking Meets Symbolic Computation
1 Introduction
2 Background
2.1 Symbolic Computation and Computer Algebra Systems
2.2 Satisfiability Checking
3 Some Scientific Challenges and Opportunities
3.1 Symbolic Computation Techniques for Satisfiability Checking
3.2 Satisfiability Checking Techniques for Symbolic Computation
3.3 Standard Languages and Benchmarks
4 Project Actions
5 Conclusions and Future Work
References
Formalization of Normal Random Variables in HOL
1 Introduction
2 Preliminaries
2.1 Measure Theory
2.2 Lebesgue Integration Theory
2.3 Probability Theory
3 Formalization of Lebesgue-Borel Measure
3.1 Gauge Integral
3.2 Borel Measurable Sets
3.3 Lebesgue Measure
3.4 Lebesgue-Borel Measure
4 Formalization of Normal Random Variables
4.1 Radon Nikodym Theorem
4.2 Probability Density Function
4.3 Normal Random Variables
4.4 Properties of Normal Random Variables
5 Application: Probabilistic Clock Synchronization in Wireless Sensor Networks
5.1 Single-Hop Network
5.2 Multi-hop Network
5.3 Discussion
6 Conclusion
References
Digital Mathematics Libraries
Progress of Self-Archiving Within the DML Corpus, with a View Toward Community Dynamics
1 Introduction
2 Matching the arXiv and zbMATH: Methodology and Precision
3 Time Lag Effect: Retroarchiving and Publication/Indexing Delay
4 General Coverage Figures and Dynamics
5 Submission Behavior: An Author-Based Analysis
6 Subject Specifics
7 Conclusions
References
Mathematical Knowledge Management
Accessing the Mizar Library with a Weakly Strict Mizar Parser
1 Introduction
2 WS-Mizar Grammar Specification
3 Parser Implementation
4 Conclusions
References
Incorporating Quotation and Evaluation into Church's Type Theory: Syntax and Semantics
1 Introduction
2 Syntax
2.1 Types
2.2 Expressions
2.3 Constructions
2.4 Definitions and Abbreviations
3 Semantics
3.1 Frames
3.2 Interpretations
3.3 Models
4 Examples
4.1 Reasoning About Syntax
4.2 Quasiquotation
4.3 Schemas
4.4 Meaning Formulas
5 A Sketch of a Simple Proof System
6 Conclusion
References
Extracting Higher-Order Goals from the Mizar Mathematical Library
1 Introduction
2 Syntax of Higher-Order Logic
3 Idealized Mizar
4 Mapping Mizar to Higher-Order Logic
5 Experiments
6 Conclusion
References
Surveys and Projects
Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach
1 Introduction
2 The OPENDREAMKIT Project (2015--2019)
3 Integrating Mathematical Software Systems via the Math-in-the-Middle Approach
3.1 A Common Meaning Space for Interoperability
3.2 Realizing and Utilizing a MitM Ontology
4 LMFDB Knowledge and Interoperability
5 Distributed Collaboration with GAP/Sage
5.1 Semantics in the Sage Category System
5.2 Exporting the GAP Knowledge: Type System Documentation
6 Conclusion
References
Formal Dependability Modeling and Analysis: A Survey
1 Introduction
2 Dependability Modeling Techniques
2.1 Reliability Block Diagrams
2.2 Fault Trees
2.3 Markov Chain
3 Formal Dependability Analysis Techniques
3.1 Petri Nets
3.2 Model Checking
3.3 Higher-Order-Logic Theorem Proving
4 Comparison and Discussion
4.1 Comparison of Dependability Modeling Techniques
4.2 Comparison of Dependability Analysis Techniques
5 Conclusions
References
Systems and Data
Extending E Prover with Similarity Based Clause Selection Strategies
1 Introduction
2 Clause Selection in E Prover
3 Similarity Based Clause Selection Strategies
4 Experimental Results and Evaluation
5 Conclusions and Future Work
References
Enhancement of MIZAR Texts with Transitivity Property of Predicates
1 Introduction
2 Transitivity
3 Experiments
4 Further Work
5 Conclusions
References
Erratum to: Formal Dependability Modeling and Analysis: A Survey
Erratum to: Chapter "Formal Dependability Modeling and Analysis: A Survey" in: M. Kohlhase et al. (Eds.): Intelligent Computer Mathematics, LNAI, DOI: 10.1007/978-3-319-42547-4_10
Author Index

System requirements

Save as PDF Copy link into clipboard

Schweitzer Fachinformationen

Intelligent Computer Mathematics

Description

More details

Other editions

Additional editions

Content

System requirements