Titlebook: Intelligent Computer Mathematics; 16th Symposium, Calc Jacques Carette,Lucas Dixon,Stephen M. Watt Conference proceedings 2009 Springer-Ver

Abrupt

VICT

Some Traditional Mathematical Knowledge ManagementReviews, for which I have worked since 1980. From that platform we can explore and speculate both historically and prospectively. Some new results of bibliometric and other machine-enabled examination of the mathematical literature will also be discussed.

抑制

使纠缠

Combining Coq and Gappa for Certifying Floating-Point Programsed a mechanism for calling Gappa from a Coq interactive proof. This paper presents this combination and shows on several examples how this approach offers a significant speedup in the process of verifying floating-point programs.

kidney

A Comparison of Equality in Computer Algebra and Correctness in Mathematical Pedagogyand show that, despite the apparent distinction, it is possible to make many of the differences amenable to formal treatment, by asking “under which congruence is the pupil’s answer equal to the teacher’s?”.

abysmal

Algorithms for the Functional Decomposition of Laurent Polynomialsare themselves integer-valued polynomials rather than integers. The algebraic independence of ., .., ., ., and some elementary results on integer-valued polynomials allow problems with symbolic polynomials to be reduced to problems with multivariate Laurent polynomials. Hence we are interested in the functional decomposition of these objects.

误传

Exploring a Quantum Theory with Graph Rewriting and Computer Algebraal relationships via the unification of matrix equations. Since these equations can grow exponentially with the size of the graph, we use this method to discover small identities and use those identities as graph rewrites to expand the theory.

有毛就脱毛

A Linear Grammar Approach to Mathematical Formula Recognition from PDFs and show how they can be overcome. The simplicity of the original method leads to a very efficient recognition technique that not only is very simple to implement but also yields results of high accuracy for the recognition of mathematical formulae from PDF documents.

lipoatrophy

询问

https://doi.org/10.1007/978-3-642-02614-0Coq; accessible mathematics; algorithmic theories; automated deduction systems; automated reasoning; axio