ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 14 Issue 1, February 2013

Linear-Logic Based Analysis of Constraint Handling Rules with Disjunction
Hariolf Betz, Thom Frühwirth
Article No.: 1
DOI: 10.1145/2422085.2422086

Constraint Handling Rules (CHR) is a declarative rule-based programming language that has cut out its niche over the course of the last 20 years. It generalizes concurrent constraint logic programming to multiple heads, thus closing the gap to...

Complexities of Horn Description Logics
Markus Krötzsch, Sebastian Rudolph, Pascal Hitzler
Article No.: 2
DOI: 10.1145/2422085.2422087

Description logics (DLs) have become a prominent paradigm for representing knowledge in a variety of application areas, partly due to their ability to achieve a favourable balance between expressivity of the logic and performance of reasoning....

Computing Loops with at Most One External Support Rule
Xiaoping Chen, Jianmin Ji, Fangzhen Lin
Article No.: 3
DOI: 10.1145/2422085.2422088

A consequence of a logic program under answer set semantics is one that is true for all answer sets. This article considers using loop formulas to compute some of these consequences in order to increase the efficiency of answer set solvers. Since...

YAPA: A Generic Tool for Computing Intruder Knowledge
Mathieu Baudet, Véronique Cortier, Stéphanie Delaune
Article No.: 4
DOI: 10.1145/2422085.2422089

Reasoning about the knowledge of an attacker is a necessary step in many formal analyses of security protocols. In the framework of the applied pi-calculus, as in similar languages based on equational logics, knowledge is typically expressed by...

Proof Nets for Herbrand’s Theorem
Richard McKinley
Article No.: 5
DOI: 10.1145/2422085.2422090

This article explores Herbrand’s theorem as the source of a natural notion of abstract proof object for classical logic, embodying the “essence” of a sequent calculus proof. We see how to view a calculus of abstract Herbrand...

Nondeterministic Phase Semantics and the Undecidability of Boolean BI
Dominique Larchey-Wendling, Didier Galmiche
Article No.: 6
DOI: 10.1145/2422085.2422091

We solve the open problem of the decidability of Boolean BI logic (BBI), which can be considered the core of separation and spatial logics. For this, we define a complete phase semantics suitable for BBI and characterize it as trivial phase...

Sound and Complete Axiomatizations of Coalgebraic Language Equivalence
Marcello M. Bonsangue, Stefan Milius, Alexandra Silva
Article No.: 7
DOI: 10.1145/2422085.2422092

Coalgebras provide a uniform framework for studying dynamical systems, including several types of automata. In this article, we make use of the coalgebraic view on systems to investigate, in a uniform way, under which conditions calculi that are...