Computational Logic (TOCL)


Search Issue
enter search term and/or author name


ACM Transactions on Computational Logic (TOCL), Volume 8 Issue 1, January 2007

A system of interaction and structure
Alessio Guglielmi
Article No.: 1
DOI: 10.1145/1182613.1182614
This article introduces a logical system, called BV, which extends multiplicative linear logic by a noncommutative self-dual logical operator. This extension is particularly challenging for the sequent calculus, and so far, it is not achieved...

Compilability of propositional abduction
Paolo Liberatore, Marco Schaerf
Article No.: 2
DOI: 10.1145/1182613.1182615
Abduction is one of the most important forms of reasoning; it has been successfully applied to several practical problems, such as diagnosis. In this article we investigate whether the computational complexity of abduction can be reduced by an...

Results on the quantitative μ-calculus qMμ
Annabelle McIver, Carroll Morgan
Article No.: 3
DOI: 10.1145/1182613.1182616
The μ-calculus is a powerful tool for specifying and verifying transition systems, including those with both demonic (universal) and angelic (existential) choice; its quantitative generalization qMμ extends to include...

On compositionality and its limitations
Alexander Rabinovich
Article No.: 4
DOI: 10.1145/1182613.1182617
The aim of this article is to examine the applicability of a compositional method developed for a generalized product construction by Feferman and Vaught to the field of program verification.We suggest an instance of the generalized product...

Logical characterizations of heap abstractions
Greta Yorsh, Thomas Reps, Mooly Sagiv, Reinhard Wilhelm
Article No.: 5
DOI: 10.1145/1182613.1182618
Shape analysis concerns the problem of determining “shape invariants” for programs that perform destructive updating on dynamically allocated storage. In recent work, we have shown how shape analysis can be performed using an abstract...

Abstract canonical inference
Maria Paola Bonacina, Nachum Dershowitz
Article No.: 6
DOI: 10.1145/1182613.1182619
An abstract framework of canonical inference is used to explore how different proof orderings induce different variants of saturation and completeness. Notions like completion, paramodulation, saturation, redundancy elimination, and rewrite-system...

Erratum to splitting an operator: Algebraic modularity results for logics with fixpoint semantics
Joost Vennekens, David Gilis, Marc Denecker
Article No.: 7
DOI: 10.1145/1182613.1189735