Workshop on Logic, Philosophy, and Computation

講者簡介

Keynote Speaker

Melvin Fitting (Departments of Computer Science, Philosophy, and Mathematics, CUNY Graduate Center, USA; 2012 Herbrand Award winner)

Title: Justification Logic—Explicit Epistemic Logic

Abstract: Justification logics are epistemic logics that allow knowledge and belief modalities to be ‘unfolded’ into justification terms: instead of □X one writes t:X, and reads it as “X is justified by reason t”. One may think of traditional modal operators as implicit modalities, and justification terms as their explicit elaborations which supplement modal logics with finer-grained epistemic machinery. The family of justification terms has structure and operations. Choice of operations gives rise to different justification logics. For all common epistemic logics their modalities can be completely unfolded into explicit justification form. In this respect Justification Logic reveals and uses the explicit, but hidden, content of traditional Epistemic Modal Logic.

Justification logic originated as part of a successful project to provide a constructive semantics for intuitionistic logic—justification terms abstracted away all but the most basic features of mathematical proofs. Proofs are justifications in perhaps their purest form. Subsequently justification logics were introduced into formal epistemology. The subject as a whole is still under active development.

Each justification logic is associated with a traditional modal logic, and that association is via a notion called realization. There are algorithms that convert modal arguments into arguments with justifications made explicit. In a way, modal arguments always had an explicit component, but it needs these algorithms to make it visible. Such algorithms are current topics of investigation by several research groups, in the U. S., Russia, and Switzerland. I will sketch the ideas and discuss the consequences.

Guest Speaker

Sven Schewe (Department of Computer Science, University of Liverpool, UK)

Title: Beautiful Games You Cannot Stop Playing

Abstract: Parity games are simple two player games played on a finite arena that have all that it takes to attract the attention of researchers: it is a simple problem which is hard to analyse -- a pocket version of P vs. NP. Parity games are known to be in UP, CoUP, and some weirder classes besides, but whether or not they are in P has proven to be a rather elusive question. What is more, when you work with them, you will have the constant feeling that there is a polynomial solution just around the corner, although, it dissolves into nothingness when you look more closely. This talk is about the beauty of these games, the relevant algorithmic approaches and their complexity and development over time. But beware: they are addictive, don't get hooked!

Invited Speakers

1. I-Jen Chiang (蔣以仁; 臺北醫學大學醫學資訊研究所副教授)

Title:

Abstract:

2. Hao-Cheng Fu (傅皓政; 文化大學哲學系助理教授)

Title: Belief Revision and Information Economy Principle

Abstract: In ordinary life people would adjust one's own belief state in respect to new information and the widely accepted principle is that the loss of information value should be minimal, i.e. information economy principle (IEP). Some philosophers such as Quine and AGM (Alchourron et al.) advocated the principle and Gardenfors proposed the idea epistemic entrenchment to estimate how to minimize the loss of information value when the new belief state generated. Nevertheless Rott casted doubt to IEP due to the ordering of epistemic entrenchment failed to hold in some situations thus sometimes we keep the less entrenched beliefs rather than more entrenched ones. In this paper, I present a game-theoretic framework to reconstruct the notion of epistemic entrenchment and claim that IEP is available to estimate generated belief states.

Download Files

3. Yih-Kuen Tsay (蔡益坤; 台大資管系教授)

Title: Tool Support for Games, Omega-Automata, and Temporal Logics

Abstract: Omega-automata and temporal logics have proven useful in formal verification, while infinite games found instrumental as a foundation for synthesis. A basic understanding of these formalisms and their relationship have thus become essential for most who want to work in verification or synthesis, but the learning curve can be steep for beginners. Furthermore, operations and tests on these formalisms often involve sophisticated algorithms, which may be hard to get right even for experts. Adequate tool support can help alleviate these difficulties.

In this talk, I will describe two tools: GOAL and Buechi Store, and show a number of typical usages. GOAL allows visual definition and manipulation of the various types of omega-automata and translation of temporal formulae to such automata. It facilitates research on relevant algorithms because of its capability of testing language equivalence. GOAL can also solve infinite games, in particular parity games. Buechi Store is a Web-based repository of temporal formulae of common patterns and their equivalent omega-automata. Such a repository provides examples for learning and also small automata for efficient model checking.

4. Farn Wang (王凡; 台大電機系教授)

Title: Game Interaction Logic

Abstract: We propose an extension to ATL (alternating-time logic), called BSIL (basic strategy-interaction logic), for the specification of interaction among the strategies of agents in a multi-agent system. BSIL allows for the specifications of one system strategy that can cooperate with several strategies of the environment for different requirements. We argue that such properties are important in practice and rigorously show that such properties are not expressible in ATL*, GL (game logic), and AMC (alternating mu-calculus). Specifically, we show that BSIL is more expressive than ATL but incomparable with ATL*, GL, and AMC in expressiveness. We show that a memoryful strategy is necessary for fulfilling a specification in BSIL. We also show that the model-checking problem of BSIL is PSPACE-complete and is of lower complexity than those of ATL*, GL, AMC, and the general strategy logics. This may imply that BSIL can be useful in closing the gap between real-world projects and the game-theoretical results. We then show the plausibility and feasibility of our techniques by reporting our implementation and experiment with our PSPACE model-checking algorithm for BSIL. Finally, we discuss an extension of BSIL.

5. Ren-June Wang (王仁俊; 國立中正大學哲學系助理教授)

Title: Temporalizing Modal Epistemic Logic

Abstract: Timed Modal Epistemic Logic, tMEL, is a newly introduced logical framework for reasoning about the modeled agent's knowledge. The framework is adapted, both syntactically and semantically, from the traditional Modal Epistemic Logic, MEL, such that the time when the known proposition is known based on the agent's deductive reasoning process can be explicitly stated. In this paper we will give a semantic proof for the formal connection between MEL and tMEL, the Temporalization Theorem, which states that every MEL theorem can be turned into a tMEL theorem if suitable time labels can be inserted to the knowledge statements involved in the MEL theorem. This result shows that MEL is dynamic in nature and the hidden temporal structure is revealed in the formalism of tMEL.

6. Syraya Chin-Mu Yang (楊金穆; 台大哲學系教授)

Title: A Defence of the Knowledge Norm of Assertion: From a Model-theoretical Perspective

Abstract: I defend the knowledge norm of assertion (KNA─'One must: assert ρ only if one knows ρ´, also referred to as the K-rule) by constructing a class of TW-models for epistemic logic, Kripke models in character, which will satisfy the main theses of Timothy Williamson's knowledge first epistemology. I start with a brief introduction of main epistemic characters of assertion and then examine some popular accounts of assertion, including the truth-rule, the warrant rule and the knowledge rule. I show that assertion, as an intentional speech act, neither merely intends to transmit agent's belief, nor to express a certain truth. I next describe the construction of TW-models for a modal language containing the modal operators K('knows'), B('believes'), and A('asserts'). Semantic rules for Kφ, Bφ, and Aφ will be given. In particular, the semantic rules for Bφ and Aφ are so stipulated such that the truth value of Bφ (or Aφ, respectively) at a certain state can be determined by virtue of truth values of the corresponding Kφ in some related states. This will provide a model-theoretical justification of the knowledge rule. Moreover, it can be argued that the TB rule (i.e. One must: assert ρ only if one believes ρ and ρ is true) will either collapse into the Knowledge rule, if one adopt a holistic view like Davidson, or become a version of warrant rule. I further argue that the BK rule (i.e. One must: assert ρ only if one believes that one knows ρ) will either collapse into the Knowledge rule or become a naive but unacceptable thesis that assertion merely aims at expressing agent's belief. A similar argument with appropriate modification goes for the RBK rule (i.e. One must: assert ρ only if one rationally believes that one knows ρ). The semantic rule for rational (or justified) belief (B^jφ, in symbols) will be given in due course. These will illustrate Williamson's underlying thought that there is no good reason to accept a belief-based account of assertion. Finally, I show that the problem of logical omniscience can be avoided on TW-models.

6. Syraya Chin-Mu Yang (楊金穆; 台大哲學系教授)

7. Charles Chih-Hi Liu, I-Jen Chiang, Jau-Min Wong

Title: Mapping Knowledge Evolution by Co-word Analysis of PubMed Literature

Abstract: We propose a new method of mapping knowledge evolution of biomedical domains, based on co-word analysis of PubMed literature. The model introduces the time factor into co-word network analysis. By adjustment of the threshold of node display heuristically, the dynamics of knoweldge and concept evolution could be evaluated. The results of two datasets were compared -- the TKI set from the 591 PubMed articles on "tyrosine kinase inbitor" and "lung cancer" between 2001 and 2010; and the BDD set from the 188 and 83 articles on "body dysmorphic disorder" with and without the topic of "surgery" between 1991 and 2010. The TKI literature map reveals a "paradigm shift" from basic science before 2005 toward the cancer chemotherapy application after 2008. The BDD map is relative stable across time.