About the Workshop
Kanazawa Workshop for Epistemic Logic and its Dynamic Extensions will be held at the Shiinoki Cultural Complex, and is organized by Satoshi Tojo and Katsuhiko Sano of Japan Advanced Institute of Science and Technology (JAIST) from 21st to 22nd February, 2014. The aim of the Workshop is to discuss about epistemic logic and dynamic epistemic logic and their application from theoretical and practical viewpoints.
Before the workshop, Computability Theory and Foundations of Mathematics 2014 is held at Tokyo Institute of Technology, Tokyo, Japan, February 17 - 20, 2014.
- Thomas Ågotnes (University of Bergen)
- Mamoru Kaneko (Waseda University)
- Hidenori Kurokawa (Kobe University)
- Minghui Ma (Southwest University)
- Jeremy Seligman (The University of Auckland)
- François Schwarzentruber (ENS Rennes)
- Sonja Smets (ILLC, Universiteit van Amsterdam)
- Nobu-Yuki Suzuki (Shizuoka University)
- Fernando R. Velázquez Quesada (Universidad de Sevilla)
- Tomoyuki Yamada (Hokkaido University)
21st, February 2014
22nd, February 2014
Tableaux and Hypersequents for Logic of Proofs and Provability
In this talk, we discuss proof systems for logics combining Artemov's logic of proofs (LP) and the logic of provability (GL) (and strong provability (Grz)). The logic of proofs has been introduced to explore a combinatorial structure of proofs and also taken to be an ``explicit'' version of epistemic logic. GL (Grz) has been studied as a logic of formal provability (provability and truth) in arithmetic. These combined logics themselves have already existed in the literature for a while. The logic combining LP and GL is called GLA, and the logic combining LP and Grz is called GrzA. Hilbert-style axiomatizations of the logics have already been given; however, neither tableau systems nor Gentzen- style proof systems for the logics with nice proof-theoretic properties have been proposed so far. In the talk, we first give some motivating discussions for the logic of proofs. Then, we introduce both Fitting-style prefixed tableau systems and hypersequent calculi for GLA and GrzA. As technical results, we present the following. The first one is the admissibility of cut for the prefixed tableau systems via semantic completeness for the cut-free prefixed tableau systems for GLA and GrzA. The second one is the admissibility of cut for the hypersequent calculi for GLA and GrzA. We show this by constructing a translation from the prefixed tableau systems to the hypersequent calculi.
The logic of justified belief change, soft evidence and defeasible knowledge
I will present a logic for reasoning about evidence-based knowledge and beliefs and the evidential dynamics of non-logically-omniscient agents. I will adapt the key tools and techniques from Dynamic Epistemic Logic, Justification Logic, and Belief Revision in order to provide a lightweight, yet fine-grained approach that characterizes well-known epistemic and doxastic attitudes in the terms of the evidential reasoning that justifies these attitudes. As a result, I will argue that this approach can serve as a lynchpin in the formal analysis of complex dynamic epistemological reasoning scenarios, such as e.g. in various Gettier-type cases. This presentation is based on joint work with A. Baltag and B. Renne.
Axiomatizing Epistemic Logic of Friendship via Tree-sequent Calculus
Epistemic Logic of Friendship (EFL) is a version of two-dimensional modal logic proposed by Seligman, Girard and Liu (2013). Compared to the ordinary epistemic logic, one of the main features of their logic is to encode the information of agents into the object language by a technique of hybrid logic. Then, a propositional variable p can be read as an indexical proposition such as `I am p' and we may formalize the sentences like `I know that all of my friend is p' or `All of my friends know that he/she is p'. Moreover, they provide a dynamic mechanism for capturing public announcements, announcements to all the friends, and private announcements and established a relative completeness result. This talk focuses on the problem of axiomatizaing EFL, i.e., the static part of their framework. First, we provided a labelled sequent calculus LEFL for EFL and establish the completeness result of LEFL. Second, we translate each sequent of LEFL into an ordinary formula and specify a Hilbert-style axiomatization HEFL of EFL and establish a semantic completeness result for HEFL.
Infinite Regress Logic and Prediction/Decision Making in Games (with Tai-Wei Hu, Northwestern University)
In order to study infinite regresses arising from prediction/decision making in an 2-person game, we present a logic called the infinite regress logic IR². It extends finitary epistemic logic KD² for two players, by incorporating the two operators expressing infinite regresses. Here, an infinite regress arises from the interactive thinking of a player about the other's subjective thinking and vice versa. If we add the Truth Axiom for the belief operators to the KD², the infinite regresses collapse into the common knowledge. Hover, we keep the subjective nature of the concept, avoiding the Truth Axiom, Positive Introspection Axiom (4) as well as the Negative Introspection Axiom (5). We prove the completeness theorem with respect to Kripke semantics and a certain restricted class of Kripke models. These lead to various meta-theorems useful for considerations of prediction decision making in games. Indeed, we will show that the players may keep different understandings about the game situation even after the actual play of the game.
Decision and Prediction Criteria for Games and Intuitionistic Epistemic Logic of Shallow Depths
Epistemic logics of shallow depths are developed in various papers by Kaneko-Suzuki to aim to study game theoretical decision making, where by ``shallow depths'' we mean players' bounded interpersonal inferences. The key idea for designing our formal system is separation of epistemic and non-epistemic inferences by means of thought-sequents. Based on this formalism, we give consideration to decision and prediction criteria in game situations.
We also discuss feasibility of player's decision in a certain game from the viewpoint of constructive reasoning. In our previous approach, classical logic is adopted as the base logic, which implies that the players' logical abilities are also described by classical logic. Classical logic has some non-constructive feature, but decision making typically requires constructive reasoning. To capture the constructive nature, we adopt intuitionistic logic as the base logic rather than classical logic. The resulting epistemic logical system is based on first-order intuisionistic logic, and is complete with respect to Kripke-type semantics. Some meta-theorems are proved by making use of this semantics, and assure the equivalence between existence of decisions and feasibility of those decisions in our framework.
Secret tweets and network discovery
You are a secret agent with a secret $S$ that you would like to transmit to a fellow agent $a$ unobtrusively using a very public network like Twitter. Any information you tweet will be received by your followers on the network. You correctly assume that they will send the message on to their followers (retweet it) if and only if it does not conflict with any information they already possess. With luck, your message will be tweeted through the network until it eventually reachers $a$. Under what conditions is it possible for you to convey $S$ to $a$ in this way, without other agents in the network learning this information? Clearly, you cannot tweet $S$ itself, but if, for example, $a$ is the only agent to knows that $K$ then the message `if $K$ then $S$’ may work, if there is a suitable path from you to $a$. To know whether you can succeed or not and what to tweet, you need to know something about the network and the information already possessed by the other agents. But you can learn something about this with a test tweet. If, for example, you know that you have two followers $b$ and $c$ and only $b$ believes $P$ and then you tweet the message $\neg P$ then if, after a certain length of time, someone tweets $P$ to you, you know that there is a loop back to you via $c$. This talk will report on recent joint work on these and similar questions with Mostafa Raziebrahimsaraei.
The workshop takes place at Shiinoki Cultural Complex, which is located in the famous sightseeing spot of Kanazawa, including Kenroku-en (Six Attributes Garden), Kanazawa Castle, 21st Century Museum of Contemporary Art, etc... See Kanazawa Tourist Information Guide for more places (in particular, home → tour guide → 01).
- Shiinoki Cultural Complex
- 2-1-1 Hirosaka, Kanazawa, Ishikawa, Japan
- tel: +81-76-261-1111
For a larger map, check the map ``Kanazawa Workshop for Epistemic Logic and its Dynamic Extensions''.
You can also find information for sightseeing at Kanazawa at Lonely Planet
Access to Kanazawa
from Tokyo Narita Airport to Kanazawa Station:
Please take a limousine bus to Haneda Airport (HND), fly to Komatsu Airport (KMQ), and then take an airport bus (time table) to Kanazawa. Note that there are also direct flights between Narita and Komatsu (but not many).
from Kansai International Airport to Kanazawa Station:
Please take a suitable train (type "Kansai Airport" in "From" and "Kanazawa" in "To"). Since trains are going frequently, you can simply take the next one. From Kansai airport (Osaka) take the trains called "Haruka" to Shin-Osaka and change to express trains of the Hokuriku Line, which run once every hour. It takes about 4 hours to Kanazawa.
from Kanazawa Station to Venue and Hotels around Venue:The easiest way is to go by taxi (approx 1,000 yen) from the station.
AccommodationFor convenience we recommend to stay at a hotel in the center of the city i.e., Katamachi or Korinbou, rather than ones around Kanazawa Station. Here we list a few hotels.
- APA hotels (search at www.expedia.com
with e.g. keywords ``Kanazawa Japan'')
- APA Hotel Kanazawa-Katamachi (from $42 per night)
- APA Hotel Kanazawa-Chuou (from $49 per night)
- APA Villa Hotel Kanazawa-Katamachi (from $62 per night)
- Toyoko Inn Kanazawa Kenroku (from 4480JPY per night)
- Hotel Econo