Steve Linton (auth.), Serge Autexier, John Campbell, Julio Rubio, Volker Sorge, Masakazu Suzuki, Freek Wiedijk (eds.)3540851097, 9783540851097
This book constitutes the joint refereed proceedings of the 9th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2008, the 15th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2008, and the 7th International Conference on Mathematical Knowledge Management, MKM 2008, held in Birmingham, UK, in July/August as CICM 2008, the Conferences on Intelligent Computer Mathematics.
The 14 revised full papers for AISC 2008, 10 revised full papers for Calculemus 2008, and 18 revised full papers for MKM 2008, plus 5 invited talks, were carefully reviewed and selected from a total of 81 submissions for a joint presentation in the book. The papers cover different aspects of traditional branches in CS such as computer algebra, theorem proving, and artificial intelligence in general, as well as newly emerging ones such as user interfaces, knowledge management, and theory exploration, thus facilitating the development of integrated mechanized mathematical assistants that will be routinely used by mathematicians, computer scientists, and engineers in their every-day business.
Table of contents :
Front Matter….Pages –
Symmetry and Search – A Survey….Pages 1-1
On a Hybrid Symbolic-Connectionist Approach for Modeling the Kinematic Robot Map – and Benchmarks for Computer Algebra….Pages 2-16
Applying Link Grammar Formalism in the Development of English-Indonesian Machine Translation System….Pages 17-23
Case Studies in Model Manipulation for Scientific Computing….Pages 24-37
Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle….Pages 38-52
AISC Meets Natural Typography….Pages 53-60
The Monoids of Order Eight and Nine….Pages 61-76
Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation….Pages 77-92
A Full First-Order Constraint Solver for Decomposable Theories….Pages 93-108
Search Techniques for Rational Polynomial Orders….Pages 109-124
Strategies for Solving SAT in Grids by Randomized Search….Pages 125-140
Towards an Implementation of a Computer Algebra System in a Functional Language….Pages 141-154
Automated Model Building: From Finite to Infinite Models….Pages 155-169
A Groebner Bases Based Many-Valued Modal Logic Implementation in Maple….Pages 170-183
On the Construction of Transformation Steps in the Category of Multiagent Systems….Pages 184-190
Increasing Interpretations….Pages 191-205
Validated Evaluation of Special Mathematical Functions….Pages 206-216
MetiTarski: An Automatic Prover for the Elementary Functions….Pages 217-231
High-Level Theories….Pages 232-245
Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL….Pages 246-260
A Global Workspace Framework for Combining Reasoning Systems….Pages 261-265
Effective Set Membership in Computer Algebra and Beyond….Pages 266-269
Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems….Pages 270-284
Symbolic Computation Software Composability….Pages 285-295
Using Coq to Prove Properties of the Cache Level of a Functional Video-on-Demand Server….Pages 296-299
Automating Side Conditions in Formalized Partial Functions….Pages 300-314
Combining Isabelle and QEPCAD-B in the Prover’s Palette….Pages 315-330
Digital Mathematics Libraries: The Good, the Bad, the Ugly….Pages 331-332
Automating Signature Evolution in Logical Theories….Pages 333-338
A Tactic Language for Hiproofs….Pages 339-354
Logic-Free Reasoning in Isabelle/Isar….Pages 355-369
A Mathematical Type for Physical Variables….Pages 370-381
Unit Knowledge Management….Pages 382-397
Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors….Pages 398-414
Verification of Mathematical Formulae Based on a Combination of Context-Free Grammar and Tree Grammar….Pages 415-429
Specifying Strategies for Exercises….Pages 430-445
Mediated Access to Symbolic Computation Systems….Pages 446-461
Herbrand Sequent Extraction….Pages 462-477
Visual Mathematics: Diagrammatic Formalization and Proof….Pages 478-493
Normalization Issues in Mathematical Representations….Pages 494-503
Notations for Living Mathematical Documents….Pages 504-519
Cross-Curriculum Search for Intergeo….Pages 520-535
Augmenting Presentation MathML for Search….Pages 536-542
Automated Classification and Categorization of Mathematical Knowledge….Pages 543-557
Kantian Philosophy of Mathematics and Young Robots….Pages 558-573
Transforming the ar χ iv to XML….Pages 574-582
On Correctness of Mathematical Texts from a Logical and Practical Point of View….Pages 583-598
Back Matter….Pages –
Reviews
There are no reviews yet.