Computational Logic (TOCL)


Search Issue
enter search term and/or author name


ACM Transactions on Computational Logic (TOCL), Volume 10 Issue 2, February 2009

The geometry of linear higher-order recursion
Ugo Dal Lago
Article No.: 8
DOI: 10.1145/1462179.1462180

Imposing linearity and ramification constraints allows to weaken higher-order (primitive) recursion in such a way that the class of representable functions equals the class of polynomial-time computable functions, as the works by Leivant, Hofmann,...

Probabilistic bisimulation as a congruence
Ruggero Lanotte, Simone Tini
Article No.: 9
DOI: 10.1145/1462179.1462181

We propose both an SOS transition rule format for the generative model of probabilistic processes, and an SOS transition rule format for the reactive model of the probabilistic processes. Our rule formats guarantee that probabilistic bisimulation...

Termination of rewriting under strategies
Isabelle Gnaedig, Hélène Kirchner
Article No.: 10
DOI: 10.1145/1462179.1462182

A termination proof method for rewriting under strategies, based on an explicit induction on the termination property, is presented and instantiated for the innermost, outermost, and local strategies. Rewriting trees are simulated by proof trees...

A compositional semantics for CHR
Maurizio Gabbrielli, Maria Chiara Meo
Article No.: 11
DOI: 10.1145/1462179.1462183

Constraint Handling Rules (CHR) is a committed-choice declarative language which has been designed for writing constraint solvers. A CHR program consists of multiheaded guarded rules which allow to rewrite constraints into simpler ones until a...

Proofs, tests and continuation passing style
Stefano Guerrini, Andrea Masini
Article No.: 12
DOI: 10.1145/1462179.1462184

The concept of syntactical duality is central in logic. In particular, the duality defined by classical negation, or more syntactically by left and right in sequents, has been widely used to relate logic and computations. We study the...

PSPACE bounds for rank-1 modal logics
LUTZ Schröder, Dirk Pattinson
Article No.: 13
DOI: 10.1145/1462179.1462185

For lack of general algorithmic methods that apply to wide classes of logics, establishing a complexity bound for a given modal logic is often a laborious task. The present work is a step towards a general theory of the complexity of modal logics....

On the proof complexity of deep inference
Paola Bruscoli, Alessio Guglielmi
Article No.: 14
DOI: 10.1145/1462179.1462186

We obtain two results about the proof complexity of deep inference: (1) Deep-inference proof systems are as powerful as Frege ones, even when both are extended with the Tseitin extension rule or with the substitution rule; (2) there are analytic...