2 papers
cs.LO2026
MCSAT Modulo Transcendental Arithmetics
Jorge Gallego-Hernández, Enrico Lipparini, Alessio Mansutti
We propose a framework for solving quantifier-free formulas from (undecidable) extensions of non-linear real arithmetic (NRA) with transcendental functions, such as exponential and…
cs.LO2025
On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number
Jorge Gallego-Hernández, Alessio Mansutti
This paper investigates , that is the extension of the existential theory of the reals by an additional unary predicate for the…