Intelligent Computer Mathematics: 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings

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 -