enter search term and/or author name
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
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
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
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 λδ 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
Article No.: 6
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
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...