Computational Logic (TOCL)


Search Issue
enter search term and/or author name


ACM Transactions on Computational Logic (TOCL), Volume 18 Issue 1, April 2017

Parametrised Complexity of Satisfiability in Temporal Logic
Martin Lück, Arne Meier, Irena Schindler
Article No.: 1
DOI: 10.1145/3001835

We apply the concept of formula treewidth and pathwidth to computation tree logic, linear temporal logic, and the full branching time logic. Several representations of formulas as graphlike structures are discussed, and corresponding notions of...

Quantified Constraint Satisfaction Problem on Semicomplete Digraphs
Petar Đapić, Petar Marković, Barnaby Martin
Article No.: 2
DOI: 10.1145/3007899

We study the (non-uniform) quantified constraint satisfaction problem QCSP(H) as H ranges over semicomplete digraphs. We obtain a complexity-theoretic trichotomy: QCSP(H) is either in P, is NP-complete, or is Pspace-complete....

A Hoare Logic for GPU Kernels
Kensuke Kojima, Atsushi Igarashi
Article No.: 3
DOI: 10.1145/3001834

We study a Hoare Logic to reason about parallel programs executed on graphics processing units (GPUs), called GPU kernels. During the execution of GPU kernels, multiple threads execute in lockstep, that is, execute the same instruction...

Equations, Contractions, and Unique Solutions
Davide Sangiorgi
Article No.: 4
DOI: 10.1145/2971339

One of the most studied behavioural equivalences is bisimilarity. Its success is much due to the associated bisimulation proof method, which can be further enhanced by means of “bisimulation up-to” techniques such as “up-to...

Datalog Queries Distributing over Components
Tom J. Ameloot, Bas Ketsman, Frank Neven, Daniel Zinn
Article No.: 5
DOI: 10.1145/3022743

We investigate the class D of queries that distribute over components. These are the queries that can be evaluated by taking the union of the query results over the connected components of the database instance. We show that it is...

Merging in the Horn Fragment
Adrian Haret, Stefan Rümmele, Stefan Woltran
Article No.: 6
DOI: 10.1145/3043700

Belief merging is a central operation within the field of belief change and addresses the problem of combining multiple, possibly mutually inconsistent knowledge bases into a single, consistent one. A current research trend in belief change is...

Abstract Program Slicing: An Abstract Interpretation-Based Approach to Program Slicing
Isabella Mastroeni, Damiano Zanardini
Article No.: 7
DOI: 10.1145/3029052

In the present article, we formally define the notion of abstract program slicing, a general form of program slicing where properties of data are considered instead of their exact value. This approach is applied to a language with numeric...