enter search term and/or author name
Datalog programs and their persistency numbers
Foto Afrati, Stavros Cosmadakis, Eugénie Foustoucos
The relation between Datalog programs and homomorphism problems and between Datalog programs and bounded treewidth structures has been recognized for some time and given much attention recently. Additionally, the essential role of persistent...
On the complexity of the disjunction property in intuitionistic and modal logics
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
In this article we study the complexity of disjunction property for intuitionistic logic, the modal logics S4, S4.1, Grzegorczyk logic, Gödel-Löb logic, and the intuitionistic counterpart of the modal logic K. For...
Disjunction and modular goal-directed proof search
This article explores goal-directed proof search in first-order multimodal logic. I focus on a family of modal logics which offer the expressive power to specify modular goals and local assumptions. A modular goal must be proved from designated...
Sequent and hypersequent calculi for abelian and łukasiewicz logics
George Metcalfe, Nicola Olivetti, Dov Gabbay
We present two embeddings of Łukasiewicz logic Ł into Meyer and Slaney's Abelian logic A, the logic of lattice-ordered Abelian groups. We give new analytic proof systems for A and use the embeddings to derive...
An effective decision procedure for linear arithmetic over the integers and reals
Bernard Boigelot, Sébastien Jodogne, Pierre Wolper
This article considers finite-automata-based algorithms for handling linear arithmetic with both real and integer variables. Previous work has shown that this theory can be dealt with by using finite automata on infinite words, but this involves some...
Arithmetic, first-order logic, and counting quantifiers
This article gives a thorough overview of what is known about first-order logic with counting quantifiers and with arithmetic predicates. As a main theorem we show that Presburger arithmetic is closed under unary counting quantifiers. Precisely, this...