# strategically_knowing_how__e86ed39c.pdf

Strategically Knowing How

Raul Fervari University of C ordoba CONICET

Andreas Herzig University of Toulouse IRIT-CNRS

Yanjun Li University of Groningen Yanjing Wang

Peking University

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 and reasoning about both knowledge-that and knowledge-how.

1 Introduction

Standard epistemic logic focuses on reasoning about propositional knowledge expressed by knowing that ϕ [Hintikka, 1962]. However, in natural language, various other knowledge expressions are also frequently used, such as knowing what, knowing how, knowing why, and so on. In particular, knowing how receives much attention in both philosophy and AI. Epistemologists debate about whether knowledge-how is also propositional knowledge (cf. the survey [Fantl, 2008]), e.g., whether knowing how to swim can be rephrased using knowing that. In AI, it is crucial to let autonomous agents know how to fulﬁll certain goals in robotics, game playing, decision making, and multi-agent systems (cf. the surveys [Gochet, 2013; Agotnes et al., 2015]). In fact, a large body of AI planning can be viewed as ﬁnding algorithms to let the autonomous planner know how to achieve some propositional goals, i.e., to obtain goal-directed knowledge-how. Here, both propositional knowledge and knowledge-how matter, especially in the planning problems where initial uncertainty and non-deterministic actions are present. From a logician s point of view, it is interesting to see how knowing how interacts with knowing that, and how they differ in their reasoning patterns. A logic of knowing how also helps us to ﬁnd a consistency notion regarding knowledge database with knowing how expressions.

corresponding author (email: y.wang@pku.edu.cn)

s1 : p, q test q/ s3 : p, q pills/ s5 : p, q

s2 : p, q test q / s4 : p, q

pills 1 s6 : p, q

Figure 1: A scenario representing how to cure the pain.

Example 1.1. Consider the scenario where a doctor needs a plan to treat a patient and cure his pain (p), under the uncertainty about some possible allergy (q). If there is no allergy ( q) then simply taking some pills can cure the pain, and the surgery is not an option. On the other hand, in presence of the allergy, the pills may cure the pain or have no effect at all, while the surgery can cure the pain for sure. The model from Figure 1 represents this scenario with an additional action of testing whether q. The dotted line represents the initial uncertainty about q, and the test on q can eliminate this uncertainty (there is no dotted line between s3 and s4). According to the model, to cure the pain (guarantee p) at the end, it makes sense to take the surgery if the result of the test of whether q is positive and take the pills otherwise. We can say the doctor in this case knows how to cure the pain.

How to formalize the knowledge-how of the agent in such scenarios with uncertainty? Already since the early days of AI, people have been looking at it in the setting of logics of knowledge and action [Mc Carthy and Hayes, 1969; Mc Carthy, 1979; Moore, 1985; Lesp erance et al., 2000; van der Hoek et al., 2000]. However, there has been no consensus on how to capture the logic of knowing how formally (cf. the recent surveys [Gochet, 2013] and [ Agotnes et al., 2015]). The difﬁculties are well discussed in [Jamroga and Agotnes, 2007] and [Herzig, 2015]: simply combining the existing modalities for knowing that and ability in a logical language like ATEL [van der Hoek and Wooldridge, 2003] does not lead to a genuine notion of knowing how , e.g., knowing how to achieve p is not equivalent to merely knowing that there exists some strategy to make sure p. It does not work even when we replace the strategy by a uniform strategy where the agent has to choose the same action on indistinguishable states [Jamroga and Agotnes, 2007]. Let ϕ(x) express that x is a way to make sure some goal is achieved, and let K be the standard knowledge-that modality. There is a crucial distinction between the de dicto read-

Proceedings of the Twenty-Sixth International Joint Conference on Artiﬁcial Intelligence (IJCAI-17)

ing of knowing how (K xϕ(x)) and the desired de re reading ( x Kϕ(x)) endorsed also by linguists and philosophers [Stanley and Williamson, 2001]. The latter intuitively implies the former, but not the other way round. For example, consider a variant of Example 1.1 where no test is available: then the doctor has de dicto knowledge-how to cure, but not de re knowledge. Proposals to capture the de re reading have been discussed in the literature, such as making the knowledge operator more constructive [Jamroga and Agotnes, 2007], making the strategy explicitly speciﬁed [Herzig et al., 2013; Belardinelli, 2014], or inserting K in-between an existential quantiﬁer and the ability modality in see-to-it-that (STIT) logic [Broersen and Herzig, 2015]. In [Wang, 2015; 2016b], a new approach is proposed by introducing a single new modality Kh of (conditional) goaldirected knowing how, instead of breaking it down into other modalities. This approach is in line with other de re treatments of non-standard epistemic logics of knowing whether, knowing what and so on (cf. [Wang, 2016a] for a survey). The semantics of Kh is inspired by the idea of conformant planning based on linear plans [Smith and Weld, 1998; Yu et al., 2016]. It is shown that Kh is not a normal modality, e.g, knowing how to get drunk and knowing how to drive does not entail knowing how to drive when drunk. The work is generalized further in [Li and Wang, 2017; Li, 2017]. However, in these previous works, there was no explicit knowing that modality K in the language and the semantics of Kh is based on linear plans, which does not capture the broader notion allowing branching plans or strategies that are essential in the scenarios like Example 1.1. In this paper, we extend this line of work in the following aspects:

Both the knowing how modality Kh and knowing that modality K are in the language, and we capture the interactions of the two explicitly by several axioms. Accordingly, we have both the action transitions and epistemic uncertainty in the models.

In contrast to the essentially state-independent (global) semantics in [Wang, 2015; 2016b], we interpret Kh locally w.r.t. the local uncertainty, in accordance with the standard semantics for the knowing that operator K.

Instead of linear plans in [Wang, 2015], the semantics of our Kh operator is based on the existence of strategies (branching plans). In this way, the agent can make use of the knowledge learned during the execution of the plan, which helps us to capture situations where the agent intuitively knows how but does not have a linear plan.

The intuitive idea behind our semantics of Khϕ is that the agent knows how to achieve ϕ iff (s)he has an executable uniform strategy σ such that the agent knows that:

σ guarantees ϕ in the end given the uncertainty;

σ always terminates after ﬁnitely many steps.

Note that for an agent to know how to make sure ϕ, it is not enough to ﬁnd a plan which works de facto, but the agent should know it works in the end. This is a strong requirement inspired by planning under uncertainty, where the collection of ﬁnal possible outcomes after executing the plan is required

to be a subset of the collection of the goal states [Geffner and Bonet, 2013]. Technically, our contributions are summarized as follows: A logical language with both Kh and K operators with a semantics which ﬂeshes out formally the above intuitions about knowing how. A complete axiomatization with intuitive axioms. Decidability of our logic. The paper is organized as follows: Section 2 lays out the language and semantics of our framework; Section 3 proposes the axiomatization and proves its soundness; We prove the completeness of our proof system and show the decidability of the logic in Section 4 before we conclude with future work.

2 Language and Semantics Let PROP be a countable set of propositional symbols. Deﬁnition 2.1 (Language). The language is deﬁned by the following BNF where p PROP: ϕ := p | ϕ | (ϕ ϕ) | Kϕ | Khϕ.

We use , , as usual abbreviations and write ˆK for K . Deﬁnition 2.2 (Models). A model M is a quintuple W, ACT, , { a | a ACT}, V where: W is a non-empty set, ACT is a set of actions, W W is an equivalence relation on W,

a W W is a binary relation for each a ACT V : W 2PROP is a valuation. Note that the labels in ACT do not appear in the language but only in the models. The graph in Example 1.1 represents a model with omitted self-loops of (dotted lines), and the equivalence classes induced by are {s1, s2}, {s3}, {s4}, {s5}, {s6}. In this paper we do not require any properties between and a to lay out the most general framework. We will come back to particular assumptions like perfect recall at the end of the paper. Given a model and a state s, if there exists t such that s a t, we say that a is executable at s. Also note that the actions can be nondeterministic as in [Wang, 2015]. For each s W, we use [s] to denote the equivalence class {t W | s t}, and use [W] to denote the collection of all the equivalence classes on W w.r.t. . We use [s] a [t] to indicate that there are s [s] and t [t] such that s a t . If there is t W such that [s] a [t], we say a is executable at [s]. Deﬁnition 2.3 (Strategies). Given a model, a (uniformly executable) strategy is a partial function σ : [W] ACT such that σ([s]) is executable at all s [s]. Particularly, the empty function is also a strategy, the empty strategy. Note that the executability is as crucial as uniformity, without which knowledge-how may be trivialized. We use dom(σ) to denote the domain of σ. Function σ can be seen as a binary relation such that ([s], a), ([s], b) σ implies a = b. Therefore, if τ is a restriction of σ, i.e. τ σ, it follows that dom(τ) dom(σ), and τ([s]) = σ([s]) for all [s] dom(τ).

Proceedings of the Twenty-Sixth International Joint Conference on Artiﬁcial Intelligence (IJCAI-17)

Deﬁnition 2.4 (Executions). Given a strategy σ w.r.t a model M, a possible execution of σ is a possibly inﬁnite sequence

of equivalence classes δ = [s0][s1] such that [si] σ([si]) [si+1] for all 0 i < |δ|. Particularly, [s] is a possible execution if [s] dom(σ). If the execution is a ﬁnite sequence [s0] [sn], we call [sn] the leaf-node, and [si] (0 i < n) an inner-node w.r.t. this execution. If it is inﬁnite, then all [si] (i N) are inner-nodes. A possible execution of σ is complete if it is inﬁnite or its leaf-node is not in dom(σ).

Given δ = [s0] [sn] and µ = [t0] [tm], we use δ µ to denote that µ extends δ, i.e., n m and [si] = [ti] for all 0 i n. If δ µ, we deﬁne δ µ = µ. We use CELeaf(σ, s) to denote the set of all leaf-nodes of all the σ s complete executions (can be many due to non-determinism) starting from [s], and CEInner(σ, s) to denote the set of all the inner-nodes of σ s complete executions starting from [s]. CELeaf(σ, s) CEInner(σ, s) = since if [s] is a leaf-node of a complete execution then σ is not deﬁned at [s].

Deﬁnition 2.5 (Semantics). Given a pointed model M, s, the satisfaction relation is deﬁned as follows: M, s p p V(s) M, s ϕ M, s ϕ M, s ϕ ψ M, s ϕ and M, s ψ M, s Kϕ for all s : s s implies M, s ϕ M, s Khϕ there exists a strategy σ such that 1.[t] JϕK for all [t] CELeaf(σ, s) 2. all its complete executions starting from [s] are ﬁnite, where JϕK = {s W | M, s ϕ}.

Note that the two conditions for σ in the semantics of Kh reﬂect our two intuitions mentioned in the introduction. The implicit role of K in Kh will become clearer when the axioms are presented. Going back to Example 1.1, we can verify that Kh p holds on s1 and s2 due to the strategy σ = {{s1, s2} 7 test, {s3} 7 pills, {s4} 7 surgery}. Note that CELeaf(σ, s1) = {[s5], [s6]} = {{s5}, {s6}} and J p K = {s5, s6}. On the other hand, Kh q is not true on s1: although the agent can guarantee q de facto on s1 by taking a strategy such that {s1, s2} 7 test and {s3} 7 pills, he cannot know it beforehand since nothing works at s2 to make sure q. Readers may also verify that Kh(p q) holds at s1 and s2 (hint: a strategy is a partial function). Let us compare our work to [Wang, 2015; 2016b], where the knowing that operator is not in the language. We include the knowledge operator K to precisely capture the interactions of knowing that and knowing how by the axioms to be introduced in the next section. Although the universal modality deﬁnable in the previous work can be viewed as a restricted kind of knowing that operator, it can only express global background knowledge to some extent. Moreover, in our models, both epistemic uncertainty and action transitions are present to model the changes of knowledge after actions, which is essential to facilitate strategies based on local knowledge, compared to the quite restricted linear plans of [Wang, 2015; 2016b]. Finally, the Kh(ψ, ϕ) operator there ( the agent knows how to achieve ϕ given ψ ) is state-independent. In the present perspective, the condition ψ there exactly deﬁnes an initial uncertainty set.

3 Axiomatization 3.1 The Proof System SKH Axioms TAUT all axioms of propositional logic DISTK Kp K(p q) Kq T Kp p 4 Kp KKp 5 Kp K Kp Ax Kto Kh Kp Khp Ax Khto Kh K Khp Kh Kp Ax Khto KKh Khp KKhp Ax Kh Kh Kh Khp Khp Ax Khbot Kh Rules

ψ NECK ϕ Kϕ

MONOKh ϕ ψ Khϕ Khψ SUB ϕ(p) ϕ[ψ/p]

Note that we have the S5 axioms for K. Ax Kto Kh says if p is known then you know how to achieve p by doing nothing (we allow the empty strategy). Ax Khto Kh K reﬂects the ﬁrst condition in the semantics that the goal is known after the executions. We will come back to this axiom at the end of the paper. Note that the termination condition is not fully expressible in our language, but Ax Khbot captures part of it by ruling out strategies that have no terminating executions at all. Ax Kh Kh essentially says that strategies can be composed. Its validity proof is quite involved and we devote the next subsection to it. Finally, Ax Khto KKh is the positive introspection axiom for Kh; it is valid due to uniformity of strategies. The corresponding negative introspection can be derived from axioms Ax Khto KKh, 5 and T: Proposition 3.1. Khp K Khp. It is also not hard to show that in SKH, Khp is provably equivalent to KKhp, Kh Kp, and Kh Khp. Note that we do not have the K axiom for Kh. Instead, we have the monotonicity rule MONOKh. In fact, the logic is not normal, as desired, e.g., Khp Khq Kh(p q) is not valid: the existence of two different strategies for different goals does not imply the existence of a uniﬁed strategy to realize both goals.

3.2 Validity of Ax Kh Kh Ax Kh Kh is about the sequential compositionality of strategies. Suppose on some pointed model there is a strategy σ to guarantee that we end up with the states where on each s of them we have some other strategy σs to make sure p (Kh Khp). Since the strategies are uniform, we only need to consider some σ[s] for each [s]. Now to validate Ax Kh Kh, we need to design a uniﬁed strategy to compose σ and those σ[s] into one strategy to still guarantee p (Khp). The general idea is actually simple: ﬁrst, order those leaf nodes [s] (using Axiom of Choice); then by transﬁnite induction adjust σ[s] one by one to make sure these strategies can ﬁt together as a uniﬁed strategy θ; ﬁnally, merge the relevant part of σ with θ into the desired strategy. We make this idea precise below. First we need an observation:

Proceedings of the Twenty-Sixth International Joint Conference on Artiﬁcial Intelligence (IJCAI-17)

Proposition 3.2. Given strategies τ and σ with τ σ, if [s] dom(τ) and dom(σ) CELeaf(τ, s) = , then a sequence is σ s complete execution from [s] if and only if it is τ s complete execution from [s].

Proof. Left to Right: Let [s0] [sn] be a σ s complete execution from [s] (it also means that [s] = [s0], similarly in later proofs). We will show it is also a τ s complete execution from [s]. Firstly, we show it is a possible execution give τ from [s]. If it is not, there exists [si] such that [si] is not the leaf-node of this execution and such that [si] dom(τ). Let [sj] be the minimal equivalence class in the sequence with such properties. It follows that [sj] CELeaf(τ, s) and [sj] dom(σ). These are contradictory with dom(σ) CELeaf(τ, s) = . Next we will show that [s0] [sn] is a τ s complete execution from [s]. It is obvious if the sequence is inﬁnite. If it is ﬁnite, let the leaf-node be [sm]. It follows that [sm] dom(σ). Since τ σ, it follows [sm] dom(τ). Therefore, the execution is complete given τ. Right to Left: Let [s0] [sn] be a τ s complete execution from [s], we will show it is also a σ s complete execution from [s]. Since τ σ, it is also a possible execution given σ. If the execution is inﬁnite, it is obvious. If it is ﬁnite, let the leaf-node be [sm]. It follows that [sm] CELeaf(τ, s). Since dom(σ) CELeaf(τ, s) = , it follows that [sm] dom(σ). Therefore, the execution is also complete give σ.

Proposition 3.3. Kh Khϕ Khϕ.

Proof. Supposing M, s Kh Khϕ, we will show that M, s Khϕ. It follows by the semantics that there exists a strategy σ such that all σ s complete executions from [s] are ﬁnite and [t] JKhϕK for all [t] CELeaf(σ, s) ( ). If [s] dom(σ), then CELeaf(σ, s) = {[s]}, and then it is trivial that M, s Khϕ. Next we focus on the case of [s] dom(σ). According to the well-ordering theorem (equivalent to Axiom of Choice), we assume CELeaf(σ, s) = {Si | i < γ} where γ is an ordinal number and γ 1. Let si be an element in Si, then [si] = Si. Since M, si Khϕ for each i < γ, it follows that for each [si] there exists a strategy σi such that all σi s complete executions from [si] are ﬁnite and [v] JϕK for all [v] CELeaf(σi, si) ( ). Next, in order to show M, s Khϕ, we need to deﬁne a strategy τ. The deﬁnition consists of the following steps.

Step I. By induction on i, we will deﬁne a set of strategies τi where 0 i < γ. Let fi = S β<i τβ and Di = CEInner(σi, si) \ (dom(fi) {[v] CELeaf(fi, t) | [t] dom(fi)}); we deﬁne:

τ0 = σ0|CEInner(σ0,s0);

τi = fi (σi|Di) for i > 0.

Claim 3.3.1. We have the following results:

1. For each 0 i < γ, τj τi if j < i;

2. For each 0 i < γ, τi is a partial function;

3. For each 0 i < γ, dom(τi) CELeaf(τj, t) = where t dom(τj) if j < i;

4. For each 0 i < γ, if δ = [t0][t1] is a τi s complete execution from [t] dom(τi) then |δ| = n for some n N and [tn] JϕK;

5. For each 0 i < γ, [si] dom(τi) or [si] JϕK.

Proof of Claim 3.3.1:

1. It is obvious.

2. We prove it by induction on i. For the case of i = 0, it is obvious. For the case of i = α > 0, it follows by the IH that τβ is a partial function for each β < α. Furthermore, it follows by (1) that τβ1 τβ2 for all β1 < β2 < α. Thus, we have fα = S β<α τβ is a partial function. Since σα is a partial function, in order to show τα is a partial function, we only need to show that dom(fα) Dα = . Since Dα = CEInner(σα, sα)\ dom(fα) \ {[v] CELeaf(fα, t) | t dom(fα)}, it is obvious that dom(fα) Dα = .

3. We prove it by induction on i. It is obvious for the case of i = 0. For the case of i = α > 0, given j < α and t dom(τj), we need to show that dom(τα) CELeaf(τj, t) = . Supposing [v] CELeaf(τj, t), we will show that [v] dom(τα), namely [v] dom(fα) Dα. Since j < α and fα = S β<α τα, it follows t dom(fα). Moreover, due to Dα = CEInner(σα, sα) \ (dom(fα) {[v] CELeaf(fα, t) | t dom(fα)}), it follows [v] Dα. Next, we only need to show [v] dom(fα). Assuming [v] dom(fα), it follows that [v] dom(τβ) for some β < α. There are two cases: j < β or j β. If j < β, it follows by the IH that dom(τβ) CELeaf(τj, t) = . Contradiction. If j β, it follows by (1) that τβ τj. Due to [v] dom(τβ), it follows [v] dom(τj). It is contradictory with [v] CELeaf(τj, t). Thus, we have [v] dom(fα).

4. We prove it by induction on i. For the case of i = 0, due to dom(τ0) = CEInner(σ0, s0), it follows that there is a σ0 s possible execution [s0] [sm] such that m N and [sm] = [t]. Let µ = [s0] [sm 1] δ. (If m = 0 then µ = δ). Since δ is a τ0 s complete execution from [t], it follows that µ is a σ0 s complete execution from [s0]. It follows by ( ) that µ is ﬁnite. Thus, δ = [t0] [tn] for some n N. Since [tn] CELeaf(σ0, s0), it follows by ( ) that [tn] JϕK. For the case of i = α > 0, there are two situations: [t] dom(fα) or [t] Dα. If [t] dom(fα), it follows that [t] dom(τβ) for some β < α. By (3), we have dom(τα) CELeaf(τβ, t) = . Since δ is a τα s complete execution, it follows by Proposition 3.2 that δ is also a τβ s complete execution from [t]. It follows by the IH that |δ| = n for some n N and [tn] JϕK. If [t] Dα, there are two cases: there exist k < |δ| and β < α s.t. [tk] dom(τβ), or there do not exist such k and β. (Please note that |δ| > 1 due to the fact that δ = [t0] is τα s complete execution from [t] dom(τα)).

[tk] dom(τβ) for some k < |δ| and some β < α: It follows that µ = [tk] is a τα s complete

Proceedings of the Twenty-Sixth International Joint Conference on Artiﬁcial Intelligence (IJCAI-17)

execution from [tk]. By (3) and Proposition 3.2, µ is a τβ s complete execution from [tk]. By IH, µ = [tk] [tk+n] for some n N and [tk+n] JϕK. Therefore, |δ| = k + n. If there does not exist k < |δ| and β < α s.t. [tk] dom(τβ), it follows that δ = [t0] is a σα s possible execution from [t]. Since [t] Dα CEInner(σα, sα), there is a σα s possible execution [s0] [sm] s.t. m N, [s0] = [sα] and [sm] = [t]. Let µ = [s0] [sm 1] δ. (If m = 0 then µ = δ). It follows that µ is σα s possible execution from sα. By ( ), all σα s complete executions from sα are ﬁnite. Thus, µ is ﬁnite. Therefore, δ = [t0] [tn] for some n N. We continue to show that [tn] JϕK. Since δ = [t0] [tn] is a τα s complete execution from [t] and it is also a σα s possible execution from t, there are two cases: [tn] CELeaf(fα, t ) for some t dom(fα), or δ is a σα s complete execution from t. If [tn] CELeaf(fα, t ) for some [t ] dom(fα), then there exists β < α s.t. [t] CELeaf(τβ, t ) and [t ] dom(β). By IH, [tn] JϕK. If δ is a σα s complete execution from [t], it follows that µ is a σα s complete execution from [sα]. Then by ( ), we have [tn] JϕK.

5. If [si] dom(σi), it follows by ( ) that [si] JϕK. Otherwise, there are two cases: i = 0 or i = α > 0. If i = 0, it follows by [s0] dom(σ0) that [s0] CEInner(σ0, s0). Thus, [s0] dom(τ0). If i = α > 0 and [sα] dom(σα), we will show that if [sα] dom(τα) then [sα] JϕK. Firstly, we have that [si] CEInner(σα, sα). Since [sα] dom(τα), it follows that [sα] CELeaf(fα, t) for some [t] dom(fα). It follows that there exists β < α such that [sα] CELeaf(τβ, t) and t dom(τβ). It follows by (4) that [si] JϕK.

Step II. We deﬁne τγ = S i<γ τi. It follows by (1) and (2) of Claim 3.3.1 that τγ is indeed a partial function. Then we prove the following claim.

Claim 3.3.2. If δ = [t0] is a τγ s complete execution from [t] dom(τγ) then |δ| = n for some n N and [tn] JϕK.

Proof of Claim 3.3.2: Since [t] dom(τγ), it follows that [t] dom(τi) for some i < γ. It follows by (5) of Claim 3.3.1 that all τi s complete executions from [t] are ﬁnite. Thus, there exists µ δ such that |µ| = n for some n N and µ is τi s complete execution from [t]. It follows by (5) of Claim 3.3.1 that [tn] JϕK. Next, we only need to show δ = µ. If not, then δ = [t0] [tn][tn+1] . We then have that there exists j < γ such that {tk | 0 k n} dom(τj). It cannot be that j i. Otherwise, µ is not τi s complete execution since τj τi by (1) of Claim 3.3.1. Thus, we have j > i. Since we also have that [tn] dom(τj), [tn] CELeaf(τi, t) and t dom(τi), this is in contradiction with (3) of Claim 3.3.1. Therefore, we have δ = µ.

Step III. We deﬁne τ as τ = τγ (σ|C) where C = CEInner(σ, s) \ (dom(τγ) {[v] CELeaf(τ , t) | [t] dom(τγ)}) and σ is the strategy mentioned at ( ). Since both τγ and σ|C are partial functions, τ is also a partial function. We then prove the following claim.

Claim 3.3.3. If δ = [t0] is a τ s complete execution from [t] dom(τ) then |δ| = n for some n N and [tn] JϕK.

Proof of Claim 3.3.3: Since dom(τ) = dom(τγ) C, there are two cases: [t] dom(τγ) or [t] C. If [t] dom(τγ), it follows that CELeaf(τγ, t) C = . Moreover, we have CELeaf(τγ, t) dom(τγ) = . Thus, we have CELeaf(τγ, t) dom(τ) = . It follows by Proposition 3.2 that δ is a τγ s complete execution from from [t]. It follows by Claim 3.3.2 |δ| = n for some n N and [tn] JϕK. If [t] C, there are two cases: there exists k < |δ| such that [tk] dom(τγ), or there does not exists such k. (Please note that |δ| > 1 due to the fact that δ = [t0] is τ s complete execution from [t] dom(τ)).

[tk] dom(τγ) for some k < |δ|: It follows that µ = [tk] is a τ s complete execution from [tk]. Since dom(τ) CELeaf(τγ, tk) = , it follows by Proposition 3.2 that µ is a τγ s complete execution from [tk]. It follows by Claim 3.3.2 that µ = [tk] [tk+n] for some n N and [tk+n] JϕK. Therefore, |δ| = k + n.

If there does not exist k < |δ| s.t. [tk] dom(τγ), then δ = [t0] is a σ s possible execution from [t]. Since [t] C CEInner(σ, s), then there is a σ s possible execution [s0] [sm] s.t. m N, [s0] = [s] and [sm] = [t]. Let µ = [s0] [sm 1] δ. (If m = 0 then µ = δ). It follows that µ is σ s possible execution from s. By ( ), all σ s complete executions from s are ﬁnite. Thus, µ is ﬁnite. Therefore, δ = [t0] [tn] for some n N. We continue to show that [tn] JϕK. Since δ = [t0] [tn] is a τ s complete execution from t and it is also a σ s possible execution from t, there are two cases: [tn] CELeaf(τγ, t ) for some t dom(τγ), or δ is a σ s complete execution from t. If [tn] CELeaf(τγ, t ) for some [t ] dom(τγ), it follows by Claim 3.3.2 that [tn] JϕK. If δ is a σ s complete execution from [t], it follows that µ is a σ s complete execution from [s]. It follows that [tn] = Si for some 0 i < γ. Since δ = [t0] [tn] is τ s complete execution from [t] dom(τγ), it follows [tn] dom(τγ). We then have [tn] dom(τi), namely Si τi. It follows by (5) of Claim 3.3.1 that Si JϕK, namely [tn] JϕK.

Next, we continue to show that M, s Khϕ with the assumption that [s] dom(σ). Since [s] dom(σ), we have [s] CEInner(σ, s). There are two cases: [s] dom(τ) or not. If [s] dom(τ), it follows by Claim 3.3.3 that M, s Khϕ. If [s] dom(τ), due to [s] CEInner(σ, s), it follows that [s] CELeaf(τγ, t) for some [t] dom(τγ). It follows by Claim 3.3.2 that [s] JϕK. It follows that M, s Kϕ. It is obvious that M, s Khϕ.

The validity of the rest of the axioms can be checked (cf. the explanation right after the system SKH), then we have:

Proceedings of the Twenty-Sixth International Joint Conference on Artiﬁcial Intelligence (IJCAI-17)

Theorem 3.4 (Soundness). If ϕ then ϕ.

4 Completeness and Decidability Let Φ be a subformula-closed set of formulas. It is obvious that Φ is countable since the whole language itself is countable. Given a set of formulas , let: |K = {Kϕ | Kϕ }, | K = { Kϕ | Kϕ }, |Kh = {Khϕ | Khϕ }, | Kh = { Khϕ | Khϕ }. Below we deﬁne the closure of Φ, and use it to build a canonical model w.r.t. Φ. We will show that when Φ is ﬁnite then we can build a ﬁnite model. Deﬁnition 4.1. The closure cl(Φ) is Φ {Kϕ | ϕ Φ}. Deﬁnition 4.2 (Atom). We enumerate the formulas in cl(Φ) by {ψi | i N}. The formula set = {Yi | i N} is an atom of cl(Φ) if Yi = ψi or Yi = ψi for each ψi cl(Φ); is consistent. Note that if Φ is the whole language then an atom is simply a maximal consistent set. By a standard inductive construction, we can obtain the Lindenbaum-like result in our setting (which is useful to show the existence lemma for K): Proposition 4.3. Let be an atom of cl(Φ), Γ and ϕ cl(Φ). If Γ { ϕ} is consistent then there is an atom of cl(Φ) such that (Γ { ϕ}) , where ϕ = ϕ or ϕ = ϕ. Deﬁnition 4.4. Given a subformula-closed Φ, the canonical model MΦ = W, ACT, , { x | x ACT}, V is deﬁned as: W = { | is an atom of cl(Φ)}; ACT = {ϕ | Khϕ Φ}; iff |K = |K;

for each ϕ ACT, ϕ iff Khϕ, Kϕ and Kϕ ; for each p Φ, p V ( ) iff p . Note that we use the ϕ in Khϕ formulas as the action labels, and we introduce an action transition if it is necessary, i.e., Khϕ but Kϕ (i.e., empty strategy does not work). Requiring Kϕ is to reﬂect the ﬁrst condition in the semantics of Kh. Using NECK, DISTK and Proposition 4.3, it is routine to show the existence lemma for K: Proposition 4.5. Let be a state in MΦ, and Kϕ cl(Φ). If Kϕ then there exists [ ] such that ϕ .

Proof. Let Γ = |K | K { ϕ}. Γ is consistent. If not, there are Kϕi, , Kϕn and Kψ1, , Kψm in :

Kϕ1 Kϕn Kψ1 Kψm ϕ.

Following by NECK and DISTK, we have

K(Kϕi Kϕn Kψ1 Kψm) Kϕ.

Since the epistemic operator K is distributive over and KKϕi Kϕi for all 1 i n and K Kψi Kψi for all 1 i m, we have

Kϕi Kϕn Kψ1 Kψm Kϕ.

Since Kϕi, , Kϕn and Kψ1, , Kψm are all in and Kϕ cl(Φ), it follows that Kϕ . It is contradictory with the assumption that Kϕ . Therefore, Γ is consistent. It follows by Proposition 4.3 that there exists an atom of cl(Φ) such that Γ . Since ( |K | K) , we have , that is, [ ].

Proposition 4.6. Let and be two states in MΦ such that . We have |Kh = |Kh.

Proof. For each Khϕ , by Deﬁnition 4.1, Khϕ Φ. Then KKhϕ cl(Φ). For each Khϕ , by Axiom Ax Khto KKh, we have KKhϕ . Since , then KKhϕ , and by Axiom T, Khϕ . Then we showed that Khϕ implies Khϕ . Similarly we can prove Khϕ implies Khϕ . Hence, |Kh = |Kh.

The following is a crucial observation for the later proofs.

Proposition 4.7. Let be a state in MΦ and ψ ACT be

executable at [ ]. If Khϕ for all with [ ] ψ [ ] then Khϕ .

Proof. First, we show that Kψ is not consistent with Khϕ. It is obvious that Khϕ cl(Φ). Since ψ is executable at [ ],

there are atoms Γ1 and Γ2 s.t. Γ1 ψ Γ2. Then Kψ Γ2. Assuming that Kψ is consistent with Khϕ, by Proposition 4.3 there exists an atom Γ of cl(Φ) s.t. {Kψ, Khϕ} Γ. Since ψ ACT is executable at [ ], then by deﬁnition of ψ , and Proposition 4.6, Khψ, Kψ . It follows that

ψ Γ, then [ ] ψ [Γ]. This is in contradiction with the

assumption that Khϕ for all with [ ] ψ [ ]. Then Kψ is not consistent with Khϕ. Hence, Kψ Khϕ. Since Kψ Khϕ, it follows by Rule MONOKh and Axiom Ax Khto Kh K that Khψ Kh Khϕ. Moreover, it follows by Axiom Ax Kh Kh that Khψ Khϕ. Since ψ is ex-

ecutable at [ ], it follows by the deﬁnition of ψ and Proposition 4.6 that Khψ . Therefore, we have Khϕ .

Lemma 4.8. For each ϕ cl(Φ), MΦ, ϕ iff ϕ .

Proof. We prove it by induction on ϕ. We only focus on the case of Khϕ cl(Φ); the other cases are straightforward, e.g., Kϕ case can be proved based on Proposition 4.5. Note that if Khϕ cl(Φ) then Khϕ Φ, therefore ϕ Φ since Φ is subformula-closed. Thus by Deﬁnition 4.1, Kϕ cl(Φ). Right to Left: If Khϕ , we will show MΦ, Khϕ. Firstly, there are two cases: Kϕ or Kϕ . If Kϕ , then Kϕ, ϕ for all [ ]. Since ϕ Φ, it follows by IH that MΦ, ϕ for all [ ]. Therefore, MΦ, Kϕ. It follows by Axiom Ax Kto Kh and the soundness of SKH that MΦ, Khϕ. If Kϕ , we ﬁrst show that Kϕ is consistent. If not, namely Kϕ , it follows by Rule MONOKh that Kh Kϕ Kh . It follows by Axiom Ax Khbot that Kh Kϕ . Since Khϕ , it follows by Axiom Ax Khto Kh K that , which is in contradiction with the fact that is consistent. Therefore, Kϕ is consistent.

Proceedings of the Twenty-Sixth International Joint Conference on Artiﬁcial Intelligence (IJCAI-17)

By Proposition 4.3 there exists an atom s.t. Kϕ . Note that ϕ ACT. Thus, we have ϕ , then [ ] ϕ [ ]. Let [ ] be an equivalence class s.t. [ ] ϕ [ ], which indicates Γ ϕ Γ for some Γ [ ] and Γ [ ]. By deﬁnition of ϕ and we get Kϕ Θ for all Θ [ ]. By IH, MΦ, Θ ϕ for all Θ [ ], namely [ ] JϕK. Moreover, ϕ is not a loop on [ ] because Kϕ . Thus, the partial function σ = {[ ] 7 ϕ} is a strategy s.t. all its complete executions starting from [ ] are ﬁnite and [ ] JϕK for each [ ] CELeaf(σ, ). Then, MΦ, Khϕ. Left to Right: Suppose MΦ, Khϕ, we will show Khϕ . By the semantics, there exists a strategy σ s.t. all σ s complete executions starting from [ ] are ﬁnite and [Γ] JϕK for all [Γ] CELeaf(σ, ). By IH, ϕ Γ for all Γ [Γ] and [Γ] CELeaf(σ, ). By Proposition 4.5, we get Kϕ Γ for all [Γ] CELeaf(σ, ). By Axiom Ax Kto Kh and Proposition 4.6, Khϕ Γ for all [Γ] CELeaf(σ, ). If [ ] dom(σ), it is obvious that Khϕ because [ ] CELeaf(σ, ). Next, we consider the case of [ ] dom(σ), then [ ] CEInner(σ, ). In order to show Khϕ , we will show a stronger result that Khϕ for all [ ] CEInner(σ, ). Firstly, we show the following claim:

Claim 4.8.1. If there exists [ ] CEInner(σ, ) such that Khϕ then there exists an inﬁnite execution of σ starting from [ ]. Proof of Claim 4.8.1: Let X be the set {[Θ] CEInner(σ, ) | Khϕ Θ}. It follows that [ ] X and X dom(σ). We deﬁne a binary relation R on X as

R = {([Θ], [Θ ]) | [Θ] σ([Θ]) [Θ ]}. For each [Θ] X, we have that σ([Θ]) is executable at [Θ]. Since Khϕ Θ, by Proposition 4.7 there exists an atom Θ

s.t. [Θ] σ([Θ]) [Θ ] and Khϕ Θ . Since Khϕ Γ for all [Γ] CELeaf(σ, ) and [Θ] CEInner(σ, ),we have [Θ ] CEInner(σ, ). Then [Θ ] X. Therefore, R is an entire binary relation on X, namely for each [Θ] X there is [Θ ] X such that ([Θ], [Θ ]) R. Then by Axiom of Dependent Choice there exists an inﬁnite sequence [Θ0][Θ1] s.t. ([Θn], [Θn+1]) R for all n N. From the deﬁnition of R, [Θ0][Θ1] is a complete execution of σ starting from [Θ0]. Since [Θ0] CEInner(σ, ) and all complete execution of σ from [ ] are ﬁnite, there is a possible execution [ 0] [ j] for some j N s.t. [ 0] = [ ] and [ j] = [Θ0]. Therefore, [ 0] [ j][Θ1] is an inﬁnite complete execution of σ from [ ]. Therefore, we have Khϕ for all [ ] CEInner(σ, s). Otherwise, by Claim 4.8.1 there is an inﬁnite complete execution given σ from [ ]. This is contradictory with all σ s complete execution from [ ] are ﬁnite, then Khϕ for all [ ] CEInner(σ, s). Since [ ] dom(σ), we get [ ] CEInner(σ, ). Then Khϕ .

Now let Φ be the set of all formulas, then each maximal consistent set is actually an atom which satisﬁes all its formulas in MΦ, according to the above truth lemma. Completeness then follows immediately.

Theorem 4.9. SKH is strongly complete.

Note that if Φ is the set of all subformulas of a given formula ϕ, then cl(Φ) is still ﬁnite. Due to the soundness of SKH and Proposition 4.3, a satisﬁable formula ϕ must be consistent thus appearing in some atom, and thus ϕ is satisﬁable in MΦ. It is not hard to see that |MΦ| 22|ϕ| where 2|ϕ| is the bound on the size of cl(Φ). This gives us a small model property of our logic, then decidability follows.

Theorem 4.10. SKH is decidable.

5 Conclusion

In this paper, we propose an epistemic logic of both (goaldirected) knowing how and knowing that, and capture their interactions. A sound and complete proof system SKH is obtained, and we prove the decidability of the logic. We hope the axioms are illuminating towards a better understanding of knowing how. Note that we do not impose any special properties between the interaction of a and in the models so far. In the future, it would be interesting to see whether assuming properties of perfect recall and/or no learning (cf. e.g., [Fagin et al., 1995; Wang and Li, 2012]) changes the logic or not. Our notion of knowing how is relatively strong, particularly evidenced by the axiom Ax Khto Kh K : Khϕ Kh Kϕ, which is due to the ﬁrst condition of our semantics for Kh, inspired by planning with uncertainty. We believe it is reasonable for the scenarios where the agent has perfect recall (or, say, never forgets), which is usually assumed implicitly in the discussions on planning (cf. [Li et al., 2017]). However, for a forgetful agent it may not be intuitive anymore, e.g., I know how to get drunk when sober but I may not know how to get to the state that I know I am drunk, assuming drunk people do not know they are drunk. The axiom Ax Kh Kh is also interesting in distinguishing different types of knowing how. We have been focusing on the goaldirected knowing how [Gochet, 2013], but for other types of knowing how such as knowing how to swim, the axiom may not be reasonable anymore, e.g., I know how to let myself to know how to swim (by registering an excellent swimming course) does not mean that I know how to swim right now. We leave the discussion of other types of knowing how in the future. Moreover, by introducing suitable notions of bisimulations we will be able to compare their expressive power. Another obvious next step is to consider knowing how in multi-agent settings, which brings us closer to coalition logics (cf. e.g., [ Agotnes and Alechina, 2012; Naumov and Tao, 2017].

Acknowledgements

Raul Fervari has received funding from the European Union s Horizon 2020 research and innovation programme under the Marie Skodowska-Curie grant agreement No. 690974 for the project MIREL: MIning and REasoning with Legal texts, Se Cy T-UNC and ANPCy T-PICT-2013-2011. Yanjun Li thanks the support from China Scholarship Council (CSC). Yanjing Wang acknowledges the support from the National Program for Special Support of Eminent Professionals, and the NSSF key project 12&ZD119.

Proceedings of the Twenty-Sixth International Joint Conference on Artiﬁcial Intelligence (IJCAI-17)

References [ Agotnes and Alechina, 2012] Thomas Agotnes and Natasha Alechina. Epistemic coalition logic: completeness and complexity. In Proceedings of AAMAS 2012, pages 1099 1106, 2012. [ Agotnes et al., 2015] Thomas Agotnes, Valentin Goranko, Wojciech Jamroga, and Michael Wooldridge. Knowledge and ability. In Hans van Ditmarsch, Joseph Halpern, Wiebe van der Hoek, and Barteld Kooi, editors, Handbook of Epistemic Logic, chapter 11, pages 543 589. College Publications, 2015. [Belardinelli, 2014] Francesco Belardinelli. Reasoning about knowledge and strategies: Epistemic strategy logic. In Proceedings of SR 2014, pages 27 33, 2014. [Broersen and Herzig, 2015] Jan Broersen and Andreas Herzig. Using STIT theory to talk about strategies. In Johan van Benthem, Sujata Ghosh, and Rineke Verbrugge, editors, Models of Strategic Reasoning: Logics, Games, and Communities, pages 137 173. Springer, 2015. [Fagin et al., 1995] R. Fagin, J. Halpern, Y. Moses, and M. Vardi. Reasoning about knowledge. MIT Press, 1995. [Fantl, 2008] Jeremy Fantl. Knowing-how and knowingthat. Philosophy Compass, 3(3):451 470, 2008. [Geffner and Bonet, 2013] Hector Geffner and Blai Bonet. A concise introduction to models and methods for automated planning. Synthesis Lectures on Artiﬁcial Intelligence and Machine Learning, 8(1):1 141, 2013. [Gochet, 2013] Paul Gochet. An open problem in the logic of knowing how. In J. Hintikka, editor, Open Problems in Epistemology. The Philosophical Society of Finland, 2013. [Herzig et al., 2013] Andreas Herzig, Emiliano Lorini, and Dirk Walther. Reasoning about actions meets strategic logics. In Proceedings of LORI 2013, pages 162 175, 2013. [Herzig, 2015] Andreas Herzig. Logics of knowledge and action: critical analysis and challenges. Autonomous Agents and Multi-Agent Systems, 29(5):719 753, 2015. [Hintikka, 1962] J. Hintikka. Knowledge and Belief: An Introduction to the Logic of the Two Notions. Cornell University Press, Ithaca N.Y., 1962. [Jamroga and Agotnes, 2007] Wojciech Jamroga and Thomas Agotnes. Constructive knowledge: what agents can achieve under imperfect information. Journal of Applied Non-Classical Logics, 17(4):423 475, 2007. [Lesp erance et al., 2000] Yves Lesp erance, Hector J. Levesque, Fangzhen Lin, and Richard B. Scherl. Ability and knowing how in the situation calculus. Studia Logica, 66(1):165 186, 2000. [Li and Wang, 2017] Yanjun Li and Yanjing Wang. Achieving while maintaining: A logic of knowing how with intermediate constraints. In Proceedings of ICLA 17, pages 154 167, 2017. [Li et al., 2017] Yanjun Li, Quan Yu, and Yanjing Wang. More for free: a dynamic epistemic framework for conformant planning over transition systems. Journal of Logic and Computation, 2017. forthcoming.

[Li, 2017] Yanjun Li. Stopping means achieving: A weaker logic of knowing how. Studies in Logic, 9(4):34 54, 2017. [Mc Carthy and Hayes, 1969] John Mc Carthy and Patrick J. Hayes. Some philosophical problems from the standpoint of artiﬁcial intelligence. In Machine Intelligence, pages 463 502. Edinburgh University Press, 1969. [Mc Carthy, 1979] John Mc Carthy. First-Order theories of individual concepts and propositions. Machine Intelligence, 9.:129 147, 1979. [Moore, 1985] Robert C Moore. A formal theory of knowledge and action. In Jerry R. Hobbs and Robert C. Moore, editors, Formal Theories of the Commonsense World. Ablex Publishing Corporation, 1985. [Naumov and Tao, 2017] Pavel Naumov and Jia Tao. Coalition power in epistemic transition systems. In Proceedings of AAMAS 2017, pages 723 731, 2017. [Smith and Weld, 1998] David E. Smith and Daniel S. Weld. Conformant graphplan. In AAAI 98, pages 889 896, 1998. [Stanley and Williamson, 2001] Jason Stanley and Timothy Williamson. Knowing how. The Journal of Philosophy, pages 411 444, 2001. [van der Hoek and Wooldridge, 2003] Wiebe van der Hoek and Machael Wooldridge. Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications. Studia Logica, (1):125 157, 2003. [van der Hoek et al., 2000] Wiebe van der Hoek, Bernd van Linder, and John-Jules Ch. Meyer. On agents that have the ability to choose. Studia Logica, 66(1):79 119, 2000. [Wang and Li, 2012] Yanjing Wang and Yanjun Li. Not all those who wander are lost: Dynamic epistemic reasoning in navigation. In Proceedings of Ai ML 2012, pages 559 580, 2012. [Wang, 2015] Yanjing Wang. A logic of knowing how. In Proceedings of LORI 2015, pages 392 405, 2015. [Wang, 2016a] Yanjing Wang. Beyond knowing that: a new generation of epistemic logics. In Hans van Ditmarsch and Gabriel Sandu, editors, Jaakko Hintikka on knowledge and game theoretical semantics. Springer, 2016. forthcoming. [Wang, 2016b] Yanjing Wang. A logic of goal-directed knowing how. Synthese, pages 1 21, 2016. in press. [Yu et al., 2016] Quan Yu, Yanjun Li, and Yanjing Wang. A dynamic epistemic framework for conformant planning. In Proceedings of TARK 15, pages 298 318. EPTCS, 2016.

Proceedings of the Twenty-Sixth International Joint Conference on Artiﬁcial Intelligence (IJCAI-17)