Computational Logic (TOCL)


Search Issue
enter search term and/or author name


ACM Transactions on Computational Logic (TOCL), Volume 17 Issue 2, March 2016

Effective Interpolation and Preservation in Guarded Logics
Michael Benedikt, Balder Ten Cate, Michael Vanden Boom
Article No.: 8
DOI: 10.1145/2814570

Desirable properties of a logic include decidability, and a model theory that inherits properties of first-order logic, such as interpolation and preservation theorems. It is known that the Guarded Fragment (GF) of first-order logic is decidable...

Belief Merging by Examples
Paolo Liberatore
Article No.: 9
DOI: 10.1145/2818645

A common assumption in belief revision is that the reliability of the information sources is either given, derived from temporal information, or the same for all. This article does not describe a new semantics for integration but studies the...

Model Checking Existential Logic on Partially Ordered Sets
Simone Bova, Robert Ganian, Stefan Szeider
Article No.: 10
DOI: 10.1145/2814937

We study the problem of checking whether an existential sentence (i.e., a first-order sentence in prefix form built using existential quantifiers and all Boolean connectives) is true in a finite partially ordered set (a poset). A poset is a...

May-Happen-in-Parallel Analysis for Actor-Based Concurrency
Elvira Albert, Antonio Flores-Montoya, Samir Genaim, Enrique Martin-Martin
Article No.: 11
DOI: 10.1145/2824255

This article presents a may-happen-in-parallel (MHP) analysis for languages with actor-based concurrency. In this concurrency model, actors are the concurrency units such that, when a method is invoked on an actor...

Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction
Stephane Demri, Morgan Deters
Article No.: 12
DOI: 10.1145/2835490

Separation logic is used as an assertion language for Hoare-style proof systems about programs with pointers, and there is an ongoing quest for understanding its complexity and expressive power. Herein, we show that first-order separation logic...

The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion Schemes
Konstantinos Mamouras
Article No.: 13
DOI: 10.1145/2835491

The equational theory of deterministic monadic recursion schemes is known to be decidable by the result of Sénizergues on the decidability of the problem of DPDA equivalence. In order to capture some properties of the domain of computation,...

Limiting Until in Ordered Tree Query Languages
Michael Benedikt, Clemens Ley
Article No.: 14
DOI: 10.1145/2856104

Marx and de Rijke have shown that the navigational core of the w3c XML query language XPath is not first-order complete; that is, it cannot express every query definable in first-order logic over the navigational predicates. How can one extend...