ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 11 Issue 2, January 2010

Logical queries over views: Decidability and expressiveness
James Bailey, Guozhu Dong, Anthony WIDJAJA To
Article No.: 8
DOI: 10.1145/1656242.1656243

We study the problem of deciding the satisfiability of first-order logic queries over views, with our aim to delimit the boundary between the decidable and the undecidable fragments of this language. Views currently occupy a central place in...

Deciding security properties for cryptographic protocols. application to key cycles
Hubert Comon-Lundh, Véronique Cortier, Eugen Zălinescu
Article No.: 9
DOI: 10.1145/1656242.1656244

There is a large amount of work dedicated to the formal verification of security protocols. In this article, we revisit and extend the NP-complete decision procedure for a bounded number of sessions. We use a, now standard, deducibility constraint...

Annotated RDF
Octavian Udrea, Diego Reforgiato Recupero, V. S. Subrahmanian
Article No.: 10
DOI: 10.1145/1656242.1656245

Real-world use of RDF requires the ability to transparently represent and explain metadata associated with RDF triples. For example, when RDF triples are extracted automatically by information extraction programs, there is a need to represent...

Weyl's predicative classical mathematics as a logic-enriched type theory
Robin Adams, Zhaohui Luo
Article No.: 11
DOI: 10.1145/1656242.1656246

We construct a logic-enriched type theory LTTW that corresponds closely to the predicative system of foundations presented by Hermann Weyl in Das Kontinuum. We formalize many results from that book in LTTW, including...

Undecidability and intractability results concerning datalog programs and their persistency numbers
Stavros Cosmadakis, Eugenie Foustoucos, Anastasios Sidiropoulos
Article No.: 12
DOI: 10.1145/1656242.1656247

The relation between Datalog programs and homomorphism problems, and, between Datalog programs and bounded treewidth structures has been recognized for some time and given much attention recently. Additionally, the essential role of persistent...

Proof search specifications of bisimulation and modal logics for the π-calculus
Alwen Tiu, Dale Miller
Article No.: 13
DOI: 10.1145/1656242.1656248

We specify the operational semantics and bisimulation relations for the finite π-calculus within a logic that contains the ∇ quantifier for encoding generic judgments and definitions for encoding fixed points. Since we restrict to...

FDNC: Decidable nonmonotonic disjunctive logic programs with function symbols
Thomas Eiter, Mantas Šimkus
Article No.: 14
DOI: 10.1145/1656242.1656249

We present the class FDNC of logic programs that allows for function symbols (F), disjunction (D), nonmonotonic negation under the answer set semantics (N), and constraints (C), while still retaining the decidability of the standard reasoning...