Carsten Schneider
Carsten Schneider
A summation framework is developed that enhances Karr's difference field approach. It covers not only indefinite nested sums and products in terms of transcendental extensions, but it can treat, e.g., nested products defined over roots of u...
Shaoshi Chen,Manuel Kauers
Shaoshi Chen
We analyze the differential equations produced by the method of creative telescoping applied to a hyperexponential term in two variables. We show that equations of low order have high degree, and that higher order equations have lower degre...
L X Châu Ngô,Franz Winkler
L X Châu Ngô
In this paper, we provide an algorithm to compute explicit rational solutions of a rational system of autonomous ordinary differential equations (ODEs) from its rational invariant algebraic curves. The method is based on the proper rational...
Cezary Kaliszyk,Josef Urban
Cezary Kaliszyk
Large formal mathematical libraries consist of millions of atomic inference steps that give rise to a corresponding number of proved statements (lemmas). Analogously to the informal mathematical practice, only a tiny fraction of such statem...
Temur Kutsia,Mircea Marin
Temur Kutsia
We extend order-sorted unification by permitting regular expression sorts for variables and in the domains of function symbols. The obtained signature corresponds to a finite bottom-up unranked tree automaton. We prove that regular expressi...
Maximilian Jaroschek
Maximilian Jaroschek
Polynomial remainder sequences contain the intermediate results of the Euclidean algorithm when applied to (non-)commutative polynomials. The running time of the algorithm is dependent on the size of the coefficients of the remainders. Diff...