LICS on Tuesday, July 13th

09:00‑10:00 FLoC Plenary Talk: Georg Gottlob
Chair: Martin Grohe
Location: George Square Lecture Theatre
09:00 Georg Gottlob (University of Oxford)
Datalog+-: A Family of Logical Query Languages for New Applications.

I will report on a recently introduced family of Datalog-based languages, called Datalog+-, which is a new framework for tractable ontology querying, and for a variety of other applications. Datalog+-extends plain Datalog by features such as existentially quantified rule heads, and, at the same time, restricts the rule bodies so to achieve decidability and tractability. I will review a number of theoretical results and show how Datalog+- relates to both Database Dependency Theory and the Guarded Fragment of first order logic. I will show that popular tractable description logics translate into Datalog+- and illustrate how this formalism can be used in the context of web data extraction, data exchange, and other applications.

10:30‑12:30 Logic and Automata
Chair: Georg Gottlob
Location: AT LT4
10:30 Mikołaj Bojańczyk and Sławomir Lasota
An extension of data automata that captures XPath

We define a new kind of automata recognizing properties of data words or data trees and prove that the automata capture all queries definable in Regular XPath. We also use the newly introduced automata as a common framework to classify existing automata on data words and trees, including data automata, register automata and alternating register automata. Finally, we demonstrate that the automata-theoretic approach may be applied to answer decidability and expressibility questions for XPath.

11:00 Thomas Place and Luc Segoufin
Deciding definability in FO2(<) on trees

We prove that it is decidable whether a regular unranked tree language is definable in FO2(<). By FO2(<) we refer to the two variable fragment of first order logic built from the descendant and following sibling predicates. In term of expressive power it corresponds to the restriction of the navigational core of XPath that contains modalities for going up to some ancestor, down to some descendant, left to some preceding sibling, and right to some following sibling.

We also investigate definability in some fragments of XPath.

11:30 Luis Barguñó, Carles Creus, Guillem Godoy, Florent Jacquemard and Camille Vacher
The Emptiness Problem for Tree Automata with Global Constraints

We define tree automata with global constraints (TAGC), generalizing the well-known class of tree automata with global equality and disequality constraints (TAGED). TAGC can test for equality and disequality between subterms whose positions are defined by the states reached during a computation. In particular, TAGC can check that all the subterms reaching a given state are distinct. This constraint is related to monadic key constraints for XML documents, meaning that every two distinct positions of a given type have different values.

We prove decidability of the emptiness problem for TAGC. This solves, in particular, the open question of decidability of emptiness for TAGED. We further extend our result by allowing global arithmetic constraints for counting the number of occurrences of some state or the number of different subterms reaching some state during a computation. We also allow local equality and disequality tests between sibling positions and the extension to unranked ordered trees. As a consequence of our results for TAGC, we prove the decidability of the existential fragment of the monadic second order logic on trees extended with predicates for equality and disequality between subtrees, and cardinality.

12:00 Nicole Schweikardt and Luc Segoufin
Addition-invariant FO and regularity

We consider formulas which, in addition to the symbols in the vocabulary, may use two designated symbols < and + that must be interpreted as a linear order and its associated addition. Such a formula is called addition-invariant if, for each fixed interpretation of the initial vocabulary, its result is independent of the particular interpretation of < and +.

This paper studies the expressive power of addition-invariant first-order logic, +-inv-FO, on the class of finite strings. Our first main result gives a characterization of the regular languages definable in +-inv-FO: we show that these are exactly the languages definable in FO with extra predicates, denoted by "lm" for short, for testing the length of the string modulo some fixed number. Our second main result shows that every language definable in +-inv-FO, that is bounded or commutative or deterministic context-free, is regular. As an immediate consequence of these two main results, we obtain that +-inv-FO is equivalent to FO(lm) on the class of finite colored sets.

Our proof methods involve Ehrenfeucht-Fraïssé games, tools from algebraic automata theory, and reasoning about semi-linear sets.

14:00‑15:00 FLoC Keynote Talk: J Strother Moore
Chair: Jean-Pierre Jouannaud
Location: George Square Lecture Theatre
14:00 J Strother Moore (University of Texas)
Theorem Proving for Verification: The Early Days.

Since Turing, computer scientists have understood that the question "does this program satisfy its specifications?" could be reduced to the question "are these formulas theorems?" But the theorem proving technology of the 50s and 60s was inadequate for the task. In 1971, here in Edinburgh, Boyer and I started building the first general-purpose theorem prover designed for a computational logic. This project continues today, with Matt Kaufmann as a partner; the current version of the theorem prover is ACL2 (A Computational Logic for Applicative Common Lisp).

In this talk I'll give a highly personal view of the four decade long "Boyer-Moore Project", including our mechanization of inductive proof, support for recursive definitions, rewriting with previously proved lemmas, integration of decision procedures, efficient representation of logical constants, fast execution, and other proof techniques. Along the way we'll see several interesting side roads: the founding of the Edinburgh school of logic programming, a structure-shared text editor that played a role in the creation of Word, and perhaps most surprisingly, the use of our "Lisp theorem prover" to formalize and prove theorems about commercial microprocessors and virtual machines via deep embeddings, including parts of processors by AMD, Centaur, IBM, Motorola, Rockwell-Collins, Sun, and others. The entire project helps shed light on the dichotomy between general-purpose theorem provers and special-purpose analysis tools.

15:30‑17:00 Logics
Chair: Amy Felty
Location: AT LT4
15:30 Alessio Guglielmi, Tom Gundersen and Lutz Strassburger
Breaking Paths in Atomic Flows for Classical Logic

This work belongs to a wider effort aimed at eliminating syntactic bureaucracy from proof systems. In this paper, we present a novel cut elimination procedure for classical propositional logic. It is based on the recently introduced `atomic flows': they are purely graphical devices that abstract away from much of the typical bureaucracy of proofs. We make crucial use of the `path breaker', an atomic flow construction that avoids some nasty termination problems, and that can be used in any proof system with sufficient symmetry. This paper contains an original 2-dimensional-diagram exposition of atomic flows, which helps us to connect atomic flows with other known formalisms.

16:00 Michele Basaldella and Kazushige Terui
Infinitary completeness in ludics

Traditional Goedel completeness holds between finite proofs and infinite models over formulas of finite depth (eg. classical first-order sentences). Our purpose is to generalize it to a completeness theorem between infinite proofs and infinite models over formulas of infinite depth (that include recursive types).

We work on a nonlinear extension of ludics, a monistic variant of game semantics which has the same expressive power as the propositional fragment of polarized linear logic. In order to extend the completeness theorem of the original ludics to the infinitary setting, we modify the notion of orthogonality by defining it via safety rather than termination of normalization. Then the new completeness ensures that the universe of behaviours (interpretations of formulas) is Cauchy-complete, so that every recursive equation has a unique solution.

Our work arises from studies on recursive types in denotational and operational semantics, but is conceptually much simpler, due to the purely logical setting of ludics, the completeness theorem for proofs, and uses of coinductive techniques.

16:30 Arnon Avron, Ofer Arieli and Anna Zamansky
On Strong Maximality of Paraconsistent Finite-Valued Logics

Maximality is a desirable property of paraconsistent logics, motivated by the aspiration to tolerate inconsistencies, but at the same time retain as much as possible from classical logic. In this paper we introduce a new, strong notion of maximal paraconsistency, which is based on possible extensions of the consequence relation of a logic. We investigate this notion in the framework of finite-valued paraconsistent logics, and show that for every n>2 there exists an extensive family of n-valued logics, each of which is maximally paraconsistent in our sense, is partial to classical logic, and is not equivalent to any k-valued logic with k<n. On the other hand, we specify a natural condition that guarantees that a paraconsistent logic is contained in a logic in the class of three-valued paraconsistent logics, and show that all reasonably expressive logics in this class are maximal.

17:15‑17:55 Short Papers Session
Chair: Stephane Lengrand
Location: AT LT4
17:15 Mohamed Nabih Menaa
On the Compositionality of Round Abstraction

We revisit a technique called round abstraction as a solution to the problem of building a synchronous system from an asynchronous specification. We define it within a trace-semantic setting akin to Abramsky's Interaction Categories, which is also a generalisation of pointer-free game semantic models. We note that, in general, round-abstracted behaviours fail to compose correctly. We then present a framework for round abstraction that is totally correct when applied to asynchronous behaviours.

17:25 Pierre-yves Strub and Qian Wang
Coq Modulo Theory - Short Paper

Coq Modulo Theory (CoqMT) is an extension of the Coq proof assistant incorporating, in its computational mechanism, validity entailment for user-defined first-order equational theories. Such a mechanism strictly enriches the system (more terms are typable), eases the use of dependent types and provides more automation during the development of proofs.

CoqMT improves over the Calculus of Congruent Inductive Constructions by getting rid of various restrictions and simplifying the type-checking algorithm and the integration of first-order decision procedures.

17:35 Stanislav Böhm, Stefan Göller and Petr Jancar
Bisimilarity of one-counter processes is PSPACE-complete

A one-counter automaton is a pushdown automaton over a singleton stack alphabet. We prove that the bisimilarity of processes generated by nondeterministic one-counter automata (with no epsilon-steps) is in PSPACE. This improves the previously known decidability result (Jancar 2000), and matches the known PSPACE lower bound (Srba 2009). We add the PTIME-completeness result for deciding regularity of one-counter processes (i.e., their finiteness upto bisimilarity).

17:45 Jian-Qi Li
A Computability Path Ordering for Polymorphic Terms

We develop a new version of the computability path ordering, which is well-founded on the set of polymorphic lambda terms. This is a new important step towards our challenge: to develop a well-founded order on the set of terms of the calculus of constructions, allowing to reduce strong normalization proofs of logical calculi to ordering comparisons of their computational rules.