Computational Logic (TOCL)


Search Issue
enter search term and/or author name


ACM Transactions on Computational Logic (TOCL), Volume 11 Issue 1, October 2009

Finitary winning in ω-regular games
Krishnendu Chatterjee, Thomas A. Henzinger, Florian Horn
Article No.: 1
DOI: 10.1145/1614431.1614432

Games on graphs with ω-regular objectives provide a model for the control and synthesis of reactive systems. Every ω-regular objective can be decomposed into a safety part and a liveness part. The liveness part ensures that something...

Automated termination proofs for logic programs by term rewriting
Peter Schneider-Kamp, Jürgen Giesl, Alexander Serebrenik, René Thiemann
Article No.: 2
DOI: 10.1145/1614431.1614433

There are two kinds of approaches for termination analysis of logic programs: “transformational” and “direct” ones. Direct approaches prove termination directly on the basis of the logic program. Transformational approaches...

Tableau-based decision procedures for logics of strategic ability in multiagent systems
Valentin Goranko, Dmitry Shkatov
Article No.: 3
DOI: 10.1145/1614431.1614434

We develop an incremental tableau-based decision procedure for the alternating-time temporal logic ATL and some of its variants. While running within the theoretically established complexity upper bound, we believe that our tableaux are...

Regular tree languages definable in FO and in FOmod
Michael Benedikt, Luc Segoufin
Article No.: 4
DOI: 10.1145/1614431.1614435

We consider regular languages of labeled trees. We give an effective characterization of the regular languages over such trees that are definable in first-order logic in the language of labeled graphs. These languages are the analog on trees of...

The formal system λδ
Ferruccio Guidi
Article No.: 5
DOI: 10.1145/1614431.1614436

The formal system λδ is a typed λ-calculus that pursues the unification of terms, types, environments, and contexts as the main goal. λδ takes some features from the Automath-related λ-calculi and some from...

Higher-order term indexing using substitution trees
Brigitte Pientka
Article No.: 6
DOI: 10.1145/1614431.1614437

We present a higher-order term indexing strategy based on substitution trees for simply typed lambda-terms. There are mainly two problems in adapting first-order indexing techniques. First, many operations used in building an efficient term index...

A general framework for sound and complete Floyd-Hoare logics
Rob Arthan, Ursula Martin, Erik A. Mathiesen, Paulo Oliva
Article No.: 7
DOI: 10.1145/1614431.1614438

This article presents an abstraction of Hoare logic to traced symmetric monoidal categories, a very general framework for the theory of systems. Our abstraction is based on a traced monoidal functor from an arbitrary traced monoidal category into...