Modular algorithms based on the Chinese Remainder Theorem (CRT) control intermediate expression growth by performing computations modulo small primes. Some primes, that we call "unlucky," produce incorrect results, or no result; their number can be bounded by finding a nonzero U epsilon Z with the property that all unlucky primes divide U. With no error correction mechanism, CRT-based methods require that all primes are lucky, resulting in large bounds on the primes we need to guarantee success with high probability 1 - epsilon. Error-correction techniques introduced by Pernet and Bohm et al. tolerate a small number of unlucky primes, allowing us to reduce the prime size. Given height bounds on the output and the integer U above, we perform a quantitative analysis that provides explicit sufficient conditions on the number and size of the primes to ensure a given success probability. We illustrate the approach with two examples, lexicographic Grobner bases in two variables and the solution of zero-dimensional systems of equations, for which the bounds we need are already in the literature, or can be derived directly from previous work.
This paper presents an advanced method for addressing the inverse kinematics and optimal path planning challenges in robot manipulators. The inverse kinematics problem involves determining the joint angles for a given position and orientation of the end-effector. Furthermore, the path planning problem seeks a trajectory between two points. Traditional approaches in computer algebra have utilized Gröbner basis computations to solve these problems, offering a global solution but at a high computational cost. To overcome the issue, the present authors have proposed a novel approach that employs the Comprehensive Gröbner System (CGS) and CGS-based quantifier elimination (CGS-QE) methods to efficiently solve the inverse kinematics problem and certify the existence of solutions for trajectory planning. This paper extends these methods by incorporating smooth curves via cubic spline interpolation for path planning and optimizing joint configurations using shortest path algorithms to minimize the sum of joint configurations along a trajectory. This approach significantly enhances the manipulator's ability to navigate complex paths and optimize movement sequences.
The aim of this paper is to establish theoretical foundations of GHC’s rewrite rules. The Glasgow Haskell Compiler (GHC) has the feature of rewrite rules to specify optimising transformations. Rewrite rules have been widely used in many libraries. However, there has been no theory to formalise the rules and establish their correctness. We present System F_RE —the polymorphic λ -calculus System F_ω extended with higher-order term rewriting and equational reasoning to model GHC’s rewrite rules. We develop a theory and methods for verifying correctness of rewrite rules. The key to our method is to guarantee the rewriting properties of local confluence and strong normalisation. We prove the Rule Meaning Preservation Theorem that gives a simple criterion for establishing correctness of rewrite rules, which is suited for mechanical checking.
Sorting is an operation that has very important practical applications, in particular for instance in the storage and analysis of data related to the environment, climat change, etc. We describe experiments of automated certification of various sorting algorithms by using the Theorema as well as Coq and we compare the two techniques. The sorting algorithms are: Quick–Sort, Patience–Sort, Min–Sort, Max–Sort, and Min–Max–Sort. In both systems we construct the appropriate underlying theory, we define the algorithms in functional style, we run them on examples and we produce the proof of their correctness together with proofs of various lemmas that are necessary. In Theorema the proofs are almost completely automatic, are presented in natural style, and the underlying theory uses multisets in order to express the fact that the input and the output have the same elements. Moreover the proofs use a generalized induction scheme based on the well-founded ordering on lists defined by strict inclusion of multisets. In Coq the proofs are based on scripts, they require more additional lemmas, and they use element counts to compare the contents of the list. However, both the algorithm definitions as well as the proofs are absolutely rigurous as Coq cannot accept any elements that are not theoretically correct.
Property graphs play an important role in representing data bases in modern graph query languages. In this paper we focus on a particular class of graph queries known as Graph-to-Graph or CONSTRUCT queries. Such queries return graphs instead of tables when applied to actual Property Graphs. We propose a symbolic graph query solving procedure which combines rewriting techniques for goal solving as well as graph transformation techniques. The proposed procedure is proven sound and complete.
