ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 15 Issue 1, February 2014

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 U12 and V12 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 ALBOid, 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...