ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 1 Issue 1, July 2000

Mechanizing UNITY in Isabelle
Lawrence C. Paulson
Pages: 3-32
DOI: 10.1145/343369.343370
UNITY is an abstract formalism for proving properties of concurrent systems, which typically are expressed using guarded assignments [Chandy and Misra 1988]. UNITY has been mechanized in higher-order logic using Isabelle, a proof assistant....

Logics with counting and local properties
Leonid Libkin
Pages: 33-59
DOI: 10.1145/343369.343376
The expressive power of first-order logic over finite structures is limited in two ways: it lacks a recursion mechanism, and it cannot count. Overcoming the first limitation has been a subject of extensive study. A number of fixpoint logics have...

On Hoare logic and Kleene algebra with tests
Dexter Kozen
Pages: 60-76
DOI: 10.1145/343369.343378
We show that Kleene algebra with tests (KAT) subsumes propositional Hoare logic (PHL). Thus the specialized syntax and deductive apparatus of Hoare logic are inessential and can be replaced by simple equational reasoning. In addition, we show...

Sequential abstract-state machines capture sequential algorithms
Yuri Gurevich
Pages: 77-111
DOI: 10.1145/343369.343384
We examine sequential algorithms and formulate a sequential-time postulate, an abstract-state postulate, and a bounded-exploration postulate . Analysis of the postulates leads us to the notion of sequential abstract-state machine and to the...

Locality of order-invariant first-order formulas
Martin Grohe, Thomas Schwentick
Pages: 112-130
DOI: 10.1145/343369.343386
A query is local if the decision of whether a tuple in a structure satisfies this query only depends on a small neighborhood of the tuple. We prove that all queries expressible by order-invariant first-order...

Compilability and compact representations of revision of Horn knowledge bases
Paolo Liberatore
Pages: 131-161
DOI: 10.1145/343369.343391
Several methods have been proposed as an attempt to deal with dynamically changing scenarios. From a computational point of view, different formalisms have different computational properties. In this article we consider knowledge bases...

Model-checking continuous-time Markov chains
Adnan Aziz, Kumud Sanwal, Vigyan Singhal, Robert Brayton
Pages: 162-170
DOI: 10.1145/343369.343402
We present a logical formalism for expressing properties of continuous-time Markov chains. The semantics for such properties arise as a natural extension of previous work on discrete-time Markov chains to continuous time. The major result is...

A note on the complexity of propositional Hoare logic
Ernie Cohen, Dexter Kozen
Pages: 171-174
DOI: 10.1145/343369.343404
We provide a simpler alternative proof of the PSPACE-hardness of propositional Hoare logic (PHL).