ACM Transactions on Computational Logic

In a recently launched research program for developing logic as a formal theory of (interactive) computability, several very interesting logics have been introduced and axiomatized. These fragments of the larger Computability Logic aim not only to ...

This article concerns the second-order systems U¹₂ and V¹₂ of bounded arithmetic, which have proof-theoretic strengths corresponding to polynomial-space and exponential-time computation. We formulate improved witnessing theorems for these two theories ...

We give a new presentation of Brzozowski's algorithm to minimize finite automata using elementary facts from universal algebra and coalgebra and building on earlier work by Arbib and Manes on a categorical presentation of Kalman duality between ...

Dynamic topological logic (DTL) is a polymodal logic designed for reasoning about dynamic topological systems. These are pairs 〈 X, f〉, where X is a topological space and f:X → X is continuous. DTL uses a language L which combines the topological S4 ...

The use of interpolants in verification is gaining more and more importance. Since theories used in applications are usually obtained as (disjoint) combinations of simpler theories, it is important to modularly reuse interpolation algorithms for the ...

Kolaitis and Kopparty have shown that for any first-order formula with parity quantifiers over the language of graphs, there is a family of multivariate polynomials of constant-degree that agree with the formula on all but a 2^−Ω(n)-fraction of the ...

This article presents a tableau approach for deciding expressive description logics with full role negation and role identity. We consider the description logic ALBO^id, which is ALC extended with the Boolean role operators, inverse of roles, the ...

Data trees are trees in which each node, besides carrying a label from a finite alphabet, also carries a data value from an infinite domain. They have been used as an abstraction model for reasoning tasks on XML and verification. However, most existing ...

We systematically investigate the complexity of model checking the existential positive fragment of first-order logic. In particular, for a set of existential positive sentences, we consider model checking where the sentence is restricted to fall into ...

The branching-time temporal logic CTL is useful for specifying systems that change over time and involve quantification over possible futures. Here we present a resolution calculus for CTL that involves the translation of formulae to a normal form and ...