# Tableaux for the Logic of Strategically Knowing How

Yanjun Li College of Philosophy, Nankai University, Tianjin, China

###### Abstract

The logic of goal-directed _knowing how_ proposed in [6] extends the standard
epistemic logic with an operator of _knowing how_. The _knowing how_ operator
is interpreted as that there exists a strategy such that the agent knows that
the strategy can make sure that $\varphi$. This paper presents a tableau
procedure for the multi-agent version of the logic of strategically _knowing
how_ and shows the soundness and completeness of this tableau procedure. This
paper also shows that the satisfiability problem of the logic can be decided
in PSPACE.

##  1 Introduction

Epistemic logic proposed by von Wright and Hintikka (see [25, 12]) is a
logical formalism for reasoning about knowledge of agents. It deals with
propositional knowledge, that is, the knowledge expressed as knowing that
$\varphi$ is true. In recent years, other patterns of knowledge besides
knowing that are attracting increasing attention in logic community, such as
knowing whether [9, 5], knowing who [4], knowing the value [3, 7], and knowing
why [29] (see a survey in [28]). Motivated by different scenarios in
philosophy and AI, reasoning about knowing how assertions are particularly
interesting [24].

The discussion about formalizing the notion of _knowing how_ can date back to
[17, 18]. Currently, there are two main approaches of formalizing _knowing
how_. One of them is connecting _knowing how_ with logics of _knowing that_
and _ability_ (see e.g. [14, 11]). However, the main difficulty of this
approach is that a simple combination of the modalities of knowing that and
ability does not seem to capture a natural understanding of _knowing how_ (see
a discussion in [13, 10]). Instead of expressing _knowing how_ by _knowing
that_ and _ability_ modalities, the other approach first adopted in [26] is
expressing _knowing how_ in modal languages with a new modality of _knowing
how_.

Inspired by the idea of automated planning under uncertainty in artificial
intelligence, The author of [26, 27] proposed a logical framework of _knowing
how_ which includes a binary modality of _knowing how_. In [2], a new
semantics for this _knowing how_ modality was given, which is based on an
indistinguishability relation between plans. It is shown in [2] that the
satisfiability problem of this _knowing how_ logic is NP-complete, but this
logic does not include the modality for _knowing that_.

Inspired by the tradition of coalition logic, the authors of [19, 22]
introduced a logic to capture _knowing how_ of coalitions. A coalition $C$
knows how to achieve $\varphi$ if and only if there is a joint action $a$ for
$C$ such that it is distributed knowledge for $C$ that doing $a$ can make sure
that $\varphi$. Variants of the basic framework were proposed and discussed.
In [21], a logic of _knowing how_ under the assumption of perfect recall was
studied. In [23], a logic of _knowing how_ with the degree of uncertainty was
discussed. In [20], a logic of second-order _knowing how_ was proposed, for
the case that one coalition knows what the joint action of another coalition
is. The topic of complexity is not covered in these literatures.

Along with the idea of formalizing _knowing how_ based on planning, the
authors of [6] proposed a single-agent logic of _knowing how_ via strategies.
A strategy is a partial function from the set of agents’ belief states into
the set of actions. The agent knows how to achieve $\varphi$ if and only if
there is a strategy such that all executions of the strategy will terminate on
$\varphi$-states. Besides strategies, there are other types of plans, such as
simple plans (i.e. a single action), linear plans (i.e. a sequence of
actions), and so on. The authors of [16] proposed a unified logical framework
to incorporate logics of _knowing how_ via different notions of plans. They
used a PDL-style programming language to syntactically specify various types
of plans and discussed ten types of _knowing how_ based on ten different
notions of plans. It is shown in [16] that the ten notions of plans lead to
the same _konwing how_ logic, but over finite models, the _konwing how_ logic
based on knowledge-based plans requires an extra axiom, which leads to the
same logic as the logic of strategically _knowing how_.

In [15], a tableau-based decision procedure was proposed for the logic of
_knowing how_ via simple plans. This paper develops the method and presents a
tableau procedure for the _knowing how_ logic via strategies proposed in [6].
Strategically _knowing how_ can not be handled by the original method, since
strategies are much more complicated than simple plans. This paper also shows
that the satisfiability problem of the logic of strategically _knowing how_ is
in PSPACE. With other known results, this leads to the result that the
satisfiability problem of the logic of strategically _knowing how_ is PSPACE-
complete.

The structure of this paper is as follows: Section 2 recalls the logic of
strategically _knowing how_ ; Section 3 presents a tableau procedure for the
logic and proves its soundness; Section 4 shows the completeness of the
tableau procedure and proves that the complexity of this logic is PSPACE-
complete. Section 5 concludes with some remarks.

##  2 The logic of strategically knowing how

This section presents the multi-agent version of the logic of strategically
_knowing how_ from [6].

Let $\mathbf{P}$ be a set of propositional letters and $\mathbf{I}$ be a set
of agents where $|\mathbf{I}|\geq 2$.

######  Definition 1 ($\textsf{ELKh}_{n}$ Language).

The Epistemic Language $\mathcal{L}_{\textsf{ELKh}_{n}}$ of _Knowing how_ is
defined by the following BNF where $p\in\mathbf{P}$ and $i\in\mathbf{I}$:

$\varphi::=\bot\mid
p\mid\neg\varphi\mid(\varphi\land\varphi)\mid{K}_{i}\varphi\mid{K}h_{i}{\varphi}.$

We use $\top,\lor,\to$ as usual abbreviations. The formula ${K}_{i}\varphi$
means that the agent $i$ knows that $\varphi$, and the formula
${K}h_{i}\varphi$ means that the agent knows how to achieve the goal that
$\varphi$.

######  Definition 2 ($\textsf{ELKh}_{n}$ Models).

A model ${M}$ is a quintuple $\langle W,\\{\sim_{i}\mid
i\in\mathbf{I}\\},\\{\mathbf{A}_{i}\mid i\in\mathbf{I}\\},\\{R_{a}\mid
a\in\mathbf{A}_{i},i\in\mathbf{I}\\},V\rangle$ where:

  * •

$W$ is a non-empty set of states,

  * •

$\sim_{i}\ \subseteq{W\times W}$ is an equivalence relation for each
$i\in\mathbf{I}$,

  * •

$\mathbf{A}_{i}$ is a set of actions for each $i\in\mathbf{I}$,

  * •

$R_{a}\subseteq{W\times W}$ is a binary relation for each $a\in\mathbf{A}$
where $\mathbf{A}=\bigcup_{i\in\mathbf{I}}\mathbf{A}_{i}$,

  * •

$V:W\to 2^{\mathbf{P}}$ is a valuation function.

Given $s\in W$, we use $[s]^{i}$ to denote the equivalence class of $s$ over
$\sim_{i}$, i.e., $[s]^{i}=\\{t\in W\mid s\sim_{i}t\\}$, and use $[W]^{i}$ to
denote the set of all equivalence classes of states in $W$ over $\sim_{i}$,
namely $[W]^{i}=\\{[s]^{i}\mid s\in W\\}$. We say that the action
$a\in\mathbf{A}_{i}$ is _executable_ at $s$ if $(s,t)\in R_{a}$ for some $t$.
We use $[s]^{i}\xrightarrow{a}[t]^{i}$ to denote that there are some
$s^{\prime}\in[s]^{i}$ and some $t^{\prime}\in[t]^{i}$ such that
$(s^{\prime},t^{\prime})\in R_{a}$.

######  Definition 3 (Strategies).

Given a model ${M}$, a _uniformly executable strategy_ (or simply called
_strategy_) for agent $i$ in ${M}$ is a partial function
$\sigma:[W]^{i}\to\mathbf{A}_{i}$ such that $\sigma([s]^{i})$ is executable at
all $s^{\prime}\in[s]^{i}$. Particularly, the empty function is also a
strategy, the _empty strategy_.

We use $\mathtt{dom}(\sigma)$ to denote the domain of $\sigma$.

######  Definition 4 (Executions).

Given a strategy $\sigma$ of agent $i$ in ${M}$, a _possible execution_ of
$\sigma$ is a possibly infinite sequence of equivalence classes
$\delta=[s_{0}]^{i}[s_{1}]^{i}\cdots$ such that
$[s_{k}]^{i}\xrightarrow{\sigma([s_{k}]^{i})}[s_{k+1}]^{i}$ for all $0\leq
k<|\delta|$. Particularly, $[s]^{i}$ is a possible execution if
$[s]^{i}\not\in\mathtt{dom}(\sigma)$. If the execution $\rho$ is a finite
sequence $[s_{0}]^{i}\cdots[s_{k}]^{i}$, we call $[s_{k}]^{i}$ the end node of
$\rho$. A possible execution of $\sigma$ is _complete_ if it is infinite or
its end node is not in $\mathtt{dom}(\sigma)$.

Given an $i$-strategy $\sigma$, we use $\mathtt{ECE}(\sigma,[s]^{i})$ to
denote the set of all end nodes of all $\sigma$’s complete executions starting
from $[s]^{i}$.

######  Definition 5 ($\textsf{ELKh}_{n}$ Semantics).

The satisfaction relation $\vDash$ between a pointed model (${M},s$) and a
formula $\varphi$ is defined as follows:

$\begin{array}[]{lll}{M},s\vDash p&\iff&s\in V(p)\\\
{M},s\vDash\neg\varphi&\iff&{M},s\nvDash\varphi\\\
{M},s\vDash\varphi\land\psi&\iff&{M},s\vDash\varphi\text{ and
}{M},s\vDash\psi\\\ {M},s\vDash{K}_{i}{\varphi}&\iff&\text{for all
}s^{\prime}:\text{ if }s{\sim_{i}}s^{\prime}\text{ then
}{M},s^{\prime}\vDash\varphi\\\ {M},s\vDash{K}h_{i}{\varphi}&\iff&\text{there
exists a strategy $\sigma$ for agent $i$ such that }\\\ &&1.\text{ all
$\sigma$'s complete executions starting from $[s]^{i}$ are finite, and }\\\
&&2.[t]^{i}{\subseteq}\\{s^{\prime}\in
W\mid{M},s^{\prime}\vDash\varphi\\}\text{ for all
}[t]^{i}{\in}\mathtt{ECE}(\sigma,[s]^{i}).\\\ \end{array}$

######  Proposition 6.

The following formulas are valid.

  1. (1).

${K}_{i}\varphi\to{K}h_{i}\varphi$

  2. (2).

${K}h_{i}\varphi\to{K}_{i}{K}h_{i}\varphi$

  3. (3).

$\neg{K}h_{i}\varphi\to{K}_{i}\neg{K}h_{i}\varphi$

  4. (4).

${K}h_{i}\varphi\to{K}h_{i}{K}_{i}\varphi$

  5. (5).

${K}h_{i}{K}h_{i}\varphi\to{K}h_{i}\varphi$

###### Proof.

For (1), it is due to the empty strategy. For (2), (3), and (4), it follows
from the semantics. For (5), see [6]. ∎

##  3 Tableaux

This section presents a tableau procedure for the logic $\textsf{ELKh}_{n}$
and shows the soundness of the tableau procedure.

Given $\varphi$, let $sub^{+}(\varphi)$ be the set $\\{\psi,\neg\psi\mid\psi$
is a subformula of
$\varphi\\}\cup\\{{K}_{i}\psi,\neg{K}_{i}\psi\mid{K}h_{i}\psi$ is a subformula
of $\varphi\\}$.

###  3.1 Tableau procedure

A tableau is a rooted tree in which each node is labeled with a set of
prefixed formulas. A prefixed formula is a pair $\langle\sigma,\varphi\rangle$
where the prefix $\sigma$ is an alternative sequence of natural numbers and
agents or ${K}h$-formulas, such as $\langle 1i2{{K}h_{i}p}3,\varphi\rangle$.
The prefixes represent states in models. The agent symbols and ${K}h$-formulas
occurring in $\sigma$ indicate some epistemic information and action
information on the current state. For example, the prefix $1i2{{K}h_{i}p}3$
indicates the following informations: there are three states $1$, $2$, and
$3$; $1\sim_{i}2$; there is an action $a$ such that $a$ is a good plan for
$2\vDash{K}h_{i}p$ and $(2,3)\in R_{a}$.

######  Definition 7 (Tableaux).

A tableau for $\varphi_{0}$ is a labeled tree that is defined as follows:

  * A.

Create the root node and label it with $\langle 0,\varphi_{0}\rangle$;

  * B.

Extend the tree by rules in Table 1.

$\langle\sigma,\neg\neg\varphi\rangle$ $(R\neg)$ $\langle\sigma,\varphi\rangle$ |
---|---
$\langle\sigma,\neg(\varphi_{1}\wedge\varphi_{2})\rangle$ $(R\vee)$ $\langle\sigma,\neg\varphi_{1}\rangle$ $\langle\sigma,\neg\varphi_{1}\rangle$ $\langle\sigma,\varphi_{1}\rangle$ $\langle\sigma,\neg\varphi_{2}\rangle$ $\langle\sigma,\varphi_{2}\rangle$ $\langle\sigma,\neg\varphi_{2}\rangle$ |  $\langle\sigma,\varphi_{1}\wedge\varphi_{2}\rangle$ $(R\wedge)$ $\langle\sigma,\varphi_{1}\rangle$ $\langle\sigma,\varphi_{2}\rangle$
$\langle\sigma,\neg{K}_{i}\varphi\rangle$ (Cut$\neg{K}$)  $\langle\sigma,\neg\varphi\rangle\mid\langle\sigma,\varphi\rangle$ |  $\langle\sigma,{K}_{i}\varphi\rangle$ $(Cut{K})$ $\langle\sigma,\varphi\rangle$
$\langle\sigma,{K}h_{i}\varphi\rangle$ (Cut${K}h$)  $\langle\sigma,\neg{K}_{i}\varphi\rangle$ $\langle\sigma,{K}_{i}\varphi\rangle$ |  $\langle\sigma,\neg{K}h_{i}\varphi\rangle$ (Cut$\neg{K}h$)  $\langle\sigma,\neg{K}_{i}\varphi\rangle$
$\langle\sigma,\neg{K}_{i}\varphi\rangle$ $(R\neg{{K}})$ $n^{\prime}$ is new $\langle\sigma in^{\prime},\neg\varphi\rangle$ |  $\langle\sigma,{K}_{i}\varphi\rangle$ $(R{K})$ $\sigma in^{\prime}$ is used $\langle\sigma in^{\prime},\varphi\rangle$
$\langle\sigma,{K}_{i}\varphi\rangle$ $(R{K}4)$ $\sigma in^{\prime}$ is used $\langle\sigma in^{\prime},{K}_{i}\varphi\rangle$ |  $\langle\sigma,\neg{K}_{i}\varphi\rangle$ $(R{K}5)$ $\sigma in^{\prime}$ is used $\langle\sigma in^{\prime},\neg{K}_{i}\varphi\rangle$
$\langle\sigma,{K}h_{i}\varphi\rangle$ $(R{K}h4)$ $\sigma in^{\prime}$ is used $\langle\sigma in^{\prime},{K}h_{i}\varphi\rangle$ |  $\langle\sigma,\neg{K}h_{i}\varphi\rangle$ $(R{K}h5)$ $\sigma in^{\prime}$ is used $\langle\sigma in^{\prime},\neg{K}h_{i}\varphi\rangle$
$\langle\sigma,{K}h_{i}\varphi\rangle$ $\langle\sigma,\neg{K}_{i}\varphi\rangle$ $(R{{K}h})$ $n^{\prime}$ is new $\langle\sigma{K}h_{i}\varphi n^{\prime},{K}_{i}\varphi\rangle$ |  $\langle\sigma,\neg{K}h_{i}\varphi\rangle$ $\langle\sigma,{K}h_{i}\psi\rangle$ $\langle\sigma,\neg{K}_{i}\psi\rangle$ $(R\neg{K}h)$ $n^{\prime}$ is new $\langle\sigma{K}h_{i}\psi n^{\prime},{K}_{i}\psi\rangle$ $\langle\sigma{K}h_{i}\psi n^{\prime},\neg{K}h_{i}\varphi\rangle$
Table 1: Tableau rules

Next, we will give a procedure to construct a tableau (Definition 8 below). In
Section 3.2, we will show that the procedure is sound, and we in Section 4.1
will show that it is complete, and we in Section 4.2 will show that it runs in
polynomial space. Before that, we first introduce some auxiliary notations
below.

Let $\mathbf{A}$ be a set of actions. We use $\mathbf{A}^{+}$ to denote the
set $\mathbf{A}\cup\\{\epsilon\\}$. Let $\Gamma$ be a set of formulas. We use
$\Gamma|{K}_{i}$, $\Gamma|\neg{K}_{i}$ and $\Gamma|{K}h_{i}$ to respectively
denote the set $\\{\varphi\in\Gamma\mid\varphi$ is of the form
${K}_{i}\psi\\}$, $\\{\varphi\in\Gamma\mid\varphi$ is of the form
$\neg{K}_{i}\psi\\}$ and $\\{\varphi\in\Gamma\mid\varphi$ is of the form
${K}h_{i}\psi\\}$. We say that a formula set $\Gamma$ is _blatantly
inconsistent_ iff either $\varphi,\neg\varphi\in\Gamma$ for some formula
$\varphi$ or $\bot\in\Gamma$.

A labeled tree $\mathscr{T}$ is a triple $\langle N,E,L\rangle$, where
$\langle N,E\rangle$ is a rooted tree with the node set $N$ and the edge set
$E$ and $L:N\cup
E\to\mathcal{P}(\mathcal{L}_{\textsf{ELKh}_{n}})\cup\mathbf{I}\cup\mathbf{A}^{+}$
is a label function such that each node is labeled a formula set and each edge
is labeled an agent $i\in\mathbf{I}$ or an action $a\in\mathbf{A}^{+}$. A node
sequence $n_{1}\cdots n_{h+1}$ is a _path_ in $\mathscr{T}$ if
$(n_{k},n_{k+1})\in E$ for all $1\leq k\leq h$. If the node sequence
$n_{1}\cdots n_{h+1}$ is a path in $\mathscr{T}$ and the label
$L(n_{k},n_{k+1})$ is either $i\in\mathbf{I}$ or $\epsilon$ for all $1\leq
k\leq h$, we then say that $n_{1}$ is an _$i$ -ancestor_ of $n_{h+1}$.

A tree is called an _and-or_ tree if each non-leaf node is marked as “and”
node or “or” node. A subtree of an and-or tree is called _complete_ if it
contains the root node, and each “and” non-leaf node has all its child nodes,
and each “or” non-leaf node has at least one child node.

Now we are ready to give a procedure to construct a tableau. We remark that,
strictly speaking, the tree constructed by the following procedure is not
really a tableau. Rather, it is a tree in which the desired tableau is
embedded. Such trees are called _pre-tableaux_ in [8]. Since in the remaining
paper, we will work only on the following procedure and show that the
following procedure is sound and complete and runs in polynomial space, it
does not matter what we call it. So, in the remaining paper, we will call the
tree constructed by the following procedure a tableau.

######  Definition 8 (Tableaux construction).

A tableau for $\varphi_{0}$ is a labeled and-or tree
$\mathscr{T}_{\varphi_{0}}$ which is constructed by the following steps:

  * (I).

Construct a tree consisting of a single node $n_{0}$ (i.e. the root node), and
label the root node the formula set $\\{\varphi_{0}\\}$.

  * (II).

Repeat until none of (1)-(2) below applies:

    * (1).

Forming a subformula-closed propositional tableau: if $n$ is an unblocked leaf
node and $L(n)$ is not blatantly inconsistent, then mark $n$ as an “or” node
and check the first unchecked formula $\varphi\in L(n)$ at $n$ by the
following:

      * (a).

If $\varphi$ is of the form $\neg\neg\psi$ and $\psi$ is not in $L(n)$, then
create a successor node $n^{\prime}$ of $n$, set

$\begin{array}[]{ll}&L(n^{\prime})=L(n)\cup\\{\psi\\},\\\
&L(n,n^{\prime})=\epsilon,\end{array}$

and mark $\varphi$ and all checked formulas at $n$ as “checked” at
$n^{\prime}$.

      * (b).

If $\varphi$ is of the form $\varphi_{1}\land\varphi_{2}$ and either
$\varphi_{1}$ or $\varphi_{2}$ is not in $L(n)$, then create a successor node
$n^{\prime}$ of $n$, set

$\begin{array}[]{ll}&L(n^{\prime})=L(n)\cup\\{\varphi_{1},\varphi_{2}\\},\\\
&L(n,n^{\prime})=\epsilon,\end{array}$

and mark $\varphi$ and all checked formulas at $n$ as “checked” at
$n^{\prime}$

      * (c).

If $\varphi$ is of the form $\neg(\varphi_{1}\land\varphi_{2})$ and none of
the three sets $\\{\neg\varphi_{1},\neg\varphi_{2}\\}$,
$\\{\neg\varphi_{1},\neg\varphi_{2}\\}$,
$\\{\neg\varphi_{1},\neg\varphi_{2}\\}$ is a subset of $L(n)$, then create
three successors $n_{1},n_{2},n_{3}$ of $n$, set

$\begin{array}[]{ll}&L(n_{1})=L(n)\cup\\{\neg\varphi_{1},\neg\varphi_{2}\\},\\\
&L(n_{2})=L(n)\cup\\{\neg\varphi_{1},\varphi_{2}\\},\\\
&L(n_{3})=L(n)\cup\\{\varphi_{1},\neg\varphi_{2}\\},\\\
&L(n,n_{1})=L(n,n_{2})=L(n,n_{3})=\epsilon,\end{array}$

and mark $\varphi$ and all checked formulas at $n$ as “checked” at
$n_{1},n_{2},n_{3}$

      * (d).

If $\varphi$ is of the form ${K}_{i}\psi$ and $\psi$ is not in $L(n)$, then
create a successor node $n^{\prime}$ of $n$, and set

$\begin{array}[]{ll}&L(n^{\prime})=L(n)\cup\\{\psi\\},\\\
&L(n,n^{\prime})=\epsilon,\end{array}$

and mark $\varphi$ and all checked formulas at $n$ as “checked” at
$n^{\prime}$

      * (e).

If $\varphi$ is of the form $\neg{K}_{i}\psi$ and neither $\neg\psi$ nor
$\psi$ is in $L(n)$, then create two successors $n_{1},n_{2}$ of $n$, set

$\begin{array}[]{ll}&L(n_{1})=L(n)\cup\\{\neg\psi\\},\\\
&L(n_{2})=L(n)\cup\\{\psi\\},\\\ &L(n,n_{1})=L(n,n_{2})=\epsilon\end{array}$

and mark $\varphi$ and all checked formulas at $n$ as “checked” at $n_{1}$ and
$n_{2}$

      * (f).

If $\varphi$ is of the form ${K}h_{i}\psi$ and neither $\neg{K}_{i}\psi$ nor
${K}_{i}\psi$ is in $L(n)$, then create two successors $n_{1},n_{2}$ of $n$,
set

$\begin{array}[]{ll}&L(n_{1})=L(n)\cup\\{\neg{K}_{i}\psi\\},\\\
&L(n_{2})=L(n)\cup\\{{K}_{i}\psi\\},\\\
&L(n,n_{1})=L(n,n_{2})=\epsilon,\end{array}$

and mark $\varphi$ and all checked formulas at $n$ as “checked” at $n_{1}$ and
$n_{2}$.

      * (g).

If $\varphi$ is of the form $\neg{K}h_{i}\psi$ and $\neg{K}_{i}\psi$ is not in
$L(n)$, then create a successor $n^{\prime}$ of $n$, set

$\begin{array}[]{ll}&L(n^{\prime})=L(n)\cup\\{\neg{K}_{i}\psi\\},\\\
&L(n,n^{\prime})=\epsilon,\end{array}$

and mark $\varphi$ and all checked formulas at $n$ as “checked” at
$n^{\prime}$

      * (h).

if none of (a)-(g) above applies, then mark $\varphi$ as “checked”.

    * (2).

Creating successors for $\neg{K}_{i},{K}h_{i},\neg{K}h_{i}$ formulas: if $n$
is an unblocked leaf node, $L(n)$ is not blatantly inconsistent, and each
formula in $L(n)$ is marked as “checked”, then mark (or re-mark) $n$ as an
“and” node and do the following:

      * (i).

For each formula in $L(n)$ of the form $\neg{K}_{i}\psi$ , if there is no
$i$-ancestor of $n^{\prime}$ such that
$L(n^{\prime})=\Sigma(n,\neg{K}_{i}\psi)$, then create a successor
$n_{\neg{K}_{i}\psi}$ of $n$ and set

$\begin{array}[]{ll}&L(n_{\neg{K}_{i}\psi})=\Sigma(n,\neg{K}_{i}\psi),\\\
&L(n,n_{\neg{K}_{i}\psi})=i\end{array}$

in which

$\Sigma(n,\neg{K}_{i}\psi)=\\{\neg\psi\\}\cup(L(n)|{K}_{i})\cup(L(n)|\neg{K}_{i})\cup(L(n)|{K}h_{i})\cup(L(n)|\neg{K}h_{i}).$

      * (j).

For each pair on $L(n)$ of the form $({K}h_{i}\psi,\neg{K}_{i}\psi)$, create a
successor $n_{{K}h_{i}\psi}$ of $n$, and set

$\begin{array}[]{ll}&L(n_{{K}h_{i}\psi})=\\{{K}_{i}\psi\\},\\\
&L(n,n_{{K}h_{i}\psi})=a_{{K}h_{i}\psi}.\end{array}$

      * (k).

For each triple on $L(n)$ of the form
$(\neg{K}h_{i}\chi,{K}h_{i}\psi,\neg{K}_{i}\psi)$, create a successor
$n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}$, and set

$\begin{array}[]{ll}&L(n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)})=\\{{K}_{i}\psi,\neg{K}h_{i}\chi\\},\\\
&L(n,n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)})=a_{{K}h_{i}\psi}.\end{array}$

Moreover, if there is an ancestor $n^{\prime}$ of
$n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}$ such that
$L(n^{\prime})=L(n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)})$, then mark
$n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}$ as blocked, and we say that
$n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}$ is blocked by $n^{\prime}$.

######  Definition 9.

A subtree of a tableau is _closed_ if there is some node $n$ in it such that
$L(n)$ is blatantly inconsistent. Otherwise, it is called _open_. A tableau is
_closed_ iff all its complete subtrees are closed.

###  3.2 Soundness

In this subsection, we will show that the procedure of Definition 8 is sound.

######  Definition 10 (Interpretations).

Given a model ${M}$ and a subtree $\mathscr{T}^{\prime}=\langle
N^{\prime},E^{\prime},L^{\prime}\rangle$ of the tableau
$\mathscr{T}_{\varphi_{0}}$, let $f$ be a function from $N^{\prime}$ to $W$.
We say that $f$ is an _interpretation_ of $\mathscr{T}^{\prime}$ if and only
if ${M},f(n)\vDash\varphi$ for all $\varphi\in L(n)$ and all $n\in
N^{\prime}$.

######  Lemma 11.

If ${M},s\vDash\varphi_{0}$, then there exists an interpretation of some
complete subtree of any $\mathscr{T}_{\varphi_{0}}$.

###### Proof.

Let $f_{0}$ be the function $f_{0}=\\{n_{0}\mapsto s\\}$ which maps the root
$n_{0}$ of $\mathscr{T}_{\varphi_{0}}$ to the state $s$. It is obvious that
${M},f_{0}(n_{0})\vDash\varphi$ for all $\varphi\in L(n_{0})$.

Then we only need to show the following statement:

If $n$ is a leaf node of a subtree $\mathscr{T}$, $f$ is an interpretation of
$\mathscr{T}$, and $n$ is in the domain of $f$, then

(A): for each construction steps (a)-(g), there is an interpretation of
$\mathscr{T}$ extending with one child node of $n$, and

(B): for each construction steps (i)-(k), there is an interpretation of
$\mathscr{T}$ extending with all child nodes of $n$.

For (A), firstly it is obvious for the steps (a)-(c). For the step (d), it
follows that $\sim_{i}$ is a reflexive relation. For the steps (e) and (f), it
follows from the fact that a formula is either true or false on a state. For
the step (g), it follows from the fact that
$\neg{K}h_{i}\psi\to\neg{K}_{i}\psi$ is valid (see Proposition 6).

Next, we will show that (B) holds.

For the step (i), for each $n$’s child node $n_{\neg{K}_{i}\psi}$, we know
that $\neg{K}_{i}\psi\in L(n)$ and
$L(n_{\neg{K}_{i}\psi})=\\{\neg\psi\\}\cup(L(n)|{K}_{i})\cup(L(n)|\neg{K}_{i})\cup(L(n)|{K}h_{i})\cup(L(n)|\neg{K}h_{i})$.
Since $f$ is an interpretation of $\mathscr{T}$ including $n$, it follows that
${M},f(n)\vDash\neg{K}_{i}\psi$. Hence, there exists a state
$t_{\neg{K}_{i}\psi}\in[f(n)]^{i}$ such that
${M},t_{\neg{K}_{i}\psi}\vDash\neg\psi$. Moreover, since $\sim_{i}$ is an
equivalence relation, $({M},t_{\neg{K}_{i}\psi})$ satisfies all the
${K}_{i}$-formulas and $\neg{K}_{i}$-formulas that are true at $f(n)$.
Furthermore, by Proposition 6, we have that $({M},t_{\neg{K}_{i}\psi})$
satisfies all the ${K}h_{i}$-formulas and $\neg{K}h_{i}$-formulas that are
true at $f(n)$. Let $f^{\prime}$ be the $f$-extension
$f\cup\\{n_{\neg{K}_{i}\psi}\mapsto t_{\neg{K}_{i}\psi}\mid
n_{\neg{K}_{i}\psi}$ is a child node of $n\\}$. Therefore, we have that
${M},f^{\prime}(n_{\neg{K}_{i}\psi})\vDash L(n_{\neg{K}_{i}\psi})$.

For the step (j), for each $n$’s child node $n_{{K}h_{i}\psi}$, we know that
${K}h_{i}\psi\in L(n)$ and $L(n_{\neg{K}_{i}\psi})=\\{{K}_{i}\psi\\}$. Since
$f$ is an interpretation of $\mathscr{T}$ including $n$, it follows that
${M},f(n)\vDash{K}h_{i}\psi$. So, by the semantics, there exist an
$i$-strategy $\sigma$ and a state
$t_{{K}h_{i}\psi}\in\mathtt{ECE}(\sigma,[f(n)]^{i})$ such that
${M},t_{{K}h_{i}\psi}\vDash{K}_{i}\psi$. Let $f^{\prime}$ be the $f$-extension
$f\cup\\{n_{{K}h_{i}\psi}\mapsto t_{{K}h_{i}\psi}\mid n_{{K}h_{i}\psi}$ is a
child node of $n\\}$. Therefore, we have that
${M},f^{\prime}(n_{{K}h_{i}\psi})\vDash L(n_{{K}h_{i}\psi})$.

For the step (k), for each $n$’s child node
$n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}$, we know that
$\neg{K}h_{i}\chi,{K}h_{i}\psi\in L(n)$ and
$L(n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)})=\\{{K}_{i}\psi,\neg{K}h_{i}\chi\\}$.
Since $f$ is an interpretation of $\mathscr{T}$ including $n$, it follows that
${M},f(n)\vDash\neg{K}h_{i}\chi\land{K}h_{i}\psi$. Due to
${M},f(n)\vDash{K}h_{i}\psi$, it follows by the semantics that there exist an
$i$-strategy $\sigma$ such that ${M},t\vDash{K}_{i}\psi$ for all
$[t]^{i}\in\mathtt{ECE}(\sigma,[f(n)]^{i})$. Moreover, it must be the case
that there exists $t_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}$ such that
$[t_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}]^{i}\in\mathtt{ECE}(\sigma,[f(n)]^{i})$
and ${M},t_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}\vDash\neg{K}h_{i}\chi$.
Otherwise, if ${M},t\vDash{K}h_{i}\chi$ for all
$[t]^{i}\in\mathtt{ECE}(\sigma,[f(n)]^{i})$, this implies
${M},f(n)\vDash{K}h{K}h_{i}\chi$. By Proposition 6, it follows that
${M},f(n)\vDash{K}h_{i}\chi$, which is contradictory with the fact that
${M},f(n)\vDash\neg{K}h_{i}\chi$. Hence, there exists
$t_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}$ such that
$[t_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}]^{i}\in\mathtt{ECE}(\sigma,[f(n)]^{i})$
and ${M},t_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}\vDash\neg{K}h_{i}\chi$, which
implies that
${M},t_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}\vDash\neg{K}h_{i}\chi\land{K}_{i}\psi$.
Let $f^{\prime}$ be the $f$-extension
$f\cup\\{n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}\mapsto
t_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}\mid n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}$
is a child node of $n\\}$. Therefore, we have that
${M},f^{\prime}(n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)})\vDash
L(n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)})$. ∎

The soundness below follows from Lemma 11 above.

######  Theorem 12 (Soundness).

If $\varphi_{0}$ is satisfiable, then $\mathscr{T}_{\varphi_{0}}$ is not
closed.

##  4 Completeness and complexity

###  4.1 Completeness

In this subsection, we will show that the procedure of Definition 8 is
complete.

Recall that $sub^{+}(\varphi)$ is the set $\\{\psi,\neg\psi\mid\psi$ is a
subformula of $\varphi\\}\cup\\{{K}_{i}\psi,\neg{K}_{i}\psi\mid{K}h_{i}\psi$
is a subformula of $\varphi\\}$. From the construction of
$\mathscr{T}_{\varphi_{0}}$, it follows that $L(n)\subseteq
sub^{+}(\varphi_{0})$ for each node $n$. Moreover, each formula in $L(n)$ is
“inherited” from $n$’s ancestors, that is, if $\psi\in L(n)$ and $n^{\prime}$
is an ancestor of $n$ then there exists $\varphi\in L(n^{\prime})$ such that
$\psi\in sub^{+}(\varphi)$.

A path $n_{1}\cdots n_{h}$ of $\mathscr{T}_{\varphi_{0}}$ is called an
$\epsilon$-path iff $L(n_{k},n_{k+1})=\epsilon$ for all $1\leq k<h$.
Particularly, a path with length 1 is an $\epsilon$-path. An $\epsilon$-path
$n_{1}\cdots n_{h}$ is _maximal_ iff there are no such nodes $n$ and
$n^{\prime}$ that either $nn_{1}\cdots n_{h}$ or $n_{1}\cdots n_{h}n^{\prime}$
is an $\epsilon$-path. Given a path $\rho=n_{1}\cdots n_{h}$, we use
$ini(\rho)$, $end(\rho)$ and $L(\rho)$ to respectively denote $n_{1}$, $n_{h}$
and $L(n_{h})$. We use $\rho\xrightarrow{x}\rho^{\prime}$ to means that
$\rho\rho^{\prime}$ is a path and $L(end(\rho),ini(\rho^{\prime}))=x$.

From the construction of $\mathscr{T}_{\varphi_{0}}$ we know that if a node
$n$ is blocked then there is a unique node $n^{\prime}$ which blocks $n$ and
$n$ itself is a maximal $\epsilon$-path. Moreover, if $\rho$ is a maximal
$\epsilon$-path and $end(\rho)$ is blocked, then $\rho$ is a single node, i.e.
$\rho=n$ where the node $n$ is blocked.

For each maximal $\epsilon$-path $\rho$ of $\mathscr{T}_{\varphi_{0}}$, by the
construction, we know that if $\rho$ is not blocked and $L(\rho)$ is not
blatantly inconsistent then each formula in $L(\rho)$ is marked as “checked”.
This means that $L(\rho)$ is closed over $sub^{+}$-formulas, that is, if
$\varphi\in L(\rho)$ then either $\psi$ or $\sim\psi$ is in $L(\rho)$ for all
$\psi\in sub^{+}(\varphi)$, where $\sim\psi=\chi$ if $\psi=\neg\chi$,
otherwise $\sim\psi=\neg\psi$.

######  Definition 13 (${M}^{\mathscr{T}}$).

Let $\mathscr{T}$ be a complete subtree of $\mathscr{T}_{\varphi_{0}}$. The
model induced by $\mathscr{T}$, denoted by ${M}^{\mathscr{T}}$, is defined as
follows:

  * •

$W=\\{\rho\mid\rho$ is a maximal $\epsilon$-path of $\mathscr{T}$, and $\rho$
is not blocked$\\}$,

  * •

$\sim_{i}$ is the minimal equivalence relation $X$ on $W$ such that
$\\{(\rho,\rho^{\prime})\mid\rho\xrightarrow{i}\rho^{\prime}\\}\subseteq X$,

  * •

$\mathbf{A}_{i}=\\{a_{{K}h_{i}\psi}\mid$ there exists an edge $(n,n^{\prime})$
in $\mathscr{T}$ such that $L(n,n^{\prime})=a_{{K}h_{i}\psi}\\}$.

  * •

for each $a\in\mathbf{A}_{i}$,
$R_{a}=\\{(\rho,\rho^{\prime})\mid\rho\xrightarrow{a}\rho^{\prime}$, or
$\rho\xrightarrow{a}\rho^{\prime\prime}$ where $\rho^{\prime\prime}$ is a
maximal $\epsilon$-path blocked by $\rho^{\prime}\\}$.

  * •

$f(\rho)\in V(p)$ iff $p\in L(f(\rho))$.

Please note that by the definition $\mathbf{A}_{i}$, we know that if $i\neq j$
then $\mathbf{A}_{i}\cap\mathbf{A}_{j}=\emptyset$.

The following proposition states that all paths in the same $\sim_{i}$-closure
share the same formulas in the forms ${K}_{i}\varphi$, $\neg{K}_{i}\varphi$,
${K}h_{i}\varphi$, or $\neg{K}h_{i}\varphi$.

######  Proposition 14.

Let $\mathscr{T}$ be a complete and open subtree of
$\mathscr{T}_{\varphi_{0}}$. If $\rho_{1}\sim_{i}\rho_{2}$ in
${M}^{\mathscr{T}}$, then $L(\rho_{1})|x=L(\rho_{2})|x$ where
$x\in\\{{K}_{i},\neg{K}_{i},{K}h_{i},\neg{K}h_{i}\\}$.

###### Proof.

Besides $\rho_{1}=\rho_{2}$, there are three possible cases: (1)
$end(\rho_{1})$ is an $i$-ancestor of $end(\rho_{2})$, or (2) $end(\rho_{2})$
is an $i$-ancestor of $end(\rho_{1})$, or (3) there is some $\rho\in W$ such
that $end(\rho)$ is an $i$-ancestor of both $end(\rho_{1})$ and
$end(\rho_{2})$.

For (1), firstly we will show that $L(\rho_{1})|x\subseteq L(\rho_{2})|x$. In
the construction step (i) all $x$-formulas are inherited from the
$i$-ancestor. Moreover, in the steps (a)-(f) all formulas labeled on the
parent node are inherited by each child node. Thus, $L(\rho_{1})|x\subseteq
L(\rho_{2})|x$.

Secondly, we will show that $L(\rho_{2})|x\subseteq L(\rho_{1})|x$. Since
$end(\rho_{1})$ is an ancestor of $end(\rho_{2})$, we know from the
construction that for each formula $\psi\in L(\rho_{2})$ there exists
$\varphi\in L(\rho_{1})$ such that $\psi\in sub^{+}(\varphi)$. Moreover, since
$\rho_{1}$ is a non-blocked maximal $\epsilon$-path and $L(\rho_{1})$ is not
blatantly inconsistent, it follows that all formulas in $L(\rho_{1})$ are
marked as “checked”. So, $L(\rho_{1})$ is closed over $sub^{+}$-formulas.
Hence, for each $x$-formula $\chi\in L(\rho_{2})$, either $\chi$ or $\sim\chi$
is in $L(\rho_{1})$. If $\sim\chi\in L(\rho_{1})$, since $\sim\chi$ will be
inherited to $L(\rho_{2})$, it means that $L(\rho_{2})$ will be blatantly
inconsistent, which is contradictory with the fact that $\mathscr{T}$ is open.
Therefore, it only can be that $\chi\in L(\rho_{1})$. Hence,
$L(\rho_{2})|x\subseteq L(\rho_{1})|x$.

For (2), it can be shown by the same process as for (1).

For (3), by (1) we know that $L(\rho)|x=L(\rho_{1})|x$ and
$L(\rho)|x=L(\rho_{2})|x$. Thus, $L(\rho_{1})|x=L(\rho_{2})|x$. ∎

Before we show the truth lemma, we need the following auxiliary proposition.

######  Proposition 15.

Let $\mathscr{T}$ be a complete subtree of $\mathscr{T}_{\varphi_{0}}$,
$\sigma$ be an $i$-strategy in ${M}^{\mathscr{T}}$, and
$\delta=[\rho_{1}]^{i}\cdots[\rho_{h}]^{i}$ be a $\sigma$-execution in
${M}^{\mathscr{T}}$. If $\neg{K}h_{i}\chi\in L(\rho_{h})$ and $\delta$ is not
complete, then there exists some $\rho\in W$ such that $\delta[\rho]^{i}$is a
$\sigma$-execution and $\neg{K}h_{i}\chi\in L(\rho)$.

###### Proof.

Since $[\rho_{1}]^{i}\cdots[\rho_{h}]^{i}$ is not complete, it follows that
$[\rho_{h}]^{i}\in\mathtt{dom}(\sigma)$. Let
$\sigma([\rho_{h}]^{i})=a_{{K}h_{i}\psi}$ for some
$a_{{K}h_{i}\psi}\in\mathbf{A}_{i}$. Since $\sigma$ is a uniformly executable
strategy, this means that $a_{{K}h_{i}}$ is executable on $\rho_{h}$. By the
definition of ${M}^{\mathscr{T}}$ in Definition 13, we know that there exists
a maximal $\epsilon$-path $\rho^{\prime}$ of $\mathscr{T}$ such that
$\rho_{h}\xrightarrow{a_{{K}h_{i}\psi}}\rho^{\prime}$, that is,
$\rho_{h}\rho^{\prime}$ is a path of $\mathscr{T}$ and
$L(end(\rho_{h}),ini(\rho^{\prime}))=a_{{K}h_{i}\psi}$. Note that such labels
can only be added by the construction step (j) or (k).

From the construction steps (j) and (k), we then have that
${K}h_{i}\psi,\neg{K}_{i}\psi\in L(\rho_{h})$. Since we also have that
$\neg{K}h_{i}\chi\in L(\rho_{h})$, by the construction step (k), there is a
node $n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}$ in $\mathscr{T}_{\varphi_{0}}$ such
that
$L(n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)})=\\{{K}_{i}\psi,\neg{K}h_{i}\chi\\}$
and $L(end(\rho_{h}),n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)})=a_{{K}h_{i}\psi}$.

Since $\mathscr{T}$ is a complete subtree of $\mathscr{T}_{\varphi_{0}}$, it
follows that $n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}$ is also a node in
$\mathscr{T}$. There are two cases: $n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}$ is
blocked or not.

If $n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}$ is not blocked, let $\rho$ be the
maximal $\epsilon$-path in $\mathscr{T}$ that begins with the node
$n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}$. By the definition of
${M}^{\mathscr{T}}$, we know that $(\rho_{h},\rho)\in R_{a_{{K}h_{i}\psi}}$.
This means that $[\rho_{1}]^{i}\cdots[\rho_{h}]^{i}[\rho]^{i}$ is a
$\sigma$-execution. Moreover, due to $\neg{K}h_{i}\chi\in L(ini(\rho))$, it
follows that $\neg{K}h_{i}\chi\in L(\rho)$.

If $n_{(\neg{K}h_{i}\chi,{K}h_{i}\psi)}$ is blocked by its some node
$n^{\prime}$, then $n^{\prime}$ is an ancestor of $n$. So, we have that
$n^{\prime}$ is a node in $\mathscr{T}$. Let $\rho^{\prime\prime}$ be the
maximal $\epsilon$-path that contains $n^{\prime}$. Since block nodes are leaf
nodes, it follows that $\rho^{\prime\prime}$ is not blocked. Thus,
$\rho^{\prime\prime}\in W$. By the definition of ${M}^{\mathscr{T}}$, we have
that $(\rho_{h},\rho^{\prime\prime})\in R_{a_{{K}h_{i}\psi}}$. This means that
$[\rho_{1}]^{i}\cdots[\rho_{h}]^{i}[\rho^{\prime\prime}]^{i}$ is a
$\sigma$-execution. Moreover, due to $\neg{K}h_{i}\chi\in L(n)$,
$L(n)=L(n^{\prime})$ and $L(n^{\prime})\subseteq L(\rho)$, it follows that
$\neg{K}h_{i}\chi\in L(\rho)$. ∎

######  Lemma 16 (Truth lemma).

If $\mathscr{T}$ is a complete and open subtree of
$\mathscr{T}_{\varphi_{0}}$, then for each $\varphi\in sub^{+}(\varphi_{0})$,
we have that ${M}^{\mathscr{T}},\rho\vDash\varphi$ iff $\varphi\in L(\rho)$.

###### Proof.

We prove it by induction on $\varphi$. Since $L(\rho)$ is closed over
$sub^{+}$-formulas, the atomic case and Boolean cases are straightforward.
Next, we will focus on the cases of ${K}_{i}\psi$ and ${K}h_{i}\psi$.

For the case ${K}_{i}\psi\in L(\rho)$, given $\rho^{\prime}\in[\rho]^{i}$, we
will show that ${M}^{\mathscr{T}},\rho^{\prime}\vDash\psi$. By Proposition 14,
we have that ${K}_{i}\psi\in L(\rho^{\prime})$. Moreover, since $\mathscr{T}$
is open and $\rho^{\prime}$ is not blocked, this means that all formulas in
$L(\rho^{\prime})$ are marked as “checked”. Let $\rho^{\prime}=n_{1}\cdots
n_{h}$. From the construction, we know that there is some node $n_{k}$, where
$1\leq k\leq h$, such that the first time in $\rho^{\prime}$ the formula
${K}_{i}\psi$ is marked as “checked”, and this only can be done by the
construction step (d). Thus, we have that $\psi\in L(n_{k})$, and then
$\psi\in L(\rho^{\prime})$. By IH, we have that
${M}^{\mathscr{T}},\rho^{\prime}\vDash\psi$.

For the case ${K}_{i}\psi\not\in L(\rho)$, since $L(\rho)$ is closed over
$sub^{+}$-formulas, it follows that $\neg{K}_{i}\psi\in L(\rho)$. Let
$end(\rho)$ be the node $n$. Since $\rho$ is a non-blocked maximal
$\epsilon$-path and $\mathscr{T}$ is open, this means that all formulas in
$L(n)$ is marked as “checked”. From the construction, we know that the
construction step (i) will be triggered on $n$. Thus, either there is an
$i$-ancestor node $n^{\prime}$ such that $\neg\psi\in L(n^{\prime})$ or there
is an $n$’s $i$-child node $n^{\prime\prime}$ such that $\neg\psi\in
L(n^{\prime\prime})$. Since $\mathscr{T}$ is a complete subtree of
$\mathscr{T}_{\varphi_{0}}$, it follows that no matter $n^{\prime}$ or
$n^{\prime\prime}$ will be included in $\mathscr{T}$. Thus, there is
$\rho^{\prime}\in[\rho]^{i}$ such that $\neg\psi\in L(\rho^{\prime})$. Since
$\mathscr{T}$ is open, it follows that $\psi\not\in L(\rho^{\prime})$. By IH,
we have that ${M}^{\mathscr{T}},\rho\not\vDash\psi$. Hence,
${M}^{\mathscr{T}},\rho\not\vDash{K}_{i}\psi$.

For the case ${K}h_{i}\psi\in L(\rho)$, since $L(\rho)$ is closed over
$sub^{+}$-formulas, it follows that either ${K}_{i}\psi\in L(\rho)$ or
$\neg{K}_{i}\psi\in L(\rho)$.

If ${K}_{i}\psi\in L(\rho)$, by the proof of the ${K}_{i}$-case above, we know
that ${M}^{\mathscr{T}},\rho\vDash{K}_{i}\psi$. By Proposition 6, we have that
${M}^{\mathscr{T}},\rho\vDash{K}h_{i}\psi$.

If $\neg{K}_{i}\psi\in L(\rho)$, we will show that $\sigma$ is a good strategy
for ${M}^{\mathscr{T}},\rho\vDash{K}h_{i}\psi$ where $\sigma$ is the function
$\\{[\rho]^{i}\mapsto a_{{K}h_{i}\psi}\\}$.

If $\rho^{\prime}\in[\rho]^{i}$ and $(\rho^{\prime},\rho^{\prime\prime})\in
R_{a_{{K}h_{i}\psi}}$, then either
$\rho^{\prime}\xrightarrow{a_{{K}h_{i}\psi}}\rho^{\prime\prime}$, or
$\rho^{\prime}\xrightarrow{a_{{K}h_{i}\psi}}\rho^{\prime\prime\prime}$ where
$\rho^{\prime\prime\prime}$ is blocked by $\rho^{\prime\prime}$. For the first
case, it is obvious that $\rho^{\prime\prime}\not\in[\rho]^{i}$. For the
second case, we also have that $\rho^{\prime\prime}\not\in[\rho]^{i}$. The
reason is that nodes can only be blocked in the construction step (k), so for
the second case we have ${K}_{i}\psi\in L(\rho^{\prime\prime\prime})$ and
$L(\rho^{\prime\prime\prime})\subseteq L(\rho^{\prime\prime})$. Due to
$\neg{K}_{i}\psi\in L(\rho)$ and Proposition 14, Therefore, for the second
case we also have that $\rho^{\prime\prime}\not\in[\rho]^{i}$. Thus, we have
shown that if $\rho^{\prime}\in[\rho]^{i}$ and
$(\rho^{\prime},\rho^{\prime\prime})\in R_{a_{{K}h_{i}\psi}}$, then
$\rho^{\prime\prime}\not\in[\rho]^{i}$, which means that
$[\rho^{\prime}]^{i}[\rho^{\prime\prime}]^{i}$ is a complete
$\sigma$-execution from $[\rho]^{i}$. Hence, to show that
${M}^{\mathscr{T}},\rho\vDash{K}h_{i}\psi$, we only need to show that for each
$\rho^{\prime}\in[\rho]^{i}$, (1) the action $a_{{K}h_{i}\psi}$ is executable
at $\rho^{\prime}$, (which means that $\sigma$ is a uniform executable
strategy,) and (2) ${M}^{\mathscr{T}},\rho^{\prime\prime}\vDash{K}_{i}\psi$
for each $\rho^{\prime\prime}$ with $(\rho^{\prime},\rho^{\prime\prime})\in
R_{a_{{K}h_{i}\psi}}$.

For (1), due to ${K}h_{i}\psi,\neg{K}_{i}\psi\in L(\rho)$ and Proposition 14,
we know that ${K}h_{i}\psi,\neg{K}_{i}\psi\in L(\rho^{\prime})$. Thus, by the
construction step (j), there is a node $n_{{K}h_{i}\psi}$ such that
$L(n_{{K}h_{i}\psi})=\\{{K}_{i}\psi\\}$ and
$L(end(\rho^{\prime}),n_{{K}h_{i}\psi})=a_{{K}h_{i}\psi}$. Since $\mathscr{T}$
is a complete subtree of $\mathscr{T}_{\varphi_{0}}$, it follows that
$n_{{K}h_{i}\psi}$ is a node in $\mathscr{T}$. Let $\rho^{\prime\prime\prime}$
be the maximal $\epsilon$-path that begins with $n_{{K}h_{i}\psi}$. We have
that $\rho^{\prime}\xrightarrow{a_{{K}h_{i}\psi}}\rho^{\prime\prime\prime}$,
and then $(\rho^{\prime},\rho^{\prime\prime\prime})\in R_{a_{{K}h_{i}\psi}}$.
Thus, the action $a_{{K}h_{i}\psi}$ is executable at $\rho^{\prime}$.

For (2), if $(\rho^{\prime},\rho^{\prime\prime})\in R_{a_{{K}h_{i}\psi}}$, it
means that either
$L(end(\rho^{\prime}),ini(\rho^{\prime\prime}))=a_{{K}h_{i}\psi}$ or
$L(end(\rho^{\prime}),n^{\prime})=a_{{K}h_{i}\psi}$ where $n^{\prime}$ is
blocked by $\rho^{\prime\prime}$. From the construction, we know that only the
steps (j) and (k) can add such labels. From these steps, we know that
${K}_{i}\psi\in L(ini(\rho^{\prime\prime}))$ or ${K}_{i}\psi\in
L(n^{\prime})$. In either case, we have that ${K}_{i}\psi\in
L(\rho^{\prime\prime})$. By the proof of the ${K}_{i}$-case above, we know
that ${M}^{\mathscr{T}},\rho^{\prime\prime}\vDash{K}_{i}\psi$.

For the case ${K}h_{i}\psi\not\in L(\rho)$, assume that
${M}^{\mathscr{T}},\rho\vDash{K}h_{i}\psi$. By the semantics, there is an
$i$-strategy $\sigma$ such that all compete $\sigma$-executions from
$[\rho]^{i}$ are finite and ${M}^{\mathscr{T}},\rho^{\prime}\vDash{K}_{i}\psi$
for all $[\rho^{\prime}]^{i}\in\mathtt{ECE}(\sigma,[\rho]^{i})$. Due to
${K}h_{i}\psi\not\in L(\rho)$, we have that $\neg{K}h_{i}\psi\in L(\rho)$. By
Proposition 15, we know that there is a complete $\sigma$-execution
$[\rho]^{i}\cdots[\rho^{\prime}]^{i}$ such that $\neg{K}h_{i}\psi\in
L(\rho^{\prime})$. By the construction step (g), we know that
$\neg{K}_{i}\psi\in L(\rho^{\prime})$. Due to ${K}h_{i}\psi\in
sub^{+}(\varphi_{0})$, it follows that ${K}_{i}\psi\in sub^{+}(\varphi_{0})$.
By proof of the $K_{i}$-case above, we have that
${M}^{\mathscr{T}},\rho^{\prime}\vDash\neg{K}_{i}\psi$. Contradiction! Thus,
${M}^{\mathscr{T}},\rho\not\vDash{K}h_{i}\psi$. ∎

The completeness below follows from Lemma 16 above.

######  Theorem 17 (Completeness).

If $\mathscr{T}_{\varphi_{0}}$ is not closed, then $\varphi_{0}$ is
satisfiable.

###  4.2 Complexity

In this section, we will show that the procedure of Definition 8 runs in
polynomial space.

######  Definition 18 (Depth).

The _depth_ of a formula, denoted by $\textit{dep}(\varphi)$, is the depth of
nesting of ${K}$ or ${K}h$ operators, which is defined in Table 2.

$\begin{array}[]{rll}\textit{dep}(\bot)&=&0\\\ \textit{dep}(p)&=&0\\\
\textit{dep}(\neg\psi)&=&\textit{dep}(\psi)\\\
\textit{dep}(\psi\land\chi)&=&max\\{\textit{dep}(\psi),\textit{dep}(\chi)\\}\\\
\textit{dep}({K}_{i}\psi)&=&\textit{dep}(\psi)+1\\\
\textit{dep}({K}h_{i}\psi)&=&\textit{dep}(\psi)+2\end{array}$ Table 2: Depth
of formulas

The reason that $\textit{dep}({K}h_{i}\psi)>\textit{dep}({K}_{i}\psi)$ is that
in the construction steps (j) and (k) we need to label $n$’s child node with
the formula ${K}_{i}\psi$ for ${K}h_{i}\psi\in L(n)$.

######  Proposition 19.

The height of the tableau tree $\mathscr{T}_{\varphi_{0}}$ is bounded by a
polynomial function of the size of the set $sub^{+}(\varphi_{0})$.

###### Proof.

Let the size of $sub^{+}(\varphi_{0})$ be $m$. In the construction of the
tableau tree $\mathscr{T}_{\varphi_{0}}$ in Definition 8, each step of (a)-(k)
might add the height of the tree with 1 degree. The steps (a)-(g) can be
consecutively executed at most $m$ times to get a $sub^{+}$-formula closure.

Now consider a $\mathscr{T}_{\varphi_{0}}$ path that starts from the root
node, and we contract it by seeing the consecutive nodes whose edges are
labeled $\epsilon$ as one single node. Let $n$ be a node in this contracted
path $b$.

If the node $n$’s child node is added by the step (j), then the greatest depth
of formulas labeled on the child node is strictly less than the greatest depth
of formulas labeled on $n$.

If the node $n$’s child node is added by the step (i), although the greatest
depth of formulas labeled on the child node might be the same as the greatest
depth of formulas labeled on $n$, but, such descendant nodes with the same
greatest depth with $n$ can be consecutively added by the step (i) at most $m$
times to achieve a node whose $K_{i}$ ancestor has the same labeled formulas.
After that, if a descendant node $n^{\prime}$ is added by the step (i) again,
then it must be a ${K}_{j}$ descendant where $i\neq j$. Thus, the greatest
depth will be strictly shrunk. If the descendant node $n^{\prime}$ is added by
the step (k), the greatest depth might still keep the same with $n$. However,
the step (k) can be executed on one path at most $m^{2}$ times before it adds
a blocked node.

Hence, there are at most $m^{4}$ consecutive nodes in $b$ that have the same
greatest depth before the greatest depth becomes strictly less. Therefore, the
length of the contracted path $b$ is at most $m^{5}$, and the length of the
original path is at most $m^{6}$. It follows that the height of
$\mathscr{T}_{\varphi_{0}}$ is bounded by $m^{6}$. ∎

######  Lemma 20.

There is an algorithm that runs in polynomial space for deciding whether
$\mathscr{T}_{\varphi_{0}}$ is closed.

###### Proof.

Let the size of $sub^{+}(\varphi_{0})$ be $m$. In the construction step (i),
at most $m$ successors are added. In the step (j), at most $m^{2}$ successors
are added, and in the step (k) at most $m^{3}$ successors are added. This
means that each node has at most $m+m^{2}+m^{3}$ child nodes. Therefore, the
tableau tree $\mathscr{T}_{\varphi_{0}}$ is an $m+m^{2}+m^{3}$-ary tree. By
Proposition 19, we know that the height of the tree is bounded by $m^{6}$.

We can mark the node to check whether the tree is closed. Note that how a node
is marked can be completely determined by its label and how its successors are
marked. Once we have determined how a node is marked, we never have to
consider the subtree below that node again. Thus, a depth-first search of the
tree that runs in polynomial space can decide whether the tree is closed [8].
∎

Since the satisfiability problem of epistemic logic with no less than 2 agents
is PSPACE-hard (see [8]), and it is a fragment of $\textsf{ELKh}_{n}$, it
follows that the satisfiability problem of $\textsf{ELKh}_{n}$ is also PSPACE-
hard. Together with Lemma 20, we have the following result.

######  Theorem 21.

The problem of the satisfiability of $\textsf{ELKh}_{n}$ formulas is PSPACE-
complete.

##  5 Conclusion

This paper presented a tableau procedure for the multi-agent version of the
logic of strategically _knowing how_. The tableau method presented in this
paper is developed from the tableau method for epistemic logic in [8] and the
tableau method for _knowing how_ logic via simple plans [15]. This paper
showed the soundness, the completeness, and the complexity of this tableau
procedure. Since the procedure runs in polynomial space, it follows that the
satisfiability problem of the logic of strategically _knowing how_ can be
decided in PSPACE. Moreover, since the _knowing how_ logic based on PDL-style
knowledge-based plans over finite models in [16] is the same as the logic of
strategically _knowing how_ , it means that the satisfiability problem of that
logic also can be decided in PSPACE.

#### Acknowledgement

The author is grateful to the anonymous reviewers of TARK-2023. Their detailed
comments helped the author to improve the presentation of the paper. The
author also thanks the support from the National Social Science Foundation of
China (Grant No. 18CZX062).

## References

  * [1]
  * [2] Carlos Areces, Raul Fervari, Andrés R. Saravia & Fernando R. Velázquez-Quesada (2021): _Uncertainty-Based Semantics for Multi-Agent Knowing How Logics_.  Electronic Proceedings in Theoretical Computer Science 335, Open Publishing Association, pp. 23–37, 10.4204/EPTCS.335.3.
  * [3] Alexandru Baltag (2016): _To Know is to Know the Value of a Variable_.  In Lev D. Beklemishev, Stéphane Demri & András Maté, editors: Advances in Modal Logic, 11, College Publications, pp. 135–155.  Available at http://www.aiml.net/volumes/volume11/Baltag.pdf.
  * [4] Sophia Epstein & Pavel Naumov (2021): _Epistemic Logic of Know-Who_.  Proceedings of the AAAI Conference on Artificial Intelligence 35(13), pp. 11479–11486, 10.1609/aaai.v35i13.17367.
  * [5] Jie Fan, Yanjing Wang & Hans van Ditmarsch (2015): _Contingency and Knowing Whether_.  Rev. Symb. Log. 8(1), pp. 75–107, 10.1017/S1755020314000343.
  * [6] Raul Fervari, Andreas Herzig, Yanjun Li & Yanjing Wang (2017): _Strategically knowing how_.  In: Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17, pp. 1031–1038, 10.24963/ijcai.2017/143.
  * [7] Tao Gu & Yanjing Wang (2016): _”Knowing value” logic as a normal modal logic_.  In Lev D. Beklemishev, Stéphane Demri & András Maté, editors: Advances in Modal Logic, 11, College Publications, pp. 362–381.  Available at http://www.aiml.net/volumes/volume11/Gu-Wang.pdf.
  * [8] Joseph Y Halpern & Yoram Moses (1992): _A guide to completeness and complexity for modal logics of knowledge and belief_.  Artificial Intelligence. 54(2), pp. 319–379, 10.1016/0004-3702(92)90049-4.
  * [9] Sergiu Hart, Aviad Heifetz & Dov Samet: _“Knowing Whether,” “Knowing That,” and The Cardinality of State Spaces_ 70(1), pp. 249–256.  10.1006/jeth.1996.0084.
  * [10] Andreas Herzig (2015): _Logics of knowledge and action: critical analysis and challenges_.  Autonomous Agents and Multi-Agent Systems 29(5), pp. 719–753, 10.1007/s10458-014-9267-z.
  * [11] Andreas Herzig & Nicolas Troquard (2006): _Knowing How to Play: Uniform Choices in Logics of Agency_.  In: Proceedings of the Fifth International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS ’06, Association for Computing Machinery, New York, NY, USA, p. 209–216, 10.1145/1160633.1160666.
  * [12] J Hintikka (1962): _Knowledge and Belief: An Introduction to the Logic of the Two Notions_.  Cornell University Press, Ithaca N.Y.
  * [13] Wojciech Jamroga & Thomas Ågotnes (2007): _Constructive knowledge: what agents can achieve under imperfect information_.  Journal of Applied Non-Classical Logics 17(4), pp. 423–475, 10.3166/jancl.17.423-475.
  * [14] Yves Lespérance, Hector J. Levesque, Fangzhen Lin & Richard B. Scherl (2000): _Ability and Knowing How in the Situation Calculus_.  Stud Logica 66(1), pp. 165–186, 10.1023/A:1026761331498.
  * [15] Yanjun Li (2021): _Tableau-Based Decision Procedure for Logic of Knowing-How via Simple Plans_.  Lecture Notes in Computer Science 13040, Springer, pp. 266–283, 10.1007/978-3-030-89391-0_15.
  * [16] Yanjun Li & Yanjing Wang (2021): _Planning-based knowing how: A unified approach_.  Artificial Intelligence 296, p. 103487, 10.1016/j.artint.2021.103487.
  * [17] J McCarthy (1979): _First Order Theories of Individual Concepts and Propositions_.  Machine Intelligence 9., pp. 129–147.
  * [18] Robert C Moore (1984): _A formal theory of knowledge and action_.  Technical Report, DTIC Document.
  * [19] Pavel Naumov & Jia Tao (2017): _Together We Know How to Achieve: An Epistemic Logic of Know-How (Extended Abstract)_.  Electronic Proceedings in Theoretical Computer Science 251, pp. 441–453, 10.4204/EPTCS.251.32.
  * [20] Pavel Naumov & Jia Tao (2018): _Second-Order Know-How Strategies_.  In: Proc. of the 17th International Conference on Autonomous Agents and Multiagent Systems (AAMAS ’18).  Available at http://dl.acm.org/citation.cfm?id=3237444.
  * [21] Pavel Naumov & Jia Tao (2018): _Strategic Coalitions with Perfect Recall_.  Proceedings of Thirty-Second AAAI Conference on Artificial Intelligence, 10.1609/aaai.v32i1.11579.
  * [22] Pavel Naumov & Jia Tao (2018): _Together we know how to achieve: An epistemic logic of know-how_.  Artificial Intelligence 262, pp. 279–300, 10.1016/j.artint.2018.06.007.
  * [23] Pavel Naumov & Jia Tao (2019): _Knowing-how under uncertainty_.  Artificial Intelligence 276, pp. 41–56, 10.1016/j.artint.2019.06.007.
  * [24] Carlotta Pavese (2022): _Knowledge How_.  In Edward N. Zalta & Uri Nodelman, editors: The Stanford Encyclopedia of Philosophy, Fall 2022 edition, Metaphysics Research Lab, Stanford University.  Available at https://plato.stanford.edu/archives/fall2022/entries/knowledge-how/.
  * [25] G H Von Wright (1951): _An Essay in Modal Logic_.  North Holland, Amsterdam.
  * [26] Yanjing Wang (2015): _A Logic of Knowing How_.  In: Proceedings of LORI 2015, pp. 392–405, 10.1007/978-3-662-48561-3_32.
  * [27] Yanjing Wang (2018): _A logic of goal-directed knowing how_.  Synthese 195, p. 4419–4439, 10.1007/s11229-016-1272-0.
  * [28] Yanjing Wang (2018): _Beyond Knowing That: A New Generation of Epistemic Logics_.  In Hans van Ditmarsch & Gabriel Sandu, editors: Jaakko Hintikka on Knowledge and Game-Theoretical Semantics, Springer International Publishing, Cham, pp. 499–533, 10.1007/978-3-319-62864-6_21.
  * [29] Chao Xu, Yanjing Wang & Thomas Studer (2021): _A logic of knowing why_.  Synthese 198(2), pp. 1259–1285, 10.1007/s11229-019-02104-0.