As verification efforts using interactive theorem proving grow, we are in need of certified algorithms in computer algebra to tackle problems over the real numbers. This is important because uncertified procedures can drastically increase the size of the trust base and under- mine the overall confidence established by interactive theorem provers, which usually rely on a small kernel to ensure the soundness of derived results. This thesis describes an ongoing effort using the Isabelle theorem prover to certify the cylindrical algebraic decomposition (CAD) algorithm, which has been widely implemented to solve non-linear problems in various engineering and mathematical fields. Because of the sophistication of this algorithm, people are in doubt of the correctness of its implementation when deploying it to safety-critical verification projects, and such doubts motivate this thesis. In particular, this thesis proposes a library of real algebraic numbers, whose distinguishing features include a modular architecture and a sign determination algorithm requiring only rational arithmetic. With this library, an Isabelle tactic based on univariate CAD has been built in a certificate-based way: external, untrusted code delivers solutions in the form of certificates that are checked within Isabelle. To lay the foundation for the multivariate case, I have formalised various analytical results including Cauchy's residue theorem and the bivariate case of the projection theorem of CAD. During this process, I have also built a tactic to evaluate winding numbers through Cauchy indices and verified procedures to count complex roots in some domains. The formalisation effort in this thesis can be considered as the first step towards a certified computer algebra system inside a theorem prover, so that various engineering projections and mathematical calculations can be carried out in a high-confidence framework.

Computations with polynomials are at the heart of any computer algebra system and also have many applications in engineering, coding theory, and cryptography. Generally speaking, the low-level polynomial computations of interest can be classified as arithmetic operations, algebraic computations, and inverse symbolic problems. New algorithms are presented in all these areas which improve on the state of the art in both theoretical and practical performance. Traditionally, polynomials may be represented in a computer in one of two ways: as a "dense" array of all possible coefficients up to the polynomial's degree, or as a "sparse" list of coefficient-exponent tuples. In the latter case, zero terms are not explicitly written, giving a potentially more compact representation. In the area of arithmetic operations, new algorithms are presented for the multiplication of dense polynomials. These have the same asymptotic time cost of the fastest existing approaches, but reduce the intermediate storage required from linear in the size of the input to a constant amount. Two different algorithms for so-called "adaptive" multiplication are also presented which effectively provide a gradient between existing sparse and dense algorithms, giving a large improvement in many cases while never performing significantly worse than the best existing approaches. Algebraic computations on sparse polynomials are considered as well. The first known polynomial-time algorithm to detect when a sparse polynomial is a perfect power is presented, along with two different approaches to computing the perfect power factorization. Inverse symbolic problems are those for which the challenge is to compute a symbolic mathematical representation of a program or "black box". First, new algorithms are presented which improve the complexity of interpolation for sparse polynomials with coefficients in finite fields or approximate complex numbers. Second, the first polynomial-time algorithm for the more general problem of sparsest-shift interpolation is presented. The practical performance of all these algorithms is demonstrated with implementations in a high-performance library and compared to existing software and previous techniques.

This paper deals with the applications of symbolic computation of Mathematica 7.0 (Wolfram, 2008) in distribution theory. The purpose of this study is twofold. Firstly, we will implement some functions to extend Mathematica capabilities to handle symbolic computations of the characteristic function for linear combination of independent univariate random variables. These functions utilizes pattern-matching codes that enhance Mathematica's ability to simplify expressions involving the product and summation of algebraic terms. Secondly, characteristic function can be classified into commonly used distributions, including six discrete distributions and seven continuous distributions, via the pattern-matching feature of Mathematica. Finally, several examples will be presented. The examples include calculating limit of characteristic function of linear combinations of independent random variables, and applications of coded functions and illustrate the central limit theorem, the law of large numbers and properties of some distributions.

Mathematica is an extremely powerful and flexible symbolic computer algebra system that enables the user to deal with complicated algebraic tasks. It can also easily handle the numerical and graphical sides. One such task is the derivation of moment generating functions (MGF) and characteristic functions (CF), demonstrably effective tools to characterize a distribution. In this paper, we define some rules in Mathematica to help in computing the MGF and CF for linear combination of independent random variables. These commands utilizes pattern-matching code that enhances Mathematica's ability to simplify expressions involving the product of algebraic terms. This enhancement to Mathematica's functionality can be of particular benefit for MGF and CF. Applications of these rules to determine mean, variance and distribution are illustrated for various independent random variables.

Computations with polynomials are at the heart of any computer algebra system and also have many applications in engineering, coding theory, and cryptography. Generally speaking, the low-level polynomial computations of interest can be classified as arithmetic operations, algebraic computations, and inverse symbolic problems. New algorithms are presented in all these areas which improve on the state of the art in both theoretical and practical performance. Traditionally, polynomials may be represented in a computer in one of two ways: as a "dense" array of all possible coefficients up to the polynomial's degree, or as a "sparse" list of coefficient-exponent tuples. In the latter case, zero terms are not explicitly written, giving a potentially more compact representation. In the area of arithmetic operations, new algorithms are presented for the multiplication of dense polynomials. These have the same asymptotic time cost of the fastest existing approaches, but reduce the intermediate storage required from linear in the size of the input to a constant amount. Two different algorithms for so-called "adaptive" multiplication are also presented which effectively provide a gradient between existing sparse and dense algorithms, giving a large improvement in many cases while never performing significantly worse than the best existing approaches. Algebraic computations on sparse polynomials are considered as well. The first known polynomial-time algorithm to detect when a sparse polynomial is a perfect power is presented, along with two different approaches to computing the perfect power factorization. Inverse symbolic problems are those for which the challenge is to compute a symbolic mathematical representation of a program or "black box". First, new algorithms are presented which improve the complexity of interpolation for sparse polynomials with coefficients in finite fields or approximate complex numbers. Second, the first polynomial-time algorithm for the more general problem of sparsest-shift interpolation is presented. The practical performance of all these algorithms is demonstrated with implementations in a high-performance library and compared to existing software and previous techniques.

Kyoto University (京都大学) / 0048 / 新制・課程博士 / 博士(工学) / 甲第14049号 / 工博第2961号 / 新制||工||1439(附属図書館) / 26328 / UT51-2008-F441 / 京都大学大学院工学研究科電気工学専攻 / (主査)教授 和田 修己, 教授 引原 隆士, 准教授 久門 尚史, 教授 萩原 朋道 / 学位規則第4条第1項該当

There are discussed implementational aspects of the special-purpose computer algebra system FELIX designed for computations in constructive algebra. In particular, data types developed for the representation of and computation with commutative and non-commutative polynomials are described. Furthermore, comparisons of time and memory requirements of different polynomial representations are reported.

The special-purpose computer algebra system FELIX is designed for computations in constructive commutative and non-commutative algebra. In this paper we discuss some features of the system supporting the computation of rather complex problems, especially standard basis computations, using standard hardware. There is a frst aspect concerning the definition and implementation of the basic data types which should be a good compromise between space and time efficient representations of the algebraic objects. Usually, rather complex computations are very time consuming (up to weeks) and often require several attempts. So, there are included special session saving methods in FELIX which allows to backup the attained intermediate results in form of memory images into special session files and to restart later on. Finally, we describe our efforts crunching complex problems by parallelization. The implemented interface is based on stream sockets and includes a special protocol for the data exchange. It supports the distributed computation on heterogeneous, loosely coupled systems.

We report on some experiences with the general purpose Computer Algebra Systems (CAS) Axiom, Macsyma, Maple, Mathematica, MuPAD, and Reduce solving systems of polynomial equations and the way they present their solutions. This snapshot (taken in the spring 1996) of the current power of the different systems in a special area concentrates both on CPU-times and the quality of the output.

Yes / It is shown that the probability generating function of a lifetime random variable T on a finite lattice with polynomial failure rate satisfies a certain differential equation. The interrelationship with Markov chain theory is highlighted. The differential equation gives rise to a system of differential equations which, when inverted, can be used in the limit to express the polynomial coefficients in terms of the factorial moments of T. This then can be used to estimate the polynomial coefficients. Some special cases are worked through symbolically using Computer Algebra. A simulation study is used to validate the approach and to explore its potential in the reliability context.