default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID9th AISC / 7th MKM / 15th Calculemus 2008: Birmingham, UK
- Serge Autexier
, John A. Campbell, Julio Rubio, Volker Sorge, Masakazu Suzuki, Freek Wiedijk:
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. Lecture Notes in Computer Science 5144, Springer 2008, ISBN 978-3-540-85109-7
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, W. 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 W. 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 William 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-12-12 01:07 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
