Computational Logic (TOCL)


Search Issue
enter search term and/or author name


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

Sound and complete elimination of singleton kinds
Karl Crary
Article No.: 8
DOI: 10.1145/1227839.1227840

Singleton kinds provide an elegant device for expressing type equality information resulting from modern module languages, but they can complicate the metatheory of languages in which they appear. I present a translation from a language with...

Recycling computed answers in rewrite systems for abduction
Fangzhen Lin, Jia-Huai You
Article No.: 9
DOI: 10.1145/1227839.1227841

In rule-based systems, goal-oriented computations correspond naturally to the possible ways that an observation may be explained. In some applications, we need to compute explanations for a series of observations with the same domain. The question...

Where fail-safe default logics fail
Paolo Liberatore
Article No.: 10
DOI: 10.1145/1227839.1227842

Reiter's original definition of default logic allows for the application of a default that contradicts one previously applied. We call this condition failure. The possibility of generating failures has been in the past considered a...

Logical definability and query languages over ranked and unranked trees
Michael Benedikt, Leonid Libkin, Frank Neven
Article No.: 11
DOI: 10.1145/1227839.1227843

We study relations on trees defined by first-order constraints over a vocabulary that includes the tree extension relation TT′ (holding if and only if every branch of T extends to a branch of T′),...

On unification for bounded distributive lattices
Viorica Sofronie-Stokkermans
Article No.: 12
DOI: 10.1145/1227839.1227844

We give a method for deciding unifiability in the variety of bounded distributive lattices. For this, we reduce the problem of deciding whether a unification problem S has a solution to the problem of checking the satisfiability of a set...

The arithmetical complexity of dimension and randomness
John M. Hitchcock, Jack H. Lutz, Sebastiaan A. Terwijn
Article No.: 13
DOI: 10.1145/1227839.1227845

Constructive dimension and constructive strong dimension are effectivizations of the Hausdorff and packing dimensions, respectively. Each infinite binary sequence A is assigned a dimension dim(A) ∈ [0,1] and a strong...