ACM Transactions on

Computational Logic (TOCL)

Latest Articles

Proof Complexity Meets Algebra

We analyze how the standard reductions between constraint satisfaction problems affect their proof complexity. We show that, for the most studied propositional, algebraic, and semialgebraic proof systems, the classical constructions of pp-interpretability, homomorphic equivalence, and addition of constants to a core preserve the proof complexity of... (more)

Checking Admissibility Using Natural Dualities

This article presents a new method for obtaining small algebras to check the admissibility—equivalently, validity in free algebras—of quasi-identities in a finitely generated quasivariety. Unlike a previous algebraic approach of Metcalfe and Röthlisberger, which is feasible only when the relevant free algebra is not too... (more)

Generalized Eilenberg Theorem: Varieties of Languages in a Category

For finite automata as coalgebras in a category C, we study languages they accept and varieties of such languages. This generalizes Eilenberg’s concept of a variety of languages, which corresponds to choosing as C the category of Boolean algebras. Eilenberg established a bijective correspondence between pseudovarieties of monoids and... (more)

Interval vs. Point Temporal Logic Model Checking: An Expressiveness Comparison

In recent years, model checking with interval temporal logics is emerging as a viable alternative to model checking with standard point-based temporal logics, such as LTL, CTL, CTL*, and the like. The behavior of the system is modeled by means of (finite) Kripke structures, as usual. However, while temporal logics which are interpreted... (more)

A Higher-Order Calculus of Computational Fields

The complexity of large-scale distributed systems, particularly when deployed in physical space, calls for new mechanisms to address composability and reusability of collective adaptive behaviour. Computational fields have been proposed as an effective abstraction to fill the gap between the macro-level of such systems (specifying a... (more)


TOCL welcomes submissions related to all aspects of logic as it pertains to topics in computer science. The journal is published quarterly. The first issue appeared in July 2000, and the journal is indexed by ISI beginning with the 2006 volume. About

Forthcoming Articles

A Theoretical and Numerical Analysis of the Worst-Case Size of Reduced Ordered Binary Decision Diagrams

Binary Decision Diagrams (BDDs) and in particular ROBDDs (Reduced Ordered BDDs) are a common data structure for manipulating Boolean Expressions Integrated Circuit design, type inferencers, model checkers, and many other applications. Although a lightweight data structure to implement, the memory-wise behavior of ROBDDs may not be obvious to the program architect. We explore experimentally and theoretically the typical and worst-cases ROBDD sizes in terms of number of nodes and residual compression ratios as compared to un-reduced BDDs; in addition, we provide an algorithm to calculate the worst-case size. Finally, we present an algorithm for constructing a worst-case ROBDD of a given number of variables. Our approach may be useful to projects deciding whether the ROBDD is the appropriate data structure to use, and in building worst-case examples to test their code.

Modularisation of sequent calculi for normal and non-normal modalities

In this work we explore the connections between (linear) nested sequent calculi and ordinary sequent calculi for normal and non-normal modal logics. By proposing local versions to ordinary sequent rules we obtain linear nested sequent calculi for a number of logics, including to our knowledge the first nested sequent calculi for a large class of simply dependent multimodal logics, and for many standard non-normal modal logics. The resulting systems are modular and have separate left and right introduction rules for the modalities, which makes them amenable to specification as linear logic clauses. While this granulation of the sequent rules introduces more choices for proof search, we show how linear nested sequent calculi can be restricted to blocked derivations, which directly correspond to ordinary sequent derivations.

Tight Bounds on the Asymptotic Descriptive Complexity of Subgraph Isomorphism

Let v(F) denote the number of vertices in a fixed connected pattern graph F. We show an infinite family of patterns F such that the existence of a subgraph isomorphic to F is expressible by a first-order sentence of quantifier depth (2/3)v(F)+1, assuming that the host graph is sufficiently large and connected. On the other hand, this is impossible for any F with using less than (2/3)v(F)-2 first-order variables.

The Complexity of Minimal Inference Problem for Conservative Constraint Languages

We study the complexity of the inference problem for propositional circumscription (the minimal inference problem) over arbitrary finite domains. The problem is of fundamental importance in nonmonotonic logics and commonsense reasoning. The complexity of the problem for the two-element domain has been completely classified. In this paper, we classify the complexity of the problem over all conservative languages. We consider a version of the problem parameterized by a set of relations (a constraint language), from which we are allowed to build a knowledge base, and where a linear order used to compare models is a part of an input. We show that in this setting the problem is either  P2-complete, coNP-complete, or in P. The classification is based on a coNP-hardness proof for a new class of languages, an analysis of languages that do not express any member of the class and a new general polynomial-time algorithm solving the minimal inference problem for a large class of languages.

Fast Query Answering over Existential Rules

Enhancing Datalog with existential quantification gives rise to Datalog^E, a powerful knowledge representation language widely used in ontology-based query answering. In this setting, a conjunctive query is evaluated over a Datalog^E program consisting of extensional data paired with so-called existential rules. Due to their high expressiveness, such rules make the evaluation of queries undecidable, even when the latter are atomic. Decidable Datalog^E fragments have been proposed in the literature (e.g., weakly-acyclic and weakly-guarded); but they pay the price of a higher computational complexity, hindering the implementation of effective systems. Conversely, the results in this paper demonstrate that it is definitely possible to enable fast yet powerful query answering over existential rules, ensuring decidability without any complexity overhead. On the theoretical side, we define the class of parsimonious programs which guarantees decidability of atomic queries. We then strengthen this class to strongly parsimonious programs ensuring decidability also for conjunctive queries. Since parsimony is an undecidable property, we single out Shy, an easily recognizable class of strongly parsimonious programs that generalizes Datalog while preserving its complexity even under conjunctive query evaluation. Shy generalizes also the class of linear existential programs, while it is uncomparable to the other main classes ensuring decidability. On the practical side, we exploit our results to implement DLV^E, an effective system for query answering over parsimonious existential rules. To asses its efficiency, we carry out an experimental analysis, comparing DLV^E against state-of-the-art systems for ontology-based query answering. The results confirm the effectiveness of DLV^E, which outperforms all other systems.

All ACM Journals | See Full Journal Index

Search TOCL
enter search term and/or author name