Automated Reasoning

@article{RISC7252,
author = {Georg Regensburger and Clemens Hofstadler and Clemens Raab},
title = {{Universal truth of operator statements via ideal membership}},
language = {english},
abstract = {We introduce a framework for proving statements about linear operators by verification of ideal membership in a free algebra. More specifically, arbitrary first-order statements about identities of morphisms in preadditive semicategories can be treated. We present a semi-decision procedure for validity of such formulas based on computations with noncommutative polynomials. These algebraic computations automatically incorporate linearity and benefit from efficient ideal membership procedures.In the framework, domains and codomains of operators are modelled using many-sorted first-order logic. To eliminate quantifiers and function symbols from logical formulas, we apply Herbrand's theorem and Ackermann's reduction. The validity of the resulting formulas is shown to be equivalent to finitely many ideal memberships of noncommutative polynomials. We explain all relevant concepts and discuss computational aspects. Furthermore, we illustrate our framework by proving concrete operator statements assisted by our computer algebra software.},
journal = {Journal of Pure and Applied Algebra},
volume = {230},
number = {108221},
pages = {0--0},
isbn_issn = {0022-4049},
year = {2026},
refereed = {yes},
length = {40},
url = {https://doi.org/10.1016/j.jpaa.2026.108221}
}

@article{RISC7253,
author = {Georg Regensburger and Stefan Müller},
title = {{Parametrized systems of generalized polynomial inequalities via linear algebra and convex geometry}},
language = {english},
abstract = {We provide fundamental results on positive solutions to parametrized systems of generalized polynomial inequalities (with real exponents and positive parameters), including generalized polynomial equations. In doing so, we also offer a new perspective on fewnomials and (generalized) mass-action systems. We find that geometric objects, rather than matrices, determine generalized polynomial systems: a bounded set/“polytope” P (arising from the coefficient matrix) and two subspaces representing monomial differences and dependencies (arising from the exponent matrix). The dimension of the latter subspace, the monomial dependency d, is crucial. As our main result, we rewrite polynomial inequalities in terms of d binomial equations on P, involving d monomials in the parameters. In particular, we establish an explicit bijection between the original solution set and the solution set on P via exponentiation. (i) Our results apply to any generalized polynomial system. (ii) The dependency d and the dimension of P indicate the complexity of a system. (iii) Our results are based on methods from linear algebra and convex/polyhedral geometry, and the solution set on P can be further studied using methods from analysis such as sign-characteristic functions (introduced in this work). We illustrate our results (in particular, the relevant geometric objects) through three examples from real fewnomial and reaction network theory. For two mass-action systems, we parametrize the set of equilibria and the region for multistationarity, respectively, and even for univariate trinomials, we offer new insights: We provide a “solution formula” involving discriminants and “roots”.},
journal = {Positivity},
volume = {30},
number = {4},
pages = {0--0},
isbn_issn = {1385-1292},
year = {2026},
refereed = {yes},
length = {26},
url = {https://link.springer.com/article/10.1007/s11117-025-01158-4}
}