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.
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.
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)
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.
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.
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.
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.
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)
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.
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)
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.