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.
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.
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.
As a new type of epistemic logic, the logic of knowing how essentially captures the high-level epistemic reasoning about the knowledge of various plans to achieve certain goals. Existing work focuses on the axiomatizations of such logics. This paper makes the first study of their model theoretical properties, by introducing suitable notions of bisimulation for a family of five logics of knowing how based on various notions of plans. As an application of these notions of bisimulation, we study and compare the expressive power of these logics.
(A preliminary version of this paper was first presented at SR2017.)
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.
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.
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.
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.
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: 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.
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 . We give a sound and complete axiomatization of this 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.
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.
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.
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: 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.
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 , Plaza proposed an intuitive know-what operator which was generalized in  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  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.
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.