ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 2 Issue 2, April 2001

A decision procedure for term algebras with queues

Pages: 155-181
DOI: 10.1145/371316.371494
In software verification it is often required to prove statements about heterogeneous domains containing elements of various sorts, such as counters, stacks, lists, trees and queues. Any domain with counters, stacks, lists, and trees (but not...

How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi
Andrei Voronkov
Pages: 182-215
DOI: 10.1145/371316.371511
We present a bottom-up decision procedure for propositional modal logic K based on the inverse method. The procedure is based on the “inverted” version of a sequent calculus. To restrict the search space, we prove a number of...

MSO definable string transductions and two-way finite-state transducers
Joost Engelfriet, Hendrik Jan Hoogeboom
Pages: 216-254
DOI: 10.1145/371316.371512
We extend a classic result of Büchi, Elgot, and Trakhtenbrot: MSO definable string transductions i.e., string-to-string functions that are definable by an interpretation using monadic second-order (MSO) logic, are exactly those realized by...

Representation results for defeasible logic
Grigoris Antoniou, David Billington, Guido Governatori, Michael J. Maher
Pages: 255-287
DOI: 10.1145/371316.371517
The importance of transformations and normal forms in logic programming, and generally in computer science, is well documented. This paper investigates transformations and normal forms in the context of Defeasible Logic, a simple but efficient...