enter search term and/or author name
Effective Interpolation and Preservation in Guarded Logics
Michael Benedikt, Balder Ten Cate, Michael Vanden Boom
Article No.: 8
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...
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
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
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
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
Article No.: 13
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,...
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...