ACM Transactions on

Computational Logic (TOCL)

Latest Articles

Dynamic QBF Dependencies in Reduction and Expansion

We provide the first proof complexity results for QBF dependency calculi. By showing that the reflexive resolution path dependency scheme admits... (more)

Adding Successor: A Transfer Theorem for Separation and Covering

Given a class C of word languages, the C-separation problem asks for an algorithm that, given as input two regular languages, decides whether there exists a third language in C containing the first language, while being disjoint from the second. Separation is usually investigated as a means to obtain a deep understanding of the class C. In this... (more)

Idempotent Anti-unification

In this article, we address two problems related to idempotent anti-unification. First, we show that there exists an anti-unification problem with a single idempotent symbol that has an infinite minimal complete set of generalizations. It means that anti-unification with a single idempotent symbol has infinitary or nullary generalization type,... (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

Finite Open-World Query Answering With Number Restrictions

Open-world query answering is the problem of deciding, given a set of facts, conjunction of constraints, and query, whether the facts and constraints imply the query. This amounts to reasoning over all instances that include the facts and satisfy the constraints. We study \emph{finite open-world query answering} (FQA), which assumes that the underlying world is finite and thus only considers the finite completions of the instance. The major known decidable cases of FQA derive from the following: the guarded fragment of first-order logic, which can express referential constraints (data in one place points to data in another) but cannot express number restrictions such as functional dependencies; and the guarded fragment with number restrictions but on a signature of arity only two. In this paper, we give the first decidability results for FQA that combine both referential constraints and number restrictions for arbitrary signatures: we show that, for unary inclusion dependencies and functional dependencies, the finiteness assumption of FQA can be lifted up to taking the finite implication closure of the dependencies. Our result relies on new techniques to construct finite universal models of such constraints, for any bound on the maximal query size.

Duality between unprovability and provability in forward refutation-search for Intuitionistic Propositional Logic

The inverse method is a saturation based theorem proving technique; it relies on a forward proof-search strategy and can be applied to cut-free calculi enjoying the subformula property. Here we apply this method to derive the unprovability of a goal formula G in Intuitionistic Propositional Logic. To this aim we design a forward calculus FRJ(G) for Intuitionistic unprovability which is prone to constructively ascertain the unprovability of a formula G by providing a concise countermodel for it; in particular we prove that the generated countermodels have minimal height. Moreover, we clarify the role of the saturated database obtained as result of a failed proof-search in FRJ(G) by showing how to extract from such a database a derivation witnessing the Intuitionistic validity of the goal.

A First-Order Logic for Reasoning about Knowledge and Probability

We present a first-order probabilistic epistemic logic, which allows combining operators of knowledge and probability within a group of possibly infinitely many agents. The proposed framework is the first order extension of the logic of Fagin and Halpern from (J.ACM 41:340-367,1994). We define its syntax and semantics, and prove the strong completeness property of the corresponding axiomatic system.

MTL and TPTL for One-Counter Machines: Expressiveness, Model Checking, and Satisfiability

Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are quantitative extensions of Linear Temporal Logic, which are prominent and widely used in the verification of real-timed systems. We examine the capabilities of using MTL and TPTL to specify properties about one-counter machines. It is known that model checking one-counter machines using the specification language Freeze LTL, a strict fragment of TPTL, is undecidable. We prove that in our setting, MTL is strictly less expressive than TPTL, and incomparable in expressiveness to Freeze LTL, so that undecidability for MTL is not implied by the result for Freeze LTL. We show, however, that MTL-model checking of one-counter machines is undecidable. We further prove that both the finitary and the infinitary satisfiability problems for the unary fragments of TPTL and MTL are undecidable; for TPTL this even holds if only one register and only the finally modality is used. This is opposed to the known decidability result for satisfiability of Freeze LTL with at most one register.

Linking Focusing and Resolution with Selection

Focusing and selection are techniques that shrink the proof search space for respectively sequent calculi and resolution. To bring out a link between them, we generalize them both: we introduce a sequent calculus where each occurrence of an atom can have a positive or a negative polarity; and a resolution method where each literal, whatever its sign, can be selected in input clauses. We prove the equivalence between cut-free proofs in this sequent calculus and derivations of the empty clause in that resolution method. Such a generalization is not semi-complete in general, which allows us to consider complete instances that correspond to theories of any logical strength. We present three complete instances: first, our framework allows us to show that ordinary focusing corresponds to hyperresolution and semantic resolution; the second instance is deduction modulo theory and the related framework called superdeduction; and a new setting, not captured by any existing framework, extends deduction modulo theory with rewriting rules having several left-hand sides, which restricts even more the proof search space.

Towards a Uniform Theory of Effectful State Machines

Using recent developments on coalgebraic and monad-based semantics, we present a uniform study of various notions of machines, e.g. finite state machines, multi-stack machines, Turing machines, valence automata, and weighted automata. They are instances of Jacobs? notion of a T-automaton, where T is a monad. We show that the generic language semantics for T-automata correctly instantiates the usual language semantics for a number of known classes of machines/languages, including regular, context-free, recursively-enumerable and various subclasses of context free languages (e.g. deterministic and real-time ones). Moreover, our approach provides new generic techniques for studying the expressivity power of various machine-based models.

Model-Checking on Ordered Structures

We study the model-checking problem for first- and monadic second-order logic on finite relational structures. The problem of verifying whether a formula of these logics is true on a given structure is considered intractable in general, but it does become tractable on interesting classes of structures, such as on classes whose Gaifman graphs have bounded treewidth. In this paper we continue this line of research and study model-checking for first- and monadic second-order logic in the presence of an ordering on the input structure. We do so in two settings: the general ordered case, where the input structures are equipped with a fixed order or successor relation, and the order invariant case, where the formulas may resort to an ordering, but their truth must be independent of the particular choice of order. In the first setting we show very strong intractability results for most interesting classes of structures. In contrast, in the order invariant case we obtain tractability results for order-invariant monadic second-order formulas on the same classes of graphs as in the unordered case. For first-order logic, we obtain tractability of successor-invariant formulas on classes whose Gaifman graphs have bounded expansion. Furthermore, we show that model-checking for order-invariant first-order formulas is tractable on coloured posets of bounded width.

Extending Liquid Types to Arrays

A liquid type is an ordinary Hindley-Milner type annotated with a logical predicate that states the properties satisfied by the elements of that type. Liquid types are a powerful tool for program verification, since programmers can use them to specify pre- and postconditions of their programs, while the predicates of intermediate variables and auxiliary functions are inferred automatically. Type inference is feasible in this context, since the logical predicates within liquid types are constrained to a quantifier-free logic in order to maintain decidability. In this paper we extend liquid types by allowing them to contain quantified properties on arrays, so that they can be used to infer invariants on array-related programs (for example, implementations of sorting algorithms). Although quantified logic is, in general, undecidable, we restrict properties on arrays to a decidable subset introduced by Bradley et al. We describe in detail the extended type system, the verification condition generator, and the iterative weakening algorithm for inferring invariants. After proving the correctness and completeness of these two algorithms, we apply them to find invariants on a set of algorithms involving array manipulations.

Dichotomies in Ontology-Mediated Querying with the Guarded Fragment

We study ontology-mediated querying in the case where ontologies are formulated in the guarded fragment of first-order logic (GF) or extensions thereof with counting and where the actual queries are (unions of) conjunctive queries. Our aim is to classify the data complexity and Datalog rewritability of query evaluation depending on the ontology O, where query evaluation w.r.t. O is in PTime (resp. Datalog rewritable) if all queries can be evaluated in PTime w.r.t. O (resp. rewritten into Datalog under O), and coNP-hard if at least one query is coNP-hard w.r.t. O. We identify several fragments of GF that enjoy a dichotomy between Datalog-rewritability (which implies PTime) and coNP-hardness as well as several other fragments that enjoy a dichotomy between PTime and coNP-hardness, but for which PTime does not imply Datalog-rewritability. For the latter, we establish and exploit a connection to constraint satisfaction problems. We also identify fragments for which there is no dichotomy between PTime and coNP. To prove this, we establish a non-trivial variation of Ladner?s theorem on the existence of NP-intermediate problems. Finally, we study the decidability of whether a given ontology enjoys PTime query evaluation, presenting both positive and negative results, depending on the fragment.

The Power of the Weak

A landmark result in the study of logics for formal verification is Janin & Walukiewicz's theorem, stating that the modal ?-calculus (?ML) is equivalent modulo bisimilarity to standard monadic second-order logic (here abbreviated as smso), over the class of labelled transition systems (LTSs for short). Our work proves two results of the same kind, one for the alternation-free fragment of ?ML (?DML) and one for weak mso (wmso). Whereas it was known that ?DML and wmso are equivalent modulo bisimilarity on binary trees, our analysis shows that the picture radically changes once we reason over arbitrary LTSs. The first theorem that we prove is that, over LTSs, ?DML is equivalent modulo bisimilarity to noetherian mso (nmso), a newly introduced variant of smso where second-order quantification ranges over "well-founded" subsets only. Our second theorem starts from wmso, and proves it equivalent modulo bisimilarity to a fragment of ?DML defined by a notion of continuity. Analogously to Janin & Walukiewicz's result, our proofs are automata-theoretic in nature: as another contribution, we introduce classes of parity automata characterising the expressiveness of wmso and nmso (on tree models) and of ?CML and ?DML (for all transition systems).

Intuitionistic Linear Temporal Logics

We consider intuitionistic variants of linear temporal logic with `next', `until' and `release' based on {\em expanding posets:} partial orders equipped with an order-preserving transition function. This class of structures gives rise to a logic which we denote $ITL^e$, and by imposing additional constraints we obtain the logics $ITL^p$ of {\em persistent posets} and $ITL^{ht}$ of {\em here-and-there temporal logic,} both of which have been considered in the literature. We prove that $ITL^e$ has the effective finite model property and hence is decidable, while $ITL^p$ does not have the finite model property. We also introduce notions of bounded bisimulations for these logics and use them to show that the `until' and `release' operators are not definable in terms of each other, even over the class of persistent posets.

Why liveness for timed automata is hard, and what we can do about it

The reachability problem for timed automata asks if a given automaton has a run leading to an accepting state, and the liveness problem asks if the automaton has an infinite run which visits accepting states infinitely often. Both these problems are known to be PSPACE-complete. We show that if P ? PSPACE, the liveness problem is more difficult than the reachability problem; in other words we exhibit a family of automata for which solving the reachability problem with the standard algorithm is in P but solving the liveness problem is PSPACE-hard. This leads us to revisit the algorithmics for the liveness problem. We propose a notion of a witness for the fact that a timed automaton violates a liveness property. We give an algorithm for computing such a witness and compare it with existing solutions.

All ACM Journals | See Full Journal Index

Search TOCL
enter search term and/or author name