Special Issue for the Conference on Computer Science Logic (CSL) 2012


Editor: Arnaud Durand

The annual conference of the European Association for Computer Science Logic (EACSL), CSL 2012, was held in Fontainebleau, France, from 3 to 6 September 2012. CSL started as a series of international workshops on Computer Science Logic, and became at its sixth meeting the Annual Conference of the EACSL. This conference was the 26th workshop and 21th EACSL conference; it was organized by the Department of Computer Science of the Institut Universitaire de Technologie, IUT de Sénart Fontainebleau, of the university Paris Est Créteil (UPEC).

For the conference, a total of 35 papers were selected for presentation together with 3 invited talks. Proceedings were published as volume 16 of the Dagstuhl LIPICS series. For this special issues, several papers were chosen by the guest editors and their authors were invited to submit an extended version of their work. Each submitted article has then been peer-reviewed by at least two experts of the field. This process results in a total of 7 papers that represents the wideness and the richness of the usual topics of CSL from automata theory, proof theory, semantics of programming language to decidability results, definability issues and finite models.

We are sincerely grateful to all members of the Programme Committee, the reviewers, and to all authors who have submitted their work to CSL.

Patrick Cégielski, Arnaud Durand
CSL'2012 Guest Editors

1. Definability of linear equation systems over groups and rings

, ; , ; , ; , ; ,.
Motivated by the quest for a logic for PTIME and recent insights that the descriptive complexity of problems from linear algebra is a crucial aspect of this problem, we study the solvability of linear equation systems over finite groups and rings from the viewpoint of logical (inter-)definability. All problems that we consider are decidable in polynomial time, but not expressible in fixed-point logic with counting. They also provide natural candidates for a separation of polynomial time from rank logics, which extend fixed-point logics by operators for determining the rank of definable matrices and which are sufficient for solvability problems over fields. Based on the structure theory of finite rings, we establish logical reductions among various solvability problems. Our results indicate that all solvability problems for linear equation systems that separate fixed-point logic with counting from PTIME can be reduced to solvability over commutative rings. Moreover, we prove closure properties for classes of queries that reduce to solvability over rings, which provides normal forms for logics extended with solvability operators. We conclude by studying the extent to which fixed-point logic with counting can express problems in linear algebra over finite commutative rings, generalising known results on the logical definability of linear-algebraic problems over finite fields.

2. Ordered Models of the Lambda Calculus

, ; ,.
Answering a question by Honsell and Plotkin, we show that there are two equations between lambda terms, the so-called subtractive equations, consistent with lambda calculus but not simultaneously satisfied in any partially ordered model with bottom element. We also relate the subtractive equations to the open problem of the order-incompleteness of lambda calculus, by studying the connection between the notion of absolute unorderability in a specific point and a weaker notion of subtractivity (namely n-subtractivity) for partially ordered algebras. Finally we study the relation between n-subtractivity and relativized separation conditions in topological algebras, obtaining an incompleteness theorem for a general topological semantics of lambda calculus.

3. Herbrand-Confluence

, ; ,.
We consider cut-elimination in the sequent calculus for classical first-order logic. It is well known that this system, in its most general form, is neither confluent nor strongly normalizing. In this work we take a coarser (and mathematically more realistic) look at cut-free proofs. We analyze which witnesses they choose for which quantifiers, or in other words: we only consider the Herbrand-disjunction of a cut-free proof. Our main theorem is a confluence result for a natural class of proofs: all (possibly infinitely many) normal forms of the non-erasing reduction lead to the same Herbrand-disjunction.

4. Undecidable First-Order Theories of Affine Geometries

, ; , ; ,.
Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation \beta, and a quaternary equidistance relation \equiv. Tarski established, inter alia, that the first-order (FO) theory of (R^2,\beta,\equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2,\beta) with unary predicates is decidable. We refute this conjecture by showing that for all n>1, the FO-theory of the class of expansions of (R^2,\beta) with just one unary predicate is not even arithmetical. We also define a natural and comprehensive class C of geometric structures (T,\beta), and show that for each structure (T,\beta) in C, the FO-theory of the class of expansions of (T,\beta) with a single unary predicate is undecidable. We then consider classes of expansions of structures (T,\beta) with a restricted unary predicate, for example a finite predicate, and establish a variety of related undecidability results. In addition to decidability questions, we briefly study the expressivities of universal MSO and weak universal MSO over expansions of (R^n,\beta). While the logics are incomparable in general, over expansions of (R^n,\beta), formulae of weak universal MSO translate into equivalent formulae of universal MSO.

5. Knowledge Spaces and the Completeness of Learning Strategies

, ; ,.
We propose a theory of learning aimed to formalize some ideas underlying Coquand's game semantics and Krivine's realizability of classical logic. We introduce a notion of knowledge state together with a new topology, capturing finite positive and negative information that guides a learning strategy. We use a leading example to illustrate how non-constructive proofs lead to continuous and effective learning strategies over knowledge spaces, and prove that our learning semantics is sound and complete w.r.t. classical truth, as it is the case for Coquand's and Krivine's approaches.

6. A Proof of Kamp's theorem

We provide a simple proof of Kamp's theorem.

7. Connection Matrices and the Definability of Graph Parameters

, ; ,.
In this paper we extend and prove in detail the Finite Rank Theorem for connection matrices of graph parameters definable in Monadic Second Order Logic with counting (CMSOL) from B. Godlin, T. Kotek and J.A. Makowsky (2008) and J.A. Makowsky (2009). We demonstrate its vast applicability in simplifying known and new non-definability results of graph properties and finding new non-definability results for graph parameters. We also prove a Feferman-Vaught Theorem for the logic CFOL, First Order Logic with the modular counting quantifiers.