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 4, August 2008

Complexity results for security protocols with Diffie-Hellman exponentiation and commuting public key encryption
Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, Mathieu Turuani
Article No.: 24
DOI: 10.1145/1380572.1380573

We show that the insecurity problem for protocols with modular exponentiation and arbitrary products allowed in exponents is NP-complete. This result is based on a protocol and intruder model which is powerful enough to uncover known attacks on...

Undecidability of the unification and admissibility problems for modal and description logics
Frank Wolter, Michael Zakharyaschev
Article No.: 25
DOI: 10.1145/1380572.1380574

We show that the unification problem “is there a substitution instance of a given formula that is provable in a given logic?” is undecidable for basic modal logics K and K4 extended with the universal modality. It follows that...

Open answer set programming with guarded programs
Stijn Heymans, Davy Van Nieuwenborgh, Dirk Vermeir
Article No.: 26
DOI: 10.1145/1380572.1380575

Open answer set programming (OASP) is an extension of answer set programming where one may ground a program with an arbitrary superset of the program's constants. We define a fixed-point logic (FPL) extension of Clark's completion such that open...

Reasoning with recursive loops under the PLP framework
Yi-Dong Shen
Article No.: 27
DOI: 10.1145/1380572.1380576

Recursive loops in a logic program present a challenging problem to the PLP (Probabilistic Logic Programming) framework. On the one hand, they loop forever so that the PLP backward-chaining inferences would never stop. On the other hand, they may...

Flat and one-variable clauses: Complexity of verifying cryptographic protocols with single blind copying
Helmut Seidl, Kumar Neeraj Verma
Article No.: 28
DOI: 10.1145/1380572.1380577

Cryptographic protocols with single blind copying were defined and modeled by Comon and Cortier using the new class C of first-order clauses. They showed its satisfiability problem to be in 3-DEXPTIME. We improve this result by showing that...

Verifiable agent interaction in abductive logic programming: The SCIFF framework
Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, Paolo Torroni
Article No.: 29
DOI: 10.1145/1380572.1380578

SCIFF is a framework thought to specify and verify interaction in open agent societies. The SCIFF language is equipped with a semantics based on abductive logic programming; SCIFF's operational component is a new abductive logic programming proof...