Search

Interpretation methods constitute a foundation of the termination analysis of term rewriting. From time to time, remarkable instances of interpretation methods appeared, such as polynomial interpretations, matrix interpretations, arctic interpretations, and their variants. In this paper, we introduce a general framework, the tuple interpretation method, that subsumes these variants as well as many previously unknown interpretation methods as instances. Employing the notion of derivers, we prove the soundness of the proposed method in an elegant way. We implement the proposed method in the termination prover NaTT and verify its significance through experiments. [ABSTRACT FROM AUTHOR]

The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm has applications in number theory, computer algebra and cryptography. In this paper, we provide an implementation of the LLL algorithm. Both its soundness and its polynomial running-time have been verified using Isabelle/HOL. Our implementation is nearly as fast as an implementation in a commercial computer algebra system, and its efficiency can be further increased by connecting it with fast untrusted lattice reduction algorithms and certifying their output. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time. [ABSTRACT FROM AUTHOR]

We formally verify the Berlekamp–Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun's square-free factorization algorithm to integer polynomials, and thus provide an efficient and certified factorization algorithm for arbitrary univariate polynomials. The algorithm first performs factorization in the prime field GF (p) and then performs computations in the ring of integers modulo p k , where both p and k are determined at runtime. Since a natural modeling of these structures via dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using locales and local type definitions. Through experiments we verify that our algorithm factors polynomials of degree up to 500 within seconds. [ABSTRACT FROM AUTHOR]

We formalize algebraic numbers in Isabelle/HOL. Our development serves as a verified implementation of algebraic operations on real and complex numbers. We moreover provide algorithms that can identify all the real or complex roots of rational polynomials, and two implementations to display algebraic numbers, an approximative version and an injective precise one. We obtain verified Haskell code for these operations via Isabelle's code generator. The development combines various existing formalizations such as matrices, Sturm's theorem, and polynomial factorization, and it includes new formalizations about bivariate polynomials, unique factorization domains, resultants and subresultants. [ABSTRACT FROM AUTHOR]

A term rewrite system is terminating when no infinite reduction sequences are possible. Relative termination generalizes termination by permitting infinite reductions as long as some distinguished rules are not applied infinitely many times. Relative termination is thus a fundamental notion that has been used in a number of different contexts, like analyzing the confluence of rewrite systems or the termination of narrowing. In this work, we introduce a novel technique to prove relative termination by reducing it to dependency pair problems. To the best of our knowledge, this is the first significant contribution to Problem #106 of the RTA List of Open Problems. We first present a general approach that is then instantiated to provide a concrete technique for proving relative termination. The practical significance of our method is illustrated by means of an experimental evaluation. [ABSTRACT FROM AUTHOR]

The objective of this study was to quantify nitrogen (N), phosphorus (P), and potassium (K) use and cycling in a dairy farming system. The data were collected from the experimental farm at the National Institute of Livestock and Grassland Science in Tochigi Prefecture, Japan, using about 11 ha of forage crop fields and about 30 dairy cows. Forage crops grown in the field were ensiled and offered to the cows, and the subsequent compost from the animals’ excretion was applied to the field. The dairy farming system consisted of soil/crop, feed storage, animal, and compost components. Nutrient inputs and outputs and flows of the soil–plant–animal pathway for the whole farm and each component were measured for 5 years. Nutrient utilization was evaluated using nutrient balances, use efficiencies, and cycling indices. The 5 year average nutrient balances and nutrient use efficiencies of N, P, and K for the whole farm (kg ha−1 year−1) were 378, 97, and 199 and 0.25, 0.19, and 0.18, respectively. The characteristics of nutrient balances and use efficiencies for each component differed among N, P, and K. The average cycling indices of N, P, and K were 0.12, 0.11, and 0.37, respectively. Significant positive relationships between use efficiencies and cycling indices were observed in N and K. Year-to-year variations in flows were relatively large for compost application. The results suggested that improving N balance would be the most effective option for solving many of the environmental problems related to dairy farming. [ABSTRACT FROM AUTHOR]