Computational Logic (TOCL)


Search Issue
enter search term and/or author name


ACM Transactions on Computational Logic (TOCL), Volume 13 Issue 1, January 2012

Robust Vacuity for Branching Temporal Logic
Arie Gurfinkel, Marsha Chechik
Article No.: 1
DOI: 10.1145/2071368.2071369

There is a growing interest in techniques for detecting whether a logic specification is satisfied too easily, or vacuously. For example, the specification “every request is eventually followed by an acknowledgment” is satisfied...

Least and Greatest Fixed Points in Linear Logic
David Baelde
Article No.: 2
DOI: 10.1145/2071368.2071370

The first-order theory of MALL (multiplicative, additive linear logic) over only equalities is a well-structured but weak logic since it cannot capture unbounded (infinite) behavior. Instead of accounting for unbounded behavior via the addition of...

Topological and Simplicial Models of Identity Types
Benno van den Berg, Richard Garner
Article No.: 3
DOI: 10.1145/2071368.2071371

In this paper we construct new categorical models for the identity types of Martin-Löf type theory, in the categories Top of topological spaces and SSet of simplicial sets. We do so building on earlier work of Awodey and Warren...

Succinctness of the Complement and Intersection of Regular Expressions
Wouter Gelade, Frank Neven
Article No.: 4
DOI: 10.1145/2071368.2071372

We study the succinctness of the complement and intersection of regular expressions. In particular, we show that when constructing a regular expression defining the complement of a given regular expression, a double exponential size increase...

The Complexity of Positive First-Order Logic without Equality
Florent Madelaine, Barnaby Martin
Article No.: 5
DOI: 10.1145/2071368.2071373

We study the complexity of evaluating positive equality-free sentences of first-order (FO) logic over a fixed, finite structure B. This may be seen as a natural generalisation of the nonuniform quantified constraint satisfaction problem...

On the Expressive Power of Multiple Heads in CHR
Cinzia Di Giusto, Maurizio Gabbrielli, Maria Chiara Meo
Article No.: 6
DOI: 10.1145/2071368.2071374

Constraint Handling Rules (CHR) is a committed-choice declarative language that has been originally designed for writing constraint solvers and is nowadays a general purpose language. CHR programs consist of multiheaded guarded rules which allow...

Reachability Problems in Piecewise FIFO Systems
Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, Richard Trefler
Article No.: 7
DOI: 10.1145/2071368.2071375

Systems consisting of several finite components that communicate via unbounded perfect FIFO channels (i.e., FIFO systems) arise naturally in modeling distributed systems. Despite well-known difficulties in analyzing such systems, they are of...

Structural Analysis of Boolean Equation Systems
Jeroen J. A. Keiren, Michel A. Reniers, Tim A. C. Willemse
Article No.: 8
DOI: 10.1145/2071368.2071376

We analyze the problem of solving Boolean equation systems through the use of structure graphs. The latter are obtained through an elegant set of Plotkin-style deduction rules. Our main contribution is that we show that equation systems...

The Complexity of Proving the Discrete Jordan Curve Theorem
Phuong Nguyen, Stephen Cook
Article No.: 9
DOI: 10.1145/2071368.2071377

The Jordan curve theorem (JCT) states that a simple closed curve divides the plane into exactly two connected regions. We formalize and prove the theorem in the context of grid graphs, under different input settings, in theories of bounded...