ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 6 Issue 3, July 2005

Datalog programs and their persistency numbers
Foto Afrati, Stavros Cosmadakis, Eugénie Foustoucos
Pages: 481-518
DOI: 10.1145/1071596.1071597
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
Pages: 519-538
DOI: 10.1145/1071596.1071598
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
Matthew Stone
Pages: 539-577
DOI: 10.1145/1071596.1071599
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
Pages: 578-613
DOI: 10.1145/1071596.1071600
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
Pages: 614-633
DOI: 10.1145/1071596.1071601
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
Nicole Schweikardt
Pages: 634-671
DOI: 10.1145/1071596.1071602
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...