ACM Transactions on

Computational Logic (TOCL)

Latest Articles

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.... (more)

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... (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

Pure Sequent Calculi: Analyticity and Decision Procedure

Analyticity, a.k.a. the subformula property, typically guarantees decidability of derivability in propositional sequent calculi. To utilize this fact, two substantial gaps have to be filled: $(i)$ what makes a sequent calculus analytic? and $(ii)$ how to obtain an efficient decision procedure for derivability in an analytic calculus? In the first part of this paper we address these gaps for \emph{pure calculi}---a general family of fully structural propositional sequent calculi whose rules allow arbitrary context formulas. We provide a sufficient syntactic criterion for analyticity in these calculi, as well as a fruitful method to construct new analytic calculi from given ones. We further introduce a scalable decision procedure for derivability in analytic pure calculi, by showing that it can be (uniformly) reduced to classical satisfiability. In the second part of the paper, we study the extension of pure sequent calculi with rules for modal operators. We show that such extensions preserve the analyticity of the calculus, and identify certain restricted operators (which we call `Next' operators) that are also amenable for a general reduction of derivability to classical satisfiability. Our proofs are all semantic, utilizing several strong general soundness and completeness theorems with respect to non-deterministic semantic frameworks: bivaluations (for pure calculi) and Kripke models (for their extension with modal operators).

Synchronizing Data Words for Register Automata

Register automata (RAs) are finite automata extended with a finite set of registers to store and compare data from an infinite domain. We study the concept of synchronizing data words in RAs: Does there exist a data word that sends all states of the RA to a single state? For deterministic RAs with k registers (k-DRAs), we prove that inputting data words with 2k+1 distinct data, from the infinite data domain, is sufficient to synchronize. We show that the synchronizing problem for DRAs is in general PSPACE-complete, and is NLOGSPACE-complete for 1-DRAs. For nondeterministic RAs (NRAs), we show that Ackermann(n) distinct data (where n is the size of the RA) might be necessary to synchronize. The synchronizing problem for NRAs is in general undecidable, however, we establish Ackermann-completeness of the problem for 1-NRAs. Our most substantial achievement is proving NEXPTIME-completeness of the length-bounded synchronizing problem for NRAs (length encoded in binary). A variant of this last construction allows to prove that the bounded universality problem for NRAs is coNEXPTIME-complete.

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.

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