Planning-based knowing how: a unified approach

AIJBeyond know-thatJournal PaperSelected
Yanjun Li, Yanjing Wang
Artificial Intelligence, Volume 296, July 2021, 103487
Publication year: 2021

Various logical notions of know-how have been recently proposed and studied in the literature based on different types of epistemic planning in different frameworks. This paper proposes a unified logical framework to incorporate the existing and some new notions of know-how. We define the semantics of the know-how operator using a unified notion of epistemic planning with parameters of different types of plans specified by a programming language. Surprisingly, via a highly unified completeness proof, we show that all the ten intuitive notions of plans discussed in this paper lead to exactly the same know-how logic, which is proven to be decidable. We also show that over finite models, the know-how logic based on knowledge-based plans requires an extension with an axiom capturing the compositionality of the plans. In the context of epistemic planning, our axiomatization results reveal the core principles behind the very idea of epistemic planning, independent of the particular notion of plans. Moreover, since epistemic planning can be expressed by the know-how modality in our object language, we can greatly generalize the planning problems that can be solved formally by model checking various formulas in our know-how language.

Neighborhood Semantics for Logic of Knowing How

Beyond know-thatJournal PaperSelectedSynthese
Yanjun Li, Yanjing Wang
Synthese (accpeted)
Publication year: 2021

In this paper, we give an alternative semantics to the non-normal logic of knowing how proposed by Fervari et al. (2017), based on a class of Kripke neighbor-hood models with both the epistemic relations and neighborhood structures. This alternative semantics is inspired by the same quantifier alternation pattern of ∃∀in the semantics of the know-how modality and the (monotonic) neighborhood semantics for the standard modality. We show that this new semantics is equivalent to the original Kripke semantics in terms of the validities. A key result is a representation theorem showing that the more abstract Kripke neighborhood models can be represented by the concrete Kripke models with action transitions modulo the valid formulas. We prove the completeness of the logic for the neighborhood semantics. The neighborhood semantics can be adapted to other variants of logics of knowing how. It provides us a powerful technical tool to study these logics while preserving the basic semantic intuition.

Beyond Knowing That: A New Generation of Epistemic Logics

Beyond know-thatBook ChapterSelected
Wang, Yanjing
Jaakko Hintikka on knowledge and game theoretical semantics, Springer, 12: 499—533, 2018
Publication year: 2018


Abstract. Epistemic logic has become a major field of philosophical logic ever since the groundbreaking work by Hintikka (1962). Despite its various successful applications in theoretical computer science, AI, and game theory, the technical development of the field has been mainly focusing on the propositional part, i.e., the propositional modal logics of “knowing that”. However, knowledge is expressed in everyday life by using various other locutions such as “knowing whether”, “knowing what”, “knowing how” and so on (knowing-wh hereafter). Such knowledge expressions are better captured in quantified epistemic logic, as was already discussed by Hintikka (1962) and his sequel works at length. This paper aims to draw the attention back again to such a fascinating but largely neglected topic. We first survey what Hintikka and others did in the literature of quantified epistemic logic, and then advocate a new quantifier-free approach to study the epistemic logics of knowing-wh, which we believe can balance expressivity and complexity, and capture the essential reasoning patterns about knowing-wh. We survey our recent line of work on the epistemic logics of “knowing whether”, “knowing what” and “knowing how” to demonstrate the use of this new approach.

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)

Strategically knowing how

Beyond know-thatIJCAIProceeding PaperSelected
Fervari, Raul and Herzig, Andreas and Li, Yanjun and Wang, Yanjing
In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI) 2017, 2017
Publication year: 2017

Abstract. In this paper, we propose a single-agent logic of goal-directed knowing how extending the standard epistemic logic of knowing that with a new knowing how operator. The semantics of the new operator is based on the idea that knowing how to achieve \phi means that there exists a (uniform) strategy such that the agent knows that it can make sure \phi. We give an intuitive axiomatization of our logic and prove the soundness, completeness, and decidability of the logic. The crucial axioms relating knowing that and knowing how illustrate our understanding of knowing how in this setting. This logic can be used in representing both knowledge-that and knowledge-how.

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.


(largely extended journal version of the TARK2015 paper)

A New Modal Framework for Epistemic Logic

Beyond know-thatProceeding PaperSelectedTARK
Wang, Yanjing
Proceedings of Conference on Theoretical Aspects of Rationality and Knowledge (TARK) 2017, 251: 515—534, 2017
Publication year: 2017

Abstract: Recent years witnessed a growing interest in non-standard epistemic logics of knowing whether, knowing how, knowing what, knowing why and so on. The new epistemic modalities introduced in those logics all share, in their semantics, the general schema of \exists x\phi, e.g., knowing how to achieve \phi roughly means that there exists a way such that you know that it is a way to ensure that \phi Moreover, the resulting logics are decidable. Inspired by those particular logics, in this work, we propose a very general and powerful framework based on quantifier-free predicate language extended by a new modality x, which packs exactly x together. We show that the resulting language, though much more expressive, shares many good properties of the basic propositional modal logic over arbitrary models, such as finite-tree-model property and van Benthem-like characterization w.r.t. first-order modal logic. We axiomatize the logic over S5 frames with intuitive axioms to capture the interaction between x and know-that operator in an epistemic setting.

Contingency and Knowing Whether

Beyond know-thatJournal PaperRSLSelected
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 Kw(\phi \to \psi)\to(Kw \phi\to \psi) 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)

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.

A preliminary version of this paper was presented at LOFT 2010.