ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 6 Issue 1, January 2005

A classification of symbolic transition systems
Thomas A. Henzinger, Rupak Majumdar, Jean-François Raskin
Pages: 1-32
DOI: 10.1145/1042038.1042039
We define five increasingly comprehensive classes of infinite-state systems, called STS1--STS5, whose state spaces have finitary structure. For four of these classes, we provide examples from hybrid systems.STS1 These are the systems with finite...

Making abstract domains condensing
Roberto Giacobazzi, Francesco Ranzato, Francesca Scozzari
Pages: 33-60
DOI: 10.1145/1042038.1042040
In this article, we show that reversible analyses of logic languages by abstract interpretation can be performed without loss of precision by systematically refining abstract domains. This is obtained by adding to the abstract domain the minimal...

On equivalence and canonical forms in the LF type theory
Robert Harper, Frank Pfenning
Pages: 61-101
DOI: 10.1145/1042038.1042041
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality are based on a confluent, strongly normalizing...

A new decidability technique for ground term rewriting systems with applications
Rakesh Verma, Ara Hayrapetyan
Pages: 102-123
DOI: 10.1145/1042038.1042042
Programming language interpreters, proving equations (e.g. x3 = x implies the ring is Abelian), abstract data types, program transformation and optimization, and even computation itself (e.g., turing machine) can all be...

A modal logic framework for multi-agent belief fusion
Churn-Jung Liau
Pages: 124-174
DOI: 10.1145/1042038.1042043
This article provides a modal logic framework for reasoning about multi-agent belief and its fusion. We propose logics for reasoning about cautiously merged agent beliefs that have different degrees of reliability. These logics are obtained by...

Eternity variables to prove simulation of specifications
Wim H. Hesselink
Pages: 175-201
DOI: 10.1145/1042038.1042044
Simulations of specifications are introduced as a unification and generalization of refinement mappings, history variables, forward simulations, prophecy variables, and backward simulations. A specification implements another specification if and...