ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 9 Issue 3, June 2008

A uniform approach to constraint-solving for lists, multisets, compact lists, and sets
Agostino Dovier, Carla Piazza, Gianfranco Rossi
Article No.: 15
DOI: 10.1145/1352582.1352583

Lists, multisets, and sets are well-known data structures whose usefulness is widely recognized in various areas of computer science. They have been analyzed from an axiomatic point of view with a parametric approach in Dovier et al....

Foundational certified code in the Twelf metalogical framework
Karl Crary, Susmit Sarkar
Article No.: 16
DOI: 10.1145/1352582.1352584

Foundational certified code systems seek to prove untrusted programs to be safe relative to safety policies given in terms of actual machine architectures, thereby improving the systems' flexibility and extensibility. Using the Twelf metalogical...

Inferring non-suspension conditions for logic programs with dynamic scheduling
Samir Genaim, Andy King
Article No.: 17
DOI: 10.1145/1352582.1352585

A logic program consists of a logic component and a control component. The former is a specification in predicate logic whereas the latter defines the order of subgoal selection. The order of subgoal selection is often controlled with delay...

Program termination and well partial orderings
Andreas Blass, Yuri Gurevich
Article No.: 18
DOI: 10.1145/1352582.1352586

The following known observation is useful in establishing program termination: if a transitive relation R is covered by finitely many well-founded relations U1,…,Un then R is well-founded. A...

Abstract state machines capture parallel algorithms: Correction and extension
Andreas Blass, Yuri Gurevich
Article No.: 19
DOI: 10.1145/1352582.1352587

We consider parallel algorithms working in sequential global time, for example, circuits or parallel random access machines (PRAMs). Parallel abstract state machines (parallel ASMs) are such parallel algorithms, and the parallel ASM thesis asserts...

What causes a system to satisfy a specification?
Hana Chockler, Joseph Y. Halpern, Orna Kupferman
Article No.: 20
DOI: 10.1145/1352582.1352588

Even when a system is proven to be correct with respect to a specification, there is still a question of how complete the specification is, and whether it really covers all the behaviors of the system. Coverage metrics attempt to check...

Proof search in Hájek's basic logic
Simone Bova, Franco Montagna
Article No.: 21
DOI: 10.1145/1352582.1352589

We introduce a proof system for Hájek's logic BL based on a relational hypersequents framework. We prove that the rules of our logical calculus, called RHBL, are sound and invertible with respect to any valuation of BL...

Conjunctive query containment and answering under description logic constraints
Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini
Article No.: 22
DOI: 10.1145/1352582.1352590

Query containment and query answering are two important computational tasks in databases. While query answering amounts to computing the result of a query over a database, query containment is the problem of checking whether, for every database,...

Contextual modal type theory
Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka
Article No.: 23
DOI: 10.1145/1352582.1352591

The intuitionistic modal logic of necessity is based on the judgmental notion of categorical truth. In this article we investigate the consequences of relativizing these concepts to explicitly specified contexts. We obtain contextual modal logic...