Invited Speakers

M4M 2017 will feature invited talks by the following speakers.

  1. Joel Gregory Lucero-Bryan
    Khalifa University of Science, Technology and Research, Abu Dhabi, UAE

    • Title: MODAL LOGICS OF TYCHONOFF HED-SPACES

    • Abstract: Topological semantics interprets modal box as topological interior, and hence modal diamond as topological closure. Topological semantics is a natural generalization of Kripke semantics for the well-known modal system S4 since an S4-frame can be viewed as a (special) topological space. Therefore, every Kripke complete extension of S4 is also topo- logically complete. However, topological spaces arising from S4-frames lack good separation properties. Thus, it is desirable to know which modal logics arise from topological spaces satisfying good separation axioms, such as Tychonoff spaces. This turns out to be a rather nontrivial problem to solve.

      In this talk we concentrate on the well-known modal logic S4.3 which is obtained from S4 by postulating the axiom ▭(▭p → q)∨ ▭(▭q → p). The Bull-Fine theorem states that there are countably many extensions of S4.3, each of which is finitely axiomatizable and has the finite model property. The modal logic S4.3 is the logic of all hereditarily extremally disconnected (HED) spaces. We introduce the concept of a Zemanian extension of S4.3 by generalizing the Zeman modal logic. By utilizing the Bull-Fine theorem we prove that an extension of S4.3 is the logic of a Tychonoff HED-space iff it is Zemanian. This solves the aforementioned problem for extensions of S4.3.

  2. Lidia Tendera
    Institute of Mathematics and Informatics, Opole University, Poland

    • Title: Finite Model Reasoning in Expressive Fragments of First-Order Logic

    • Abstract: Over the past two decades several fragments of first-order logic have been identified and shown to have good computational and algorithmic properties, to a great extent as a result of appropriately describing the image of the standard translation of modal logic to first-order logic. This applies most notably to the guarded fragment, where quantifiers are appropriately relativized by atoms, and the fragment defined by restricting the number of variables to two

      The aim of this talk is to review recent work concerning these fragments, their extensions and related fragments obtained by other restrictions. When presenting the material special attention is given to decision procedures for the finite satisfiability problems, as many of the fragments discussed contain infinity axioms. We highlight most effective techniques used in this context, their advantages and limitations. We also mention a few open directions of study.

M4M 2017 will feature invited tutorials by the following speakers.

  1. Thomas Bolander
    Technical University of Denmark

    • Title: Epistemic Planning: The DEL approach

    • Abstract: Automated planning is a branch of artificial intelligence concerned with computing plans (sequences of actions) leading to some desired goal. A human or robot could e.g. have the goal of picking up a parcel at the postal office, and then the problem becomes to find a succesful sequence of actions achieving this. Epistemic planning is the enrichment of planning with epistemic notions, that is, knowledge and beliefs. The human or robot might have to reason about epistemic aspects such as: Do I know at which postal office the parcel is? If not, who would be relevant to ask? Maybe the parcel is a birthday present for my daughter, and I want to ensure that she doesn't get to know, and have to plan my actions accordingly (make sure she doesn't see me with the parcel). The epistemic notions are usually formalised using an epistemic logic. Epistemic planning can naturally be seen as the combination of automated planning with epistemic logic, relying on ideas, concepts and solutions from both areas

      In general, epistemic planning considers the following problem: Given my current state of knowledge, and a desirable state of knowledge, how do I get from one to the other? It is of central importance in settings where agents need to be able to reason about their own lack of knowledge, and e.g. make plans of how to achieve the required knowledge. It is also essential in multi-agent planning, where succesful coordination and collaboration can only be expected if agents are able to reason about the knowledge, uncertainty and capabilities of the other agents.

      In this tutorial on epistemic planning, the focus will primarily be on the DEL approach to epistemic planning: Using Dynamic Epistemic Logic (DEL) as the underlying formalism. The DEL approach will also be related to competing approaches and formalisms, both those that come from the planning community and those that come from the logic community. The tutorial will first briefly introduce classical (non-epistemic) planning, and then carefully explain how classical planning is generalised into epistemic planning. The tutorial will also include a brief crash course in the necessary parts of the underlying DEL formalism. Then the tutorial will give a structured overview of the major contributions to DEL-based epistemic planning from its conception in 2011 up to today. This includes the computational complexity of computing epistemic plans, different types and notions of epistemic plans, variants of the underlying framework, applications and implemented systems.

  2. Kamal Lodaya
    Institute of Mathematical Science
    Paritosh Pandya
    Tata Institute of Fundamental Research

    • Title: Deterministic temporal logics and interval constraints

    • Abstract: In temporal logics, a central question is about the choice of modalities and their relative expressive power, in comparison to the complexity of decision problems such as satisfiability. In this tutorial, we will illustrate the study of such questions over finite word models, first with logics for Unambiguous Starfree Regular Languages (UL), originally defined by Schutzenberger, and then for extensions with constraints, which appear in interval logics. We present Deterministic temporal logics, with diverse sets of modalities, which also characterize UL. The tools and techniques used go under the name of "Turtle Programs" or "Rankers". These are simple kinds of automata. We use properties such as Ranker Directionality and Ranker Convexity to show that all these logics have NP satisfiability. A recursive extension of some of these modalities gives us the full power of first-order logic over finite linear orders. In contrast, a monotone recursive extension is no more powerful than UL. We also discuss Interval Constraint modalities extending Deterministic temporal logics, with intermediate expressiveness. These allow counting or simple algebraic operations on paths. The complexity of these extended logics is PSpace, as of full temporal logic (and ExpSpace when using binary notation).