9 papers
Abstract Compilation as Abstraction of Operator Semantics, applied to Cost Analysis
Louis Rustenholz, Alessio Mansutti, Pedro López-García +3
Least fixpoints are fundamental to program semantics, but they abstract away the recursive structure that generated them. We introduce operator semantics: a semantic intermediate r…
Towards an Automated Reasoning Tool for Complexity Analysis of Automated Reasoners
Louis Rustenholz, Manuel V. Hermenegildo, Pedro Lopez-Garcia +3
We present the theory underpinning a complexity analysis tool (under development) that aims at automating tedious parts of the analysis of complex algorithms originating from the f…
How (and when) can you fit examples to logic-based hypothesis classes over infinite structures?
Michael Benedikt, Alessio Mansutti
We study fitting problems, sometimes called ``training problems'', where we have a finite sample consisting of inputs and outputs, and we want to know whether there is a function i…
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…
The complexity of Presburger arithmetic with power or powers
Michael Benedikt, Dmitry Chistikov, Alessio Mansutti
We investigate expansions of Presburger arithmetic, i.e., the theory of the integers with addition and order, with additional structure related to exponentiation: either a function…
On Polynomial-Time Decidability of k-Negations Fragments of First-Order Theories
Christoph Haase, Alessio Mansutti, Amaury Pouly
This paper introduces a generic framework that provides sufficient conditions for guaranteeing polynomial-time decidability of fixed-negation fragments of first-order theories that…