Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker.

Unlabelled: Automated reasoning techniques based on computer algebra have seen renewed interest in recent years and are for example heavily used in formal verification of arithmetic circuits. However, the verification process might contain errors. Generating and checking proof certificates is important to increase the trust in automated reasoning tools.

Lonely Points in Simplices.

Given a lattice and a subset , we say that a point in is if it is not equivalent modulo to another point of . We are interested in identifying lonely points for specific choices of when is a dilated standard simplex, and in conditions on which ensure that the number of lonely points is unbounded as the simplex dilation goes to infinity.

Walks with Small Steps in the 4D-Orthant.

We provide some first experimental data about generating functions of restricted lattice walks with small steps in  .

Incremental column-wise verification of arithmetic circuits using computer algebra.

Verifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice still requires substantial manual effort. The currently most effective approach uses polynomial reasoning over pseudo boolean polynomials. In this approach a word-level specification is reduced by a Gröbner basis which is implied by the gate-level representation of the circuit.

Formal Laurent series in several variables.

We explain the construction of fields of formal infinite series in several variables, generalizing the classical notion of formal Laurent series in one variable. Our discussion addresses the field operations for these series (addition, multiplication, and division), the composition, and includes an implicit function theorem.

Trading order for degree in creative telescoping.

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 degree. More precisely, we derive degree bounding formulas which allow to estimate the degree of the output equations from creative telescoping as a function of the order.