Computational Logic (TOCL)


Search Issue
enter search term and/or author name


ACM Transactions on Computational Logic (TOCL), Volume 3 Issue 1, January 2002

The intuitionism behind Statecharts steps
Gerald Lüttgen, Michael Mendler
Pages: 1-41
DOI: 10.1145/504077.504078
The semantics of Statecharts macro steps, as introduced by Pnueli and Shalev [1991], lacks compositionality. This article first analyzes the compositionality problem and traces it back to the invalidity of the Law of the Excluded Middle. It then...

Datalog LITE: a deductive query language with linear time model checking
Georg Gottlob, Erich Grädel, Helmut Veith
Pages: 42-79
DOI: 10.1145/504077.504079
We present Datalog LITE, a new deductive query language with a linear-time model-checking algorithm, that is, linear time data complexity and program complexity. Datalog LITE is a variant of Datalog that uses stratified negation, restricted variable...

Reasoning with higher-order abstract syntax in a logical framework
Raymond C. McDowell, Dale A. Miller
Pages: 80-136
DOI: 10.1145/504077.504080
Logical frameworks based on intuitionistic or linear logics with higher-type quantification have been successfully used to give high-level, modular, and formal specifications of many important judgments in the area of programming languages and...

Intuitionistic Light Affine Logic
Andrea Asperti, Luca Roversi
Pages: 137-175
DOI: 10.1145/504077.504081
This article is a structured introduction to Intuitionistic Light Affine Logic (ILAL). ILAL has a polynomially costing normalization, and it is expressive enough to encode, and simulate, all PolyTime Turing machines. The bound on...