Publication Types:

A logic of knowing why

Beyond know-thatJournal PaperSynthese
Xu, Chao and Wang, Yanjing and Studer, Thomas
Synthese, To appear, 2019
Publication year: 2019

Abstract. When we say “I know why he was late”, we know not only the fact that he was late, but also an explanation of this fact. We propose a logical framework of “knowing why” inspired by the existing formal studies on why-questions, scientific explanation, and justification logic. We introduce the $Ky_i$ operator into the language of epistemic logic to express “agent i knows why phi” and propose a Kripke-style semantics of such expressions in terms of knowing an explanation of phi. We obtain two sound and complete axiomatizations w.r.t. two different model classes depending on different assumptions about introspection.

A dynamic epistemic framework for reasoning about conformant probabilistic plans

AIJJournal Paper
Li, Yanjun and Kooi, Barteld and Wang, Yanjing
Artificial Intelligence, 268: 54—84, 2019
Publication year: 2019

Abstract: In this paper, we introduce a probabilistic dynamic epistemic logical framework that can be applied for reasoning and verifying conformant probabilistic plans in a single agent setting. In conformant probabilistic planning (CPP), we are looking for a linear plan such that the probability of achieving the goal after executing the plan is no less than a given threshold probability $\delta$. Our logical framework can trace the change of the belief state of the agent during the execution of the plan and verify the conformant plans. Moreover, with this logic, we can enrich the CPP framework by formulating the goal as a formula in our language with action modalities and probabilistic beliefs. As for the main technical results, we provide a complete axiomatization of the logic and show the decidability of its validity problem.

True lies

Journal PaperSynthese
AAgotnes, Thomas and van Ditmarsch, Hans and Wang, Yanjing
Synthese, 195(10): 4581—4615, 2018
Publication year: 2018

Abstract: A true lie is a lie that becomes true when announced. In a logic of announcements, where the announcing agent is not modelled, a true lie is a formula (that is false and) that becomes true when announced. We investigate true lies and other types of interaction between announced formulas, their preconditions and their postconditions, in the setting of Gerbrandy’s logic of believed announcements, wherein agents may have or obtain incorrect beliefs. Our results are on the satisfiability and validity of instantiations of these semantically defined categories, on iterated announcements, including arbitrarily often iterated announcements, and on syntactic characterization. We close with results for iterated announcements in the logic of knowledge (instead of belief), and for lying as private announcements (instead of public announcements) to different agents. Detailed examples illustrate our lying concepts.

A logic of goal-directed knowing how

Beyond know-thatJournal PaperSelectedSynthese
Wang, Yanjing
Synthese, 195(10): 4419—4439, 2018
Publication year: 2018

Abstract: In this paper, we propose a decidable single-agent modal logic for reasoning about goal-directed “knowing how”, based on ideas from linguistics, philosophy, modal logic, and automated planning in AI. We first define a modal language to express “I know how to guarantee (Formula presented.) given (Formula presented.)” with a semantics based not on standard epistemic models but on labeled transition systems that represent the agent’s knowledge of his own abilities. The semantics is inspired by conformant planning in AI. A sound and complete proof system is given to capture valid reasoning patterns, which highlights the compositional nature of “knowing how”. The logical language is further extended to handle knowing how to achieve a goal while maintaining other conditions.

(This is an extended journal version of the LORI2015 paper)

More for free: A dynamic epistemic framework for conformant planning over transition systems

Journal PaperSelected
Li, Yanjun and Yu, Quan and Wang, Yanjing
Journal of Logic and Computation, 27(8): 2383—2410, 2017
Publication year: 2017

Abstract: In this article, we introduce a lightweight dynamic epistemic logical framework for automated planning under initial uncertainty. We generalize the standard conformant planning problem in AI (over transition systems) in two crucial aspects: first, the planning goal can be any formula expressed in an epistemic propositional dynamic logic (EPDL); second, procedural constraints of the desired plan specified by regular expressions can be imposed. We then reduce the problem of generalized conformant planning to the model checking problem of our logic. Although our conformant planning problem is much more general than the standard one with Boolean goals and no procedural constraints, the complexity is still PSPACE-complete which is equally hard as standard conformant planning over explicit transition systems.

Beyond know-thatJournal Paper
Lau, Tszyuen and Wang, Yanjing
Philosophical Forum, 47(3-4): 415—423, 2016
Publication year: 2016

Abstract：In this article, we present an attempt to reconcile intellectualism and the anti-intellectualist ability account of knowledge-how by reducing “S knows how to F” to, roughly speaking, “S knows that she has the ability to F demonstrated by a concrete way w.” More precisely, “S has a certain ability” is further formalized as the proposition that S can guarantee a certain goal by a concrete way w of some method under some precondition. Having the knowledge of our own ability, we can plan our future actions accordingly, which would not be possible by merely having the ability without knowing it, and this pinpoints the crucial difference between knowledge-how and ability. Our semi-formal account avoids most of the objections to both intellectualism and the anti-intellectualist ability account and provides a multistage learning process of knowledge-how, which reveals various subtleties.

From rules to runs: A dynamic epistemic take on imperfect information games

Journal Paper
Li, Kai and Wang, Yanjing
Studies in Logic, 8(4): 74—107, 2015
Publication year: 2015

Abstract: In the literature of game theory, the information sets of extensive form games have different interpretations, which may lead to confusions and paradoxical cases. We argue that the problem lies in the mix-up of two interpretations of the extensive form game structures: game rules or game runs which do not always coincide. In this paper, we try to separate and connect these two views by proposing a dynamic epistemic framework in which we can compute the runs step by step from the game rules plus the given assumptions of the players. We propose a modal logic to describe players’ knowledge and its change during the plays, and provide a complete axiomatization. We also show that, under certain conditions, the mix-up of the rules and the runs is not harmful due to the structural similarity of the two.

Contingency and Knowing Whether

Beyond know-thatJournal PaperSelected
Fan, Jie and Wang, Yanjing and Ditmarsch, Hans Van
Review of Symbolic Logic, 8(1): 75—107, 2015
Publication year: 2015

Abstract: A proposition is noncontingent, if it is necessarily true or it is necessarily false. In an epistemic context, ‘a proposition is noncontingent’ means that you know whether the proposition is true. In this paper, we study contingency logic with the noncontingency operator ? but without the necessity operator 2. This logic is not a normal modal logic, because is not valid. Contingency logic cannot define many usual frame properties, and its expressive power is weaker than that of basic modal logic over classes of models without reflexivity. These features make axiomatizing contingency logics nontrivial, especially for the axiomatization over symmetric frames. In this paper, we axiomatize contingency logics over various frame classes using a novel method other than the methods provided in the literature, based on the ‘almost-definability’ schema AD proposed in our previous work. We also present extensions of contingency logic with dynamic operators. Finally, we compare our work to the related work in the fields of contingency logic and ignorance logic, where the two research communities have similar results but are apparently unaware of each other’s work. One goal of our paper is to bridge this gap.

Hidden protocols: Modifying our expectations in an evolving world

AIJJournal PaperSelected
Van Ditmarsch, Hans and Ghosh, Sujata and Verbrugge, Rineke and Wang, Yanjing
Artificial Intelligence, 208(1): 18—40, 2014
Publication year: 2014

Abstract. When agents know a protocol, this leads them to have expectations about future observations. Agents can update their knowledge by matching their actual observations with the expected ones. They eliminate states where they do not match. In this paper, we study how agents perceive protocols that are not commonly known, and propose a semantics-driven logical framework to reason about knowledge in such scenarios. In particular, we introduce the notion of epistemic expectation models and a propositional dynamic logic-style epistemic logic for reasoning about knowledge via matching agents’ expectations to their observations. It is shown how epistemic expectation models can be obtained from epistemic protocols. Furthermore, a characterization is presented of the effective equivalence of epistemic protocols. We introduce a new logic that incorporates updates of protocols and that can model reasoning about knowledge and observations. Finally, the framework is extended to incorporate fact-changing actions, and a worked-out example is given.

(Extended journal version of the TARK2011 paper)

Book Review: Logical Dynamics of Information and Interaction

Journal Paper
Wang, Yanjing
Studia Logica, 102(3): 647—654, 2014
Publication year: 2014

Abstract. An extensive review of Johan van Benthem’s book Logical Dynamics of Information and Interaction

Reasoning about agent types and the hardest logic puzzle ever

Journal PaperSelected
Liu, Fenrong and Wang, Yanjing
Minds and Machines, 23(1): 123—161, 2013
Publication year: 2013

Abstract. In this paper, we first propose a simple formal language to specify types of agents in terms of necessary conditions for their announcements. Based on this language, types of agents are treated as ‘first-class citizens’ and studied extensively in various dynamic epistemic frameworks which are suitable for reasoning about knowledge and agent types via announcements and questions. To demonstrate our approach, we discuss various versions of Smullyan’s Knights and Knaves puzzles, including the Hardest Logic Puzzle Ever (HLPE) proposed by Boolos (in Harv Rev Philos 6:62-65, 1996). In particular, we formalize HLPE and verify a classic solution to it. Moreover, we propose a spectrum of new puzzles based on HLPE by considering subjective (knowledge-based) agent types and relaxing the implicit epistemic assumptions in the original puzzle. The new puzzles are harder than the previously proposed ones in the literature, in the sense that they require deeper epistemic reasoning. Surprisingly, we also show that a version of HLPE in which the agents do not know the others’ types does not have a solution at all. Our formalism paves the way for studying these new puzzles using automatic model checking techniques.

On axiomatizations of public announcement logic

Journal PaperSelectedSynthese
Wang, Yanjing and Cao, Qinxiang
Synthese, 190(SUPPL.1): 103—134, 2013
Publication year: 2013

Abstract. In the literature, different axiomatizations of Public Announcement Logic (PAL) have been proposed. Most of these axiomatizations share a “core set” of the so-called “reduction axioms”. In this paper, by designing non-standard Kripke semantics for the language of PAL, we show that the proof system based on this core set of axioms does not completely axiomatize PAL without additional axioms and rules. In fact, many of the intuitive axioms and rules we took for granted could not be derived from the core set. Moreover, we also propose and advocate an alternative yet meaningful axiomatization of PAL without the reduction axioms. The completeness is proved directly by a detour method using the canonical model where announcements are treated as merely labels for modalities as in normal modal logics. This new axiomatization and its completeness proof may sharpen our understanding of PAL and can be adapted to other dynamic epistemic logics.

(largely extended journal version of the LORI2011 paper)

Composing models

Journal PaperSelected
van Eijck, Jan and Sietsma, Floor and Wang, Yanjing
Journal of Applied Non-Classical Logics, 21(3-4): 397—425, 2011
Publication year: 2011

Abstract. We propose and study a new composition operation on (epistemic) multi-agent models with different vocabularies of propositional letters. This operation allows us to compose large models by small components representing agents’ partial observational information. Our investigation provides ways to decompose (locally generated) epistemic models such that the truth of certain formulas are preserved. By using the composition operation we also propose and study action model composition and action model updates on models with arbitrary vocabularies.

To know or not to know: Epistemic approaches to security protocol verification

Journal PaperSynthese
Dechesne, Francien and Wang, Yanjing
Synthese, 177(SUPPL. 1): 51—76, 2010
Publication year: 2010

Abstract.  Security properties naturally combine temporal aspects of protocols with aspects of knowledge of the agents. Since BAN-logic, there have been several initiatives and attempts to incorporate epistemics into the analysis of security protocols. In this paper, we give an overview of work in the field and present it in a unified perspective, with comparisons on technical subtleties that have been employed in different approaches. Also, we study to which degree the use of epistemics is essential for the analysis of security protocols. We look for formal conditions under which knowledge modalities can bring extra expressive power to pure temporal languages. On the other hand, we discuss the cost of the epistemic operators in terms of model checking complexity.