You have Guest access.
Log In
Serge Autexier, John Campbell, Julio Rubio, Volker Sorge, Masakazu Suzuki and Freek Wiedijk
Front matter
1
Symmetry and Search – A Survey
2-16
On a Hybrid Symbolic-Connectionist Approach for Modeling the Kinematic Robot Map - and Benchmarks for Computer Algebra
17-23
Applying Link Grammar Formalism in the Development of English-Indonesian Machine Translation System
24-37
Case Studies in Model Manipulation for Scientific Computing
38-52
Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle
53-60
AISC Meets Natural Typography
61-76
The Monoids of Order Eight and Nine
77-92
Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation
93-108
A Full First-Order Constraint Solver for Decomposable Theories
109-124
Search Techniques for Rational Polynomial Orders
125-140
Strategies for Solving SAT in Grids by Randomized Search
141-154
Towards an Implementation of a Computer Algebra System in a Functional Language
155-169
Automated Model Building: From Finite to Infinite Models
170-183
A Groebner Bases Based Many-Valued Modal Logic Implementation in Maple
184-190
On the Construction of Transformation Steps in the Category of Multiagent Systems
191-205
Increasing Interpretations
206-216
Validated Evaluation of Special Mathematical Functions
217-231
MetiTarski: An Automatic Prover for the Elementary Functions
232-245
High-Level Theories
246-260
Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL
261-265
A Global Workspace Framework for Combining Reasoning Systems
266-269
Effective Set Membership in Computer Algebra and Beyond
270-284
Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
285-295
Symbolic Computation Software Composability
296-299
Using Coq to Prove Properties of the Cache Level of a Functional Video-on-Demand Server
300-314
Automating Side Conditions in Formalized Partial Functions
315-330
Combining Isabelle and QEPCAD-B in the Prover’s Palette
331-332
Digital Mathematics Libraries: The Good, the Bad, the Ugly
333-338
Automating Signature Evolution in Logical Theories
339-354
A Tactic Language for Hiproofs
355-369
Logic-Free Reasoning in Isabelle/Isar
370-381
A Mathematical Type for Physical Variables
382-397
Unit Knowledge Management
398-414
Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors
415-429
Verification of Mathematical Formulae Based on a Combination of Context-Free Grammar and Tree Grammar
430-445
Specifying Strategies for Exercises
446-461
Mediated Access to Symbolic Computation Systems
462-477
Herbrand Sequent Extraction
478-493
Visual Mathematics: Diagrammatic Formalization and Proof
494-503
Normalization Issues in Mathematical Representations
504-519
Notations for Living Mathematical Documents
520-535
Cross-Curriculum Search for Intergeo
536-542
Augmenting Presentation MathML for Search
543-557
Automated Classification and Categorization of Mathematical Knowledge
558-573
Kantian Philosophy of Mathematics and Young Robots
574-582
Transforming the ar χ iv to XML
583-598
On Correctness of Mathematical Texts from a Logical and Practical Point of View
Back matter
This page requires script.
Frequently asked questions General info on journals and books Send us your feedback Impressum Contact us
© Springer, Part of Springer Science+Business Media Privacy, Disclaimer, Terms & Conditions, and Copyright Info