Table of Contents

• Symmetry and Search - A SurveySteve Linton. 1 [doi]
• On a Hybrid Symbolic-Connectionist Approach for Modeling the Kinematic Robot Map - and Benchmarks for Computer AlgebraJochen Pfalzgraf. 2-16 [doi]
• Applying Link Grammar Formalism in the Development of English-Indonesian Machine Translation SystemTeguh Bharata Adji, Baharum Baharudin, Norshuhani Zamin. 17-23 [doi]
• Case Studies in Model Manipulation for Scientific ComputingJacques Carette, Spencer Smith, John McCutchan, Christopher Kumar Anand, Alexandre Korobkine. 24-37 [doi]
• Mechanising a Proof of Craig s Interpolation Theorem for Intuitionistic Logic in Nominal IsabellePeter Chapman, James McKinna, Christian Urban. 38-52 [doi]
• AISC Meets Natural TypographyJames H. Davenport. 53-60 [doi]
• The Monoids of Order Eight and NineAndreas Distler, Tom Kelsey. 61-76 [doi]
• Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum ComputationLucas Dixon, Ross Duncan. 77-92 [doi]
• A Full First-Order Constraint Solver for Decomposable TheoriesKhalil Djelloul. 93-108 [doi]
• Search Techniques for Rational Polynomial OrdersCarsten Fuhs, Rafael Navarro-Marset, Carsten Otto, Jürgen Giesl, Salvador Lucas, Peter Schneider-Kamp. 109-124 [doi]
• Strategies for Solving SAT in Grids by Randomized SearchAntti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä. 125-140 [doi]
• Towards an Implementation of a Computer Algebra System in a Functional LanguageOleg Lobachev, Rita Loogen. 141-154 [doi]
• Automated Model Building: From Finite to Infinite ModelsNicolas Peltier. 155-169 [doi]
• A Groebner Bases Based Many-Valued Modal Logic Implementation in MapleEugenio Roanes-Lozano, Luis M. Laita, Eugenio Roanes-Macías. 170-183 [doi]
• On the Construction of Transformation Steps in the Category of Multiagent SystemsThomas Soboll. 184-190 [doi]
• Increasing InterpretationsHarald Zankl, Aart Middeldorp. 191-205 [doi]
• Validated Evaluation of Special Mathematical FunctionsFranky Backeljauw, Stefan Becuwe, Annie A. M. Cuyt. 206-216 [doi]
• MetiTarski: An Automatic Prover for the Elementary FunctionsBehzad Akbarpour, Lawrence C. Paulson. 217-231 [doi]
• High-Level TheoriesJacques Carette, William M. Farmer. 232-245 [doi]
• Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOLAmine Chaieb. 246-260 [doi]
• A Global Workspace Framework for Combining Reasoning SystemsJohn Charnley, Simon Colton. 261-265 [doi]
• Effective Set Membership in Computer Algebra and BeyondJames H. Davenport. 266-269 [doi]
• Formalizing in Coq Hidden Algebras to Specify Symbolic Computation SystemsCésar Domínguez. 270-284 [doi]
• Symbolic Computation Software ComposabilitySebastian Freundt, Peter Horn, Alexander Konovalov, Steve Linton, Dan Roozemond. 285-295 [doi]
• Using Coq to Prove Properties of the Cache Level of a Functional Video-on-Demand ServerJ. Santiago Jorge, Víctor M. Gulías, Laura M. Castro. 296-299 [doi]
• Automating Side Conditions in Formalized Partial FunctionsCezary Kaliszyk. 300-314 [doi]
• Combining Isabelle and QEPCAD-B in the Prover s PaletteLaura I. Meikle, Jacques D. Fleuriot. 315-330 [doi]
• Digital Mathematics Libraries: The Good, the Bad, the UglyThierry Bouche. 331-332 [doi]
• Automating Signature Evolution in Logical TheoriesAlan Bundy. 333-338 [doi]
• A Tactic Language for HiproofsDavid Aspinall, Ewen Denney, Christoph Lüth. 339-354 [doi]
• Logic-Free Reasoning in Isabelle/IsarStefan Berghofer, Makarius Wenzel. 355-369 [doi]
• A Mathematical Type for Physical VariablesJoseph B. Collins. 370-381 [doi]
• Unit Knowledge ManagementJonathan Stratford, James H. Davenport. 382-397 [doi]
• Authoring Verified Documents by Interactive Proof Construction and Verification in Text-EditorsDominik Dietrich, Ewaryst Schulz, Marc Wagner. 398-414 [doi]
• Verification of Mathematical Formulae Based on a Combination of Context-Free Grammar and Tree GrammarAkio Fujiyoshi, Masakazu Suzuki, Seiichi Uchida. 415-429 [doi]
• Specifying Strategies for ExercisesBastiaan Heeren, Johan Jeuring, Arthur van Leeuwen, Alex Gerdes. 430-445 [doi]
• Mediated Access to Symbolic Computation SystemsJónathan Heras, Vico Pascual, Julio Rubio. 446-461 [doi]
• Herbrand Sequent ExtractionStefan Hetzl, Alexander Leitsch, Daniel Weller, Bruno Woltzenlogel Paleo. 462-477 [doi]
• Visual Mathematics: Diagrammatic Formalization and ProofJohn Howse, Gem Stapleton. 478-493 [doi]
• Normalization Issues in Mathematical RepresentationsManfred Kerber. 494-503 [doi]
• Notations for Living Mathematical DocumentsMichael Kohlhase, Christine Müller, Florian Rabe. 504-519 [doi]
• Cross-Curriculum Search for IntergeoPaul Libbrecht, Cyrille Desmoulins, Christian Mercat, Colette Laborde, Michael Dietrich, Maxim Hendriks. 520-535 [doi]
• Augmenting Presentation MathML for SearchBruce R. Miller, Abdou Youssef. 536-542 [doi]
• Automated Classification and Categorization of Mathematical KnowledgeRadim Rehurek, Petr Sojka. 543-557 [doi]
• Kantian Philosophy of Mathematics and Young RobotsAaron Sloman. 558-573 [doi]
• Transforming the arXiv to XMLHeinrich Stamerjohanns, Michael Kohlhase. 574-582 [doi]
• On Correctness of Mathematical Texts from a Logical and Practical Point of ViewKonstantin Verchinine, Alexander V. Lyaletski, Andrey Paskevich, Anatoly Anisimov. 583-598 [doi]