Abstract. It it shown that the first-order theory of an automatic structure, whose Gaifman graph has bounded degree, is decidable in doubly exponential space (for injective automa...
We define strong monads of continuous (lower, upper) previsions, and of forks, modeling both probabilistic and non-deterministic choice. This is an elegant alternative to recent p...
Abstract. We present a method of integrating linear rational arithmetic into superposition calculus for first-order logic. One of our main results is completeness of the resulting...
We provide a new correctness criterion for unit-free MLL proof structures and MELL proof structures with units. We prove that deciding the correctness of a MLL and of a MELL proof ...
We study the complexity of model-checking for the fixpoint extension of Hintikka and Sandu’s independence-friendly logic. We show that this logic captures ExpTime; and by embedd...