ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 13 Issue 3, August 2012

The dynamic complexity of formal languages
Wouter Gelade, Marcel Marquardt, Thomas Schwentick
Article No.: 19
DOI: 10.1145/2287718.2287719

The article investigates the power of the dynamic complexity classes DynFO, DynQF, and DynPROP over string languages. The latter two classes contain problems that can be maintained using quantifier-free first-order...

Permissive-nominal logic: First-order logic over nominal terms and sets
Gilles Dowek, Murdoch J. Gabbay
Article No.: 20
DOI: 10.1145/2287718.2287720

Permissive-Nominal Logic (PNL) is an extension of first-order predicate logic in which term-formers can bind names in their arguments.

This allows for direct axiomatizations with binders, such as of the λ-binder of the...

LTL over description logic axioms
Franz Baader, Silvio Ghilardi, Carsten Lutz
Article No.: 21
DOI: 10.1145/2287718.2287721

Most of the research on temporalized Description Logics (DLs) has concentrated on the case where temporal operators can be applied to concepts, and sometimes additionally to TBox axioms and ABox assertions. The aim of this article is to study...

Calculus of cooperation and game-based reasoning about protocol privacy
Sara Miner More, Pavel Naumov
Article No.: 22
DOI: 10.1145/2287718.2287722

The article introduces a new formal system, the calculus of cooperation, for reasoning about coalitions of players in a certain class of games. The calculus is an extension of the propositional intuitionistic logic that adds a coalition parameter...

Deductive inference for the interiors and exteriors of horn theories
Kazuhisa Makino, Hirotaka Ono
Article No.: 23
DOI: 10.1145/2287718.2287723

In this article, we investigate deductive inference for interiors and exteriors of Horn knowledge bases, where interiors and exteriors were introduced by Makino and Ibaraki [1996] to study stability properties of knowledge bases. We present a...

Arithmetic complexity via effective names for random sequences
Bjørn Kjos-Hanssen, Frank Stephan, Jason Teutsch
Article No.: 24
DOI: 10.1145/2287718.2287724

We investigate enumerability properties for classes of sets which permit recursive, lexicographically increasing approximations, or left-r.e. sets. In addition to pinpointing the complexity of left-r.e. Martin-Löf, computably, Schnorr,...

Graded computation tree logic
Alessandro Bianco, Fabio Mogavero, Aniello Murano
Article No.: 25
DOI: 10.1145/2287718.2287725

In modal logics, graded (world) modalities have been deeply investigated as a useful framework for generalizing standard existential and universal modalities in such a way that they can express statements about a given number of immediately...

Well-structured program equivalence is highly undecidable
Robert Goldblatt, Marcel Jackson
Article No.: 26
DOI: 10.1145/2287718.2287726

We show that strict deterministic propositional dynamic logic with intersection is highly undecidable, solving a problem in the Stanford Encyclopedia of Philosophy. In fact we show something quite a bit stronger. We introduce the construction of...

Algorithmic analysis of array-accessing programs
Rajeev Alur, Pavol Černý, Scott Weinstein
Article No.: 27
DOI: 10.1145/2287718.2287727

For programs whose data variables range over Boolean or finite domains, program verification is decidable, and this forms the basis of recent tools for software model checking. In this article, we consider algorithmic verification of programs that...