Computational Logic (TOCL)


Search Issue
enter search term and/or author name


ACM Transactions on Computational Logic (TOCL), Volume 2 Issue 1, Jan. 2001

Inadequacy of computable loop invariants
Andreas Blass, Yuri Gurevich
Pages: 1-11
DOI: 10.1145/371282.371285
Hoare logic is a widely recommended verification tool. There is, however, a problem of finding easily checkable loop invariants; it is known that decidable assertions do not suffice to verify while programs, even when the pre- and postconditions...

Clausal temporal resolution
Michael Fisher, Clare Dixon, Martin Peim
Pages: 12-56
DOI: 10.1145/371282.371311
In this article, we examine how clausal resolution can be applied to a specific, but widely used, nonclassical logic, namely discrete linear temporal logic. Thus, we first define a normal form for temporal formulae and show how arbitrary...

Termination proofs for logic programs with tabling
Sofie Verbaeten, Danny De Schreye, Konstantinos Sagonas
Pages: 57-92
DOI: 10.1145/371282.371357
Tabled evaluation is receiving increasing attention in the logic programming community. It avoids many of the shortcomings of SLD execution and provides a more flexible and often considerably more efficient execution mechanism for logic...

Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
Randal E. Bryant, Steven German, Miroslav N. Velev
Pages: 93-134
DOI: 10.1145/371282.371364
The logic of Equality with Uninterpreted Functions (EUF) provides a means of abstracting the manipulation of data by a processor when verifying the correctness of its control logic. By reducing formulas in this logic to propositional formulas,...

Logics capturing local properties
Leonid Libkin
Pages: 135-153
DOI: 10.1145/371282.371388
Well-known theorems of Hanf and Gaifman establishing locality of first-order definable properties have been used in many applications. These theorems were recently generalized to other logics, which led to new applications in descriptive...