Yanjing Wang
Department of Philosophy Peking University
Proceeding Paper
Publication Types:
Strong Permission Bundled: First Steps
In this paper, we introduce a novel framework for deontic logic of strong permission that accommodates free choice. Our approach treats permission as a bundled modality, which combines a universal quantifier with a possibility modality such that an action type 
is permitted if and only if every token of can be executed in some deontically ideal world. Our formalization of action tokens and their types is inspired by the BHK-style interpretation for intuitionistic logic. We axiomatize the logics of strong permission under various conditions. In addition to satisfying the desirable logical requirements found in the literature, our framework also predicts interesting new phenomena related to permission and distribution laws that align with our linguistic intuition.
Epistemic Syllogistic: First Steps
Aristotle’s discussions on modal syllogistic have often been viewed as error-prone and have garnered significant attention in the literature due to historical interests. However, from a contemporary standpoint, they also introduced natural fragments of first-order modal logic, warranting a comprehensive technical analysis. In this paper, drawing inspiration from the natural logic program, we propose and examine several variants of modal syllogistic within the epistemic context, thereby coining the term “epistemic syllogistic.” Specifically, we concentrate on the de re interpretation of epistemic syllogisms containing non-trivial yet natural expressions such as “all things known to be A are also known to be not B.” We explore the epistemic apodeictic syllogistic and its extensions, which accommodate more complex terms. Our main contributions include several axiomatizations of these logics, with completeness proofs that may be of independent interest.
Lattice theory has intimate connections with modal logic via algebraic semantics and lattices of modal logics. However, one less explored direction is to view lattices as relational structures extending partial orders, and study the modal logic over them. In this paper, following the earlier steps of Burgess and van Benthem in the 1980s, we use the basic tense logic and its extension with infimum and supremum binary modalities and nominals to talk about lattices based on Kripke semantics. As the main results and also the first steps of a general research program, we obtain a series of complete finite axiomatizations of lattices and (un)bounded lattices.
Generalized Bundled Fragments of First-order Modal Logic
When we bundle quantifiers and modalities together (as in $\exists x \Box$, $\Diamond \forall x$ etc.) in first-order modal logic (FOML), we get new logical operators whose combinations produce interesting \textit{bundled} fragments of FOML. It is well-known that finding decidable fragments of \FOML is hard, but existing work shows that certain bundled fragments are decidable [Padmanabha et al 2018], without any restriction on the arity of predicates, the number of variables, or the modal scope. In this paper, we explore generalized bundles such as $\forall x\forall y \Box, \forall x\exists y \Diamond$ etc., and map the terrain with regard to decidability, presenting both decidability and undecidability results. In particular, we propose the loosely bundled fragment which is decidable over increasing domains and encompasses all known decidable bundled fragments.
An Epistemic Interpretation of Tensor Disjunction
In this paper, we present an epistemic interpretation of the tensor disjunction in dependence logic, inspired by the weak disjunction studied by Medvedev under a formalized BHK-like semantics. To put the tensor disjunction in the same picture with intuitionistic and classical disjunctions, we give an alternative epistemic semantics to inquisitive logic with tensor, studied by Ciardelli and Barbero (2019). We then use a much more powerful epistemic language with propositional quantifiers to give a complete axiomatization where the non-classical formulas are reduced in the system to classical but epistemic ones. It also turns out that the idea of the tensor disjunction can be generalized greatly without adding expressive power, resulting in a (k, n)-parametrized general tensor that captures the epistemic state that knowing k out of n given answers to the corresponding n questions are correct. The standard tensor is simply a special case where k=1 and n=2.
Knowing How to Plan
Various planning-based know-how logics have been proposed and studied in the recent literature. In this paper, we use such a logic to do know-how-based planning via model checking. In particular, we can handle the higher-order epistemic planning involving know-how formulas as the goal, e.g., find a plan to make sure p such that the adversary does not know how to make p false afterward. We give a PTIME-algorithm for the model checking problem over finite epistemic transition systems and axiomatize the logic under the assumption of perfect recall.
Hypergraphs, local reasoning, and weakly aggregative modal logic
Abstract. This paper connects the following three apparently unrelated topics: an epistemic framework fighting logical omniscience, a class of generalized graphs without the arities of relations, and a family of nonnormal modal logic rejecting the aggregative axiom. Through neighborhood frames as their meeting point, we show that, among many completeness results obtained in this paper, the limit of a family of weakly aggregative logics is both exactly the modal logic of hypergraphs and also the epistemic logic of local reasoning with veracity and positive introspection, which also answers a question left open by Fagin and Halpern (1988). The logics studied are shown to be decidable based on a filtration construction.
In this paper, we propose a lightweight yet powerful dynamic epistemic logic that not only captures the distinction between de dicto and de re knowledge but also the distinction between de dicto and de re updates. The logic is based on the dynamified version of an epistemic language extended with the assignment operator borrowed from dynamic logic, following the work of Wang and Seligman (2018). We obtain complete axiomatizations for the counterparts of public announcement logic and event-model-based DEL based on new reduction axioms taking care of the interactions between dynamics and assignments.
Weakly Aggregative Modal Logic: Characterization and Interpolation
Abstract. Weakly Aggregative Modal Logic (WAML) is a collection of disguised polyadic modal logics with n-ary modalities whose arguments are all the same. WAML has some interesting applications on epistemic logic and logic of games, so we study some basic model theoretical aspects of WAML in this paper. Specically, we give a van Benthem-Rosen characterization theorem of WAML based on an intuitive notion of bisimulation and show that each basic WAML system Kn lacks Craig Interpolation.
Multi-agent knowing how via multi-step plans: a dynamic epistemic planning based approach
Abstract. There are currently two approaches to the logic of knowing how: the planning-based one and the coalition-based one. However, the rst is single-agent, and the second is based on single-step joint actions. In this paper, to overcome both limitations, we propose a multi-agent framework for the logic of knowing how, based on multi-step dynamic epistemic planning studied in the literature. We obtain a sound and com- plete axiomatization and show that the logic is decidable, although the corresponding multi-agent epistemic planning problem is undecidable.
Knowledge-now and Knowledge-all
Abstract: In this paper, we propose a logical framework extending the standard epistemic logic with a new knowledge operator $\G_i$ which captures the knowledge about (physically) necessary facts, e.g., scientific knowledge. Semantically, the truth of $\G_i\phi$ depends on not only the epistemically indistinguishable worlds from the current real world but also the relevant (physically) possible worlds which are clearly distinguishable. Essentially, $\G_i$ is a bundle of the standard epistemic modality and a necessity-like modality. We axiomatize the corresponding epistemic logic completely in single- and multi-agent cases with interesting interaction axioms between the two epistemic operators.
How to Agree without Understanding Each Other: Public Announcement Logic with Boolean Definitions
Abstract. In standard epistemic logic, knowing that p is the same as knowing that p is true, but it does not say anything about understanding p or knowing its meaning. In this paper, we present a conservative extension of Public Announcement Logic (PAL) in which agents have knowledge or belief about both the truth values and the meanings of propositions. We give a complete axiomatization of PAL with Boolean Definitions and discuss various examples. An agent may understand a proposition without knowing its truth value or the other way round. Moreover, multiple agents can agree on something without agreeing on its meaning and vice versa.
When Names Are Not Commonly Known: Epistemic Logic with Assignments
Abstract: In standard epistemic logic, agent names are usually assumed to be common knowledge implicitly. This is unreasonable for various applications. Inspired by term modal logic and assignment operators in dynamic logic, we introduce a lightweight modal predicate logic where names can be non-rigid. The language can handle various de dicto and de re distinctions in a natural way. The main technical result is a complete axiomatisation of this logic over S5 models.
Bundled fragments of first-order modal logic: (un)decidability
Abstract: Quantified modal logic provides a natural logical language for reasoning about modal attitudes even while retaining the richness of quantification for referring to predicates over domains. But then most fragments of the logic are undecidable, over many model classes. Over the years, only a few fragments (such as the monodic) have been shown to be decidable. In this paper, we study fragments that bundle quantifiers and modalities together, inspired by earlier work on epistemic logics of know-how/why/what. As always with quantified modal logics, it makes a significant difference whether the domain stays the same across worlds, or not. In particular, we show that the bundle 
is undecidable over constant domain interpretations, even with only monadic predicates, whereas 
bundle is decidable. On the other hand, over increasing domain interpretations, we get decidability with both and bundles with unrestricted predicates. In these cases, we also obtain tableau based procedures that run in PSPACE. We further show that the bundle cannot distinguish between constant domain and increasing domain interpretations.
Strategically knowing how
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 
means that there exists a (uniform) strategy such that the agent knows that it can make sure . 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.
Knowing values and public inspection
Abstract: We present a basic dynamic epistemic logic of “knowing the value”. Analogous to public announcement in standard DEL, we study “public inspection”, a new dynamic operator which updates the agents’ knowledge about the values of constants.We provide a sound and strongly complete axiomatization for the single and multi-agent case, making use of the well-known Armstrong axioms for dependencies in databases.
Achieving while maintaining: A logic of knowing how with intermediate constraints
Abstract: In this paper, we propose a ternary knowing how operator to express that the agent knows how to achieve $\phi$ given $\psi$ while maintaining $\chi$ in-between. It generalizes the logic of goal-directed knowing how proposed by Wang in [10]. We give a sound and complete axiomatization of this logic.
A New Modal Framework for Epistemic Logic
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 
, e.g., knowing how to achieve roughly means that there exists a way such that you know that it is a way to ensure that 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.
Knowing value logic as a normal modal logic
Abstract. Recent years witness a growing interest in nonstandard epistemic logics of “knowing whether”, “knowing what”, “knowing how”, and so on. These logics are usually not normal, i.e., the standard axioms and reasoning rules for modal logic may be invalid. In this paper, we show that the conditional “knowing value” logic proposed by Wang and Fan (2013) can be viewed as a disguised normal modal logic by treating the negation of the Kv operator as a special diamond. Under this perspective, it turns out that the original first-order Kripke semantics can be greatly simplified by introducing a ternary relation 
in standard Kripke models, which associates one world with two i-accessible worlds that do not agree on the value of constant c. Under intuitive constraints, the modal logic based on such Kripke models is exactly the one studied by Wang and Fan (2013,2014). Moreover, there is a very natural binary generalization of the “knowing value” diamond, which, surprisingly, does not increase the expressive power of the logic. The resulting logic with the binary diamond has a transparent normal modal system, which sharpens our understanding of the “knowing value” logic and simplifies some previously hard problems.
Representing Imperfect Information of Procedures with Hyper Models
Abstract. When reasoning about knowledge of procedures under imperfect information, the explicit representation of epistemic possibilities blows up the S5-like models of standard epistemic logic. To overcome this drawback, in this paper, we propose a new logical framework based on compact models without epistemic accessibility relations for reasoning about knowledge of procedures. Inspired by the 3-valued abstraction method in model checking, we introduce hyper models which encode the imperfect procedural information. We give a highly non-trivial 2-valued semantics of epistemic dynamic logic on such models while validating all the usual S5 axioms. Our approach is suitable for applications where procedural information is ‘learned’ incrementally, as demonstrated by various examples.
A logic of knowing how
Abstract: In this paper, we propose a single-agent modal logic framework for reasoning about goal-direct “knowing how” based on ideas from linguistics, philosophy, modal logic and automated planning. We first define a modal language to express “I know how to guarantee phi given $\psi$” with a semantics not based on standard epistemic models but labelled transition systems that represent the agent’s knowledge of his own abilities. A sound and complete proof system is given to capture the valid reasoning patterns about “knowing how” where the most important axiom suggests its compositional nature.
A Dynamic Epistemic Framework for Conformant Planning
Abstract: In this paper, we introduce a lightweight dynamic epistemic logical framework for automated plan-ning under initial uncertainty. We reduce plan verification and conformant planning to model check-ing problems of our logic. We show that the model checking problem of the iteration-free fragment is PSPACE-complete. By using two non-standard (but equivalent) semantics, we give novel model checking algorithms to the full language and the iteration-free language.
Conditionally knowing what
Abstract. Classic epistemic logic focuses on propositional knowledge expressed by “knowing that” operators. However, there are various types of knowledge used in natural language, in terms of “knowing how”, “knowing whether”, “knowing what”, and so on. In [10], Plaza proposed an intuitive know-what operator which was generalized in [16] by introducing a condition. The latter know-what operator can express natural conditional knowledge such as $\backslash$I know what your password is, if it is 4-digits”, which is not simply a material implication. Essentially this know-what operator packages a first-order quantifier and an S5-modality together in a non-trivial way, thus making it hard to axiomatize. In [16] an axiomatization is given for the single-agent epistemic logic with both know-that and know-what operators, while leaving axiomatizing the multi-agent case open due to various technical difficulties. In this paper, we solve this open problem. The completeness proof is highly non-trivial, compared to the singleagent case, which requires different techniques inspired by first-order intensional logic.
Almost necessary
Abstract. A formula is contingent if it is possibly true and possibly false. A formula is non- contingent if it is not contingent, i.e., if it is necessarily true or necessarily false. In an epistemic setting, a formula is contingent’ means that you are ignorant about its value, whereas a formula is non-contingent’ means that you know whether it is true. Although non-contingency is definable in terms of necessity as above, necessity is not always definable in terms of non-contingency, as studied in the literature. We propose an almost-definability’ schema AD for non-contingency logic, the logic with the noncontingency operator as the only modality, making precise when necessity is definable with non-contingency. Based on AD we propose a notion of bisimulation for non- contingency logic, and characterize non-contingency logic as the (non-contingency) bisimulation invariant fragment of modal logic and of first-order logic. A known pain for non-contingency logic is the absence of axioms characterizing frame properties. This makes it harder to find axiomatizations of non-contingency logic over given frame classes. In particular, no axiomatization over symmetric frames is known, despite the rich results about non-contingency logic obtained in the literature since the 1960s. We demonstrate that the almost-definability’ schema AD can guide our search for proper axioms for certain frame properties, and help us in defining the canonical models. Following this idea, as the main result, we give a complete axiomatization of non-contingency logic over symmetric frames.
Knowing that, knowing what, and public communication: Public announcement logic with Kv operators
An alternative axiomatization of DEL and its applications
Not All Those Who Wander Are Lost: Dynamic Epistemic Reasoning in Navigation
Abstract. In everyday life, people get lost even when they have the map: they simply may not know where they are in the map. However, when moving forward they may have new observations which can help to locate themselves by reasoning. In this paper, we propose and develop a semantic-driven dynamic epistemic framework to handle epistemic reasoning in such navigation scenarios. Our framework can be viewed as a careful blend of dynamic epistemic logic and epistemic temporal logic, thus enjoying features from both frameworks. We made an in-depth study on many model theoretical aspects of the proposed framework and provide a complete axiomatization.
Reasoning about protocol change and knowledge
Abstract. In social interactions, protocols govern our behavior and assign meaning to actions. In this paper, we investigate the dynamics of protocols and their epistemic effects. We develop two logics, inspired by Propositional Dynamic Logic (PDL) and Public Announcement Logic (PAL), for reasoning about protocol change and knowledge updates. We show that these two logics can be translated back to the standard PDL and PAL respectively.
On axiomatizations of PAL
Abstract. In the literature, different axiomatizations of Public Announcement Logic (PAL) were proposed. Most of these axiomatizations share a ‘core set’ of the so-called reduction axioms. In particular, there is a composition axiom which stipulates how two consecutive announcements are composed into one. In this paper, by designing non-standard Kripke semantics for the language of PAL, we show that without the composition axiom the core set does not completely axiomatize PAL. In fact, most of the intuitive ‘axioms’ and rules we took for granted could not be derived from the core set. The non-standard semantics we proposed is of its own interest in modelling realistic agents. We show that with the help of different composition axioms we may axiomatize PAL w.r.t. such non-standard semantics.
Logic of information flow on communication channels (full paper)
Abstract. In this paper, we develop an epistemic logic for specifying and reasoning about information flow on the underlying communication channels. By combining ideas from Dynamic Epistemic Logic (DEL) and Interpreted Systems (IS), our semantics offers a natural and neat way of modeling multi-agent communication scenarios with different assumptions about the observational power of agents. We relate our logic to the standard DEL and IS approaches and demonstrate its use by studying a telephone call communication scenario.
Abstract appeared at AAMAS2010
Hidden protocols
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 logic to reason about knowledge in such scenarios.
(largely extended journal version of the TARK2011 paper)
Verifying epistemic protocols under common knowledge
Abstract. Epistemic protocols are communication protocols aiming at transfer of knowledge in a controlled way. Typically, the preconditions or goals for protocol actions depend on the knowledge of agents, often in nested form. Informal epistemic protocol descriptions for muddy children, coordinated attack, dining cryptographers, Russian cards, secret key exchange are well known. The contribution of this paper is a formal study of a natural requirement on epistemic protocols, that the contents of the protocol can be assumed to be common knowledge. By formalizing this requirement we can prove that there can be no unbiased deterministic protocol for the Russian cards problem. For purposes of our formal analysis we introduce an epistemic protocol language, and we show that its model checking problem is decidable.
Refinement of Kripke Models for dynamics
Abstract. We propose a property-preserving refinement/abstraction theory for Kripke Modal Labelled Transition Systems incorporating not only state mapping but also label and proposition lumping, in order to have a compact but informative abstraction. We develop a 3-valued version of Public Announcement Logic (PAL) which has a dynamic operator that changes the model in the spirit of public broadcasting. We prove that the refinement relation on static models assures us to safely reason about any dynamic properties in terms of PAL-formulas on the abstraction of a model. The theory is in particular interesting and applicable for an epistemic setting as the example of the Muddy Children puzzle shows, especially in the view of the growing interest for epistemic modelling and (automatic) verification of communication protocols.
Propositional dynamic logic as a logic of belief revision
PDL over accelerated labeled transition systems
Abstract. We present a thorough study of Propositional Dynamic Logic over a variation of labeled transition systems, called accelerated labelled transition systems, which are transition systems labeled with regular expressions over action labels. We study the model checking and satisfiability decision problems. Through a notion of regular expression rewriting, we reduce these two problems to the corresponding ones of PDL in the traditional semantics (w.r.t. LTS). As for the complexity, both of problems are proved to be EXPSPACE-complete. Moreover, the program, complexity of model checking problem turns out to be Nlogspace-complete. Furthermore, we provide an axiomatization for PDL which involves Kleene Algebra as an Oracle. The soundness and completeness are shown.
