ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 11 Issue 3, May 2010

A fast algorithm and datalog inexpressibility for temporal reasoning
Manuel Bodirsky, Jan Kára
Article No.: 15
DOI: 10.1145/1740582.1740583

We introduce a new tractable temporal constraint language, which strictly contains the Ord-Horn language of Bürkert and Nebel and the class of AND/OR precedence constraints. The algorithm we present for this language decides whether a given...

On the completeness of compositional reasoning methods
Kedar S. Namjoshi, Richard J. Trefler
Article No.: 16
DOI: 10.1145/1740582.1740584

Hardware systems and reactive software systems can be described as the composition of several concurrently active processes. Automated reasoning based on model checking algorithms can substantially increase confidence in the overall reliability of...

Deciding strategy properties of contract-signing protocols
Detlef Kähler, Ralf Küsters, Thomas Wilke
Article No.: 17
DOI: 10.1145/1740582.1740585

Research on the automatic analysis of cryptographic protocols has so far concentrated on reachability properties, such as secrecy and authentication. In this article, we prove that certain game-theoretic security properties, including balance for...

Complexity of propositional proofs under a promise
Nachum Dershowitz, Iddo Tzameret
Article No.: 18
DOI: 10.1145/1740582.1740586

We study—within the framework of propositional proof complexity—the problem of certifying unsatisfiability of CNF formulas under the promise that any satisfiable formula has many satisfying assignments, where many stands for an...

Lower bounds for bounded depth Frege proofs via Pudlák-Buss games
Eli Ben-Sasson, Prahladh Harsha
Article No.: 19
DOI: 10.1145/1740582.1740587

We present a simple proof of the bounded-depth Frege proof lower bounds of Pitassi et al. [1993] and Krajíček et al. [1995] for the pigeonhole principle. Our method uses the interpretation of proofs as two player games given by...

On the distributivity of LTL specifications
Marko Samer, Helmut Veith
Article No.: 20
DOI: 10.1145/1740582.1740588

In this article, we investigate LTL specifications where γ[ϕ ∧ ψ] is equivalent to γ[ϕ] ∧ γ[ψ] independent of ϕ and ψ. Formulas γ with this property are called distributive queries...