WoLLIC 2012


If you have questions please contact the co-chairs of the organizing committee.

Download the Program

Program at a Glance



  • Tutorial 1: Hans van Ditmarsch (Sevilla)
    Title: Introduction to Dynamic Epistemic Logic
    Abstract: Dynamic epistemic logic is the multi-agent logic of change of knowledge. It can be used to specify multi-agent systems and their dynamic behaviour on a high level of systems architecture. The language contains operations K φ for 'knowing that φ', and also operators for knowledge change, such as [φ]ψ for 'after announcing φ, ψ is true'. Puzzling phenomena about this logic are the consequences of announcing 'p is true and you do not know that'. After that, you know p, which seems to be contradictory. The logic exists in many variations, including operators for more complex change of information such as private actions, operators for factual instead of informational change, and operators for quantification over change.
  • Tutorial 2: Eduardo Bonelli (Buenos Aires)
    Title: Curry-Howard for Justification Logic
    Abstract: Justification Logic (JL) is a refinement of modal logic that has recently been proposed for explaining well-known paradoxes arising in the formalization of Epistemic Logic. Assertions of knowledge and belief are accompanied by justifications: the formula [t]A states that t is ``reason'' for knowing/believing A. After an overview of JL we shall focus on devising computational interpretations for it via the Curry-de Bruijn-Howard isomorphism. Two avenues are explored: certifying mobile computation and history-aware computation.
  • Tutorial 3: Peter Selinger (Halifax)
    Title: Semantics of Quantum Computation
    Abstract:This lecture will be an introduction to quantum computing from a logical and symbolic point of view. I will introduce the basic rules of quantum computing, and illustrate them by designing a very simple typed quantum programming language. I will also discuss the denotational semantics of this language, and briefly discuss related structures in category theory.
  • Tutorial 4: Nicole Schweikardt (Frankfurt)
    Title: A tutorial on order-invariant logics
    Abstract: Order-invariant formulas are formulas for which the following is true: If a structure satisfies the formula with one particular linear order of the structure's universe, then it satisfies the formula with any linear order of the structure's universe. This tutorial will give an introduction to order-invariant logics.

Invited Talks

  • Invited Speaker 1: Andrea Asperti (Bologna)
    Title: Formalizing Turing Machines
    Abstract: We discuss the formalization, in the Matita Theorem Prover, of a few, basic results on Turing Machines, up to the existence of a (certified) Universal Machine. The work is meant to be a preliminary step towards the creation of a formal repository in Complexity Theory, and is a small piece in our Reverse Complexity program, aiming to a comfortable, machine independent axiomatization of the field.
  • Invited Speaker 2: George Metcalfe (Bern)
    Title: Admissible Rules: From Characterizations to Applications
    Abstract: The admissible rules of a logic (understood as a consequence relation) can be described, equivalently, as rules that can be added to the logic without producing any new theorems, and also as rules such that any substitution making the premises into theorems, also makes the conclusion into a theorem. However, this equivalence collapses once multiple-conclusion or other, more exotic, admissible rules are considered. The first aim of this talk will be to explain how such distinctions can be explained and characterized. The second will be to show how the admissibility of rules, often established using syntactic eliminations, can be useful in characterizing properties of classes of algebras.
  • Invited Speaker 3: Hans van Ditmarsch (Sevilla)
    Title: Quantifying over information change
    Abstract: I will present different modal logics with propositional quantification. These logics are often taken to be epistemic logics, such that the quantification is over information change. The presentation includes the following alternatives - where 'φ' is any epistemic formula, such as 'Ann knows the deal of cards', and similarly 'an announcement' may be of any epistemic formula, such as (Bob announces that:) 'Bob has the white card'.
    1 <>φ for 'there is an announcement after which φ'
    2 φ for 'there is an announcement by coalition G after which φ'
    3 <[G]>φ for 'there is an announcement by coalition G after which, no matter what the agents not in G do, φ'
    4 <>φ for 'there is an action model after which φ'
    5 <>φ for 'there is a refinement after which φ' (refinement is the dual of simulation, the two directions of bisimulation)
    The logics have widely diverging properties, e.g., variation 1 is undecidable but variation 5 is decidable. In contrast to well-known bisimulation quantified logics, variation 5 can be called refinement quantified logic. Given the temporal aspect of all these quantifiers ('there is a future moment such that'), such logics may also serve as dynamic epistemic specifications such that their implementation is a form of synthesis. The logics with a coalitional aspect obviously relate to other coalitional logics, e.g., Pauly's coalitional logic can be embedded in 3.
  • Invited Speaker 4: Nicole Schweikardt (Frankfurt)
    Title: On the expressive power of logics with invariant uses of arithmetic predicates
    Abstract: In this talk I consider first-order formulas (FO, for short) where, apart from the symbols in the given vocabulary, also predicates for linear order and arithmetic may be used. For example, order-invariant formulas are formulas for which the following is true: If a structure satisfies the formula with one particular linear order of the structure's universe, then it satisfies the formula with any linear order of the structure's universe. Arithmetic-invariant formulas are defined analogously, where apart from the linear order other arithmetic predicates may be used in an invariant way. When restricting attention to finite structures, it is known that order-invariant FO is strictly more expressive than plain FO, and arithmetic-invariant FO can express exactly the properties that belong to the circuit complexity class AC0. On the other hand, by Trakthenbrot's theorem we know that order-invariance (on the class of finite structures) is undecidable. The aim of this talk is to give an overview of the state-of-the art concerning the expressive power of order-invariant and arithmetic-invariant logics.
  • Invited Speaker 5: Andre Nies (Auckland)
    Title: Interactions of computability and randomness
    Abstract: Randomness and complexity are closely connected. We provide mathematical counterparts of the two concepts for infinite sequences of bits. Then we discuss mathematical theorems showing the close relationship between the two concepts. For a mathematician, randomness of an infinite sequence of bits (equivalently, a real) is usually understood probability-theoretically. Theorems about random objects hold outside some unspecified null class; for instance, a function of bounded variation is differentiable at every ''random'' real. One cannot say that an individual real is random. In algorithmic randomness one introduces a notion of effective null class. A sequence is random in that sense if it avoids each effective null class. For instance, Chaitin's halting probability is random in the sense of Martin-Loef. A real is Martin-Loef random if and only if every computable function of bounded variation is differentiable at the real (Demuth 1975; work of Brattka, Miller and Nies 2011). Effective randomness notions interact in fascinating ways with the computational complexity of sequences of bits. For instance, being far from Martin-Loef random is equivalent to being close to computable in a specific sense (Nies, Advances in Math, 2005). We also consider the case that the tests are resource bounded. Polynomial time randomness, for instance, can be used to produce computable reals that are Borel normal with respect to every base.
  • Invited Speaker 6: Laura Kallmeyer (Düsseldorf)
    Title: Syntax-Driven Semantic Frame Composition in Lexicalized Tree Adjoining Grammars
    Abstract: In this talk, we present analyses of directed motion expressions and of the dative alternation in English in the framework of Lexicalized Tree Adjoining Grammars (LTAG) enriched with a (de)compositional frame semantics. This approach to the syntax-semantics interface allows us to combine a detailed decomposition and composition of syntactic building blocks with a parallel decomposition and composition of meaning components. In LTAG, lexical anchors can be distinguished from unanchored elementary trees which allows for the description of the meaning contributions of constructions. Furthermore, due to the metagrammatical factorization of the descriptions of unanchored elementary trees, the meaning contributions of single argument realizations and of their combinations can be described in a systematic way. We give a brief introduction to the LTAG formalism and show how the specification of elementary trees by means of metagrammatical constraints allows a strong factorization of the syntactic and semantic information provided by a given construction and, thereby, a detailed model of the interaction of the lexical semantics of the verb and the semantics of the constructional realization. We then use the English dative alternation ('send somebody something' vs 'send something to somebody') and directed motion expressions ('walked into the house', 'throw over the fence into the yard') as examples to illustrate how constructions and semantic frames can be decomposed and composed within the metagrammar and how syntactic unification in the metagrammar and in LTAG can drive the semantic unification of frames.
  • Invited Speaker 7: Peter Selinger (Halifax)
    Title:Logical methods in quantum information theory.
    Abstract: I will talk about some recent applications of logical methods to quantum information theory. In computing, a higher-order function is a function for which the input or output is another function. I will argue that many of the interesting phenomena of quantum information theory involve higher-order functions, although that is not how they are usually presented. I'll talk about the quantum lambda calculus as a possible framework to describe such phenomena.
  • Invited Speaker 8: Anca Muscholl (Bordeaux)
    Title: On distributed control and monitoring
    Abstract: In this survey we discuss verification issues in the setting of distributed finite-state systems. Verifying the correctness of such systems is known to be a very challenging task, for which current techniques are much less advanced than for sequential systems. First we will consider the control problem for finite-state processes synchronizing via shared variables, a particular instance of distributed synthesis. Its decidability status is one the main open problems in this area. Then we consider the monitoring problem, where we are interested in properties that can be monitored locally on such systems. We propose a distributed framework for monitoring issued from topological considerations.

Paper Sessions

Session 1

  • A. Baltag, B. Renne and S. Smets. The Logic of Justified Belief Change, Soft Evidence and Defeasible Knowledge
  • L. Menasché Schechter. A Logic of Plausible Justifications
  • M. Ribeiro and M. Coniglio. Contracting Logics

Session 2

  • S. Abriola, S. Figueira and G. Senno. Linearizing Bad Sequences: Upper Bounds for the Product and Majoring Well Quasi-orders
  • A. Farjudian. Polynomial-Time Solution of Initial Value Problems Using Polynomial Enclosures
  • B. Rossman. A Tight Upper Bound on the Number of Variables for Average-case k-Clique on Ordered Graphs

Session 3

  • W. Fouche. Algorithmic Randomness and Ramsey Properties of Countable Homogeneous Structures
  • A. Sankaran, B. Adsul, V. Madan, P. Kamath and S. Chakraborty. Preservation under Substructures Modulo Bounded Cores

Session 4

  • C. Areces, R. Fervari and G. Hoffmann. Moving Arrows and Four Model Checking Results
  • M. Volpe, J. Marcos and C. Caleiro. Classic-like Cut-based Tableau Systems for Finite-valued Logics
  • N. Bezhanishvili, C. Kupke and P. Panangaden. Minimization via Duality

Session 5

  • S. Link. Propositional Reasoning about Probabilistic Saturated Conditional Independence
  • C. Callejas, J. Marcos and B. Callejas Bedregal. On Some Subclasses of the Fodor-Roubens Fuzzy Bi-implications
  • P. Baldi, A. Ciabattoni and L. Spendier. Standard Completeness for Extensions of MTL: an Automated Approach

Session 6

  • B. Ahrens. Initiality for Typed Syntax and Semantics
  • A. Díaz-Caro and B. Petit. Linearity in the Non-deterministic Call-by-Value Setting