Search ACM DL

Search Issue

enter search term and/or author name

**A PSPACE-complete first-order fragment of computability logic**

Matthew S. Bauer

Article No.: 1

DOI: 10.1145/2559949

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...

**Improved witnessing and local improvement principles for second-order bounded arithmetic**

Arnold Beckmann, Samuel R. Buss

Article No.: 2

DOI: 10.1145/2559950

This article concerns the second-order systems U^{1}_{2} and V^{1}_{2} of bounded arithmetic, which have proof-theoretic strengths corresponding to polynomial-space and exponential-time computation. We formulate...

**Algebra-coalgebra duality in brzozowski's minimization algorithm**

Filippo Bonchi, Marcello M. Bonsangue, Helle H. Hansen, Prakash Panangaden, Jan J. M. M. Rutten, Alexandra Silva

Article No.: 3

DOI: 10.1145/2490818

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...

**Non-finite axiomatizability of dynamic topological logic**

David Fernández-Duque

Article No.: 4

DOI: 10.1145/2489334

*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* →...

**Quantifier-free interpolation in combinations of equality interpolating theories**

Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise

Article No.: 5

DOI: 10.1145/2490253

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...

**Degree lower bounds of tower-type for approximating formulas with parity quantifiers**

Albert Atserias, Anuj Dawar

Article No.: 6

DOI: 10.1145/2559948

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...

**Using tableau to decide description logics with full role negation and identity**

Renate A. Schmidt, Dmitry Tishkovsky

Article No.: 7

DOI: 10.1145/2559947

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...

**Extending two-variable logic on data trees with order on data values and its automata**

Tony Tan

Article No.: 8

DOI: 10.1145/2559945

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...

**On the complexity of existential positive queries**

Hubie Chen

Article No.: 9

DOI: 10.1145/2559946

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...

**A resolution calculus for the branching-time temporal logic CTL**

Lan Zhang, Ullrich Hustadt, Clare Dixon

Article No.: 10

DOI: 10.1145/2529993

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...