ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 10 Issue 3, April 2009

Checking timed Büchi automata emptiness on simulation graphs
Stavros Tripakis
Article No.: 15
DOI: 10.1145/1507244.1507245

Timed automata [Alur and Dill 1994] comprise a popular model for describing real-time and embedded systems and reasoning formally about them. Efficient model-checking algorithms have been developed and implemented in tools such as Kronos [Daws et...

LTL with the freeze quantifier and register automata
Stéphane Demri, Ranko Lazić
Article No.: 16
DOI: 10.1145/1507244.1507246

A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. To reason about data words, linear temporal logic is extended by the freeze quantifier,...

Generalizing consistency and other constraint properties to quantified constraints
Lucas Bordeaux, Marco Cadoli, Toni Mancini
Article No.: 17
DOI: 10.1145/1507244.1507247

Quantified constraints and Quantified Boolean Formulae are typically much more difficult to reason with than classical constraints, because quantifier alternation makes the usual notion of solution inappropriate. As a consequence, basic...

Analytic tableaux calculi for KLM logics of nonmonotonic reasoning
Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato
Article No.: 18
DOI: 10.1145/1507244.1507248

We present tableau calculi for the logics of nonmonotonic reasoning defined by Kraus, Lehmann and Magidor (KLM). We give a tableau proof procedure for all KLM logics, namely preferential, loop-cumulative, cumulative, and rational logics. Our...

An algebra of quantum processes
Mingsheng Ying, Yuan Feng, Runyao Duan, Zhengfeng Ji
Article No.: 19
DOI: 10.1145/1507244.1507249

We introduce an algebra qCCS of pure quantum processes in which communications by moving quantum states physically are allowed and computations are modeled by super-operators, but no classical data is explicitly involved. An operational semantics...

Simultaneous checking of completeness and ground confluence for algebraic specifications
Adel Bouhoula
Article No.: 20
DOI: 10.1145/1507244.1507250

Algebraic specifications provide a powerful method for the specification of abstract data types in programming languages and software systems. Completeness and ground confluence are fundamental notions for building algebraic specifications in a...

Tableau calculus for preference-based conditional logics: PCL and its extensions
Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Camilla Schwind
Article No.: 21
DOI: 10.1145/1507244.1507251

We present a tableau calculus for some fundamental systems of propositional conditional logics. We consider the conditional logics that can be characterized by preferential semantics (i.e., possible world structures equipped with a family...

Differential recursion
Akitoshi Kawamura
Article No.: 22
DOI: 10.1145/1507244.1507252

We present a redevelopment of the theory of real-valued recursive functions that was introduced by C. Moore in 1996 by analogy with the standard formulation of the integer-valued recursive functions. While his work opened a new line of research on...