AISC 2008

Invited Talks

• 
  Steve Linton: Symmetry and Search - A Survey. 1
• 
  Jochen Pfalzgraf: On a Hybrid Symbolic-Connectionist Approach for Modeling the Kinematic Robot Map - and Benchmarks for Computer Algebra. 2-16

Contributed Papers

• 
  Teguh Bharata Adji, Baharum Baharudin, Norshuhani Zamin: Applying Link Grammar Formalism in the Development of English-Indonesian Machine Translation System. 17-23
• 
  Jacques Carette, Spencer Smith, John McCutchan, Christopher Kumar Anand, Alexandre Korobkine: Case Studies in Model Manipulation for Scientific Computing. 24-37
• 
  Peter Chapman, James McKinna, Christian Urban: Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle. 38-52
• 
  James H. Davenport: AISC Meets Natural Typography. 53-60
• 
  Andreas Distler, Tom Kelsey: The Monoids of Order Eight and Nine. 61-76
• 
  Lucas Dixon, Ross Duncan: Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation. 77-92
• 
  Khalil Djelloul: A Full First-Order Constraint Solver for Decomposable Theories. 93-108
• 
  Carsten Fuhs, Rafael Navarro-Marset, Carsten Otto, Jürgen Giesl, Salvador Lucas, Peter Schneider-Kamp: Search Techniques for Rational Polynomial Orders. 109-124
• 
  Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä: Strategies for Solving SAT in Grids by Randomized Search. 125-140
• 
  Oleg Lobachev, Rita Loogen: Towards an Implementation of a Computer Algebra System in a Functional Language. 141-154
• 
  Nicolas Peltier: Automated Model Building: From Finite to Infinite Models. 155-169
• 
  Eugenio Roanes-Lozano, Luis M. Laita, Eugenio Roanes-Macías: A Groebner Bases Based Many-Valued Modal Logic Implementation in Maple. 170-183
• 
  Thomas Soboll: On the Construction of Transformation Steps in the Category of Multiagent Systems. 184-190
• 
  Harald Zankl, Aart Middeldorp: Increasing Interpretations. 191-205

Calculemus 2008

Invited Talk

• 
  Franky Backeljauw, Stefan Becuwe, Annie A. M. Cuyt: Validated Evaluation of Special Mathematical Functions. 206-216

Contributed Papers

• 
  Behzad Akbarpour, Lawrence C. Paulson: MetiTarski: An Automatic Prover for the Elementary Functions. 217-231
• 
  Jacques Carette, William M. Farmer: High-Level Theories. 232-245
• 
  Amine Chaieb: Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL. 246-260
• 
  John Charnley, Simon Colton: A Global Workspace Framework for Combining Reasoning Systems. 261-265
• 
  James H. Davenport: Effective Set Membership in Computer Algebra and Beyond. 266-269
• 
  César Domínguez: Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems. 270-284
• 
  Sebastian Freundt, Peter Horn, Alexander Konovalov, Steve Linton, Dan Roozemond: Symbolic Computation Software Composability. 285-295
• 
  J. Santiago Jorge, Víctor M. Gulías, Laura M. Castro: Using Coq to Prove Properties of the Cache Level of a Functional Video-on-Demand Server. 296-299
• 
  Cezary Kaliszyk: Automating Side Conditions in Formalized Partial Functions. 300-314
• 
  Laura I. Meikle, Jacques D. Fleuriot: Combining Isabelle and QEPCAD-B in the Prover's Palette. 315-330

MKM 2008

Invited Talks

• 
  Thierry Bouche: Digital Mathematics Libraries: The Good, the Bad, the Ugly. 331-332
• 
  Alan Bundy: Automating Signature Evolution in Logical Theories. 333-338

Contributed Papers

• 
  David Aspinall, Ewen Denney, Christoph Lüth: A Tactic Language for Hiproofs. 339-354
• 
  Stefan Berghofer, Makarius Wenzel: Logic-Free Reasoning in Isabelle/Isar. 355-369
• 
  Joseph B. Collins: A Mathematical Type for Physical Variables. 370-381
• 
  Jonathan Stratford, James H. Davenport: Unit Knowledge Management. 382-397
• 
  Dominik Dietrich, Ewaryst Schulz, Marc Wagner: Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors. 398-414
• 
  Akio Fujiyoshi, Masakazu Suzuki, Seiichi Uchida: Verification of Mathematical Formulae Based on a Combination of Context-Free Grammar and Tree Grammar. 415-429
• 
  Bastiaan Heeren, Johan Jeuring, Arthur van Leeuwen, Alex Gerdes: Specifying Strategies for Exercises. 430-445
• 
  Jónathan Heras, Vico Pascual, Julio Rubio: Mediated Access to Symbolic Computation Systems. 446-461
• 
  Stefan Hetzl, Alexander Leitsch, Daniel Weller, Bruno Woltzenlogel Paleo: Herbrand Sequent Extraction. 462-477
• 
  John Howse, Gem Stapleton: Visual Mathematics: Diagrammatic Formalization and Proof. 478-493
• 
  Manfred Kerber: Normalization Issues in Mathematical Representations. 494-503
• 
  Michael Kohlhase, Christine Müller, Florian Rabe: Notations for Living Mathematical Documents. 504-519
• 
  Paul Libbrecht, Cyrille Desmoulins, Christian Mercat, Colette Laborde, Michael Dietrich, Maxim Hendriks: Cross-Curriculum Search for Intergeo. 520-535
• 
  Bruce R. Miller, Abdou Youssef: Augmenting Presentation MathML for Search. 536-542
• 
  Radim Rehurek, Petr Sojka: Automated Classification and Categorization of Mathematical Knowledge. 543-557
• 
  Aaron Sloman: Kantian Philosophy of Mathematics and Young Robots. 558-573
• 
  Heinrich Stamerjohanns, Michael Kohlhase: Transforming the arXiv to XML. 574-582
• 
  Konstantin Verchinine, Alexander V. Lyaletski, Andrey Paskevich, Anatoly V. Anisimov: On Correctness of Mathematical Texts from a Logical and Practical Point of View. 583-598

last updated on Wed May 22 04:18:31 2013 by the dblp team
data released under the ODC-BY 1.0 license
see also our legal information page