The Local Definability of Robotic Large-Scale Knowledge Based on Splitting

Abstract

In order to reduce the computational tasks in robots with large-scale and complex knowledge, several methods of robotic knowledge localization have been proposed over the past decades. Logic is an important and useful tool for complex robotic reasoning, action planning, learning and verification. This paper uses propositional atoms in logic to describe the affecting factors of robotic large-scale knowledge. Definability in logic reasoning shows that truths of some propositional atoms are decided by other propositional atoms. Definability technology is an important method to eliminate inessential propositional atoms in robotic large-scale and complex knowledge, so the computational tasks in robotic knowledge can be completed faster. On the other hand, by applying the splitting technique, the knowledge base can be equivalently divided into a number of sub-knowledge bases, without sharing any propositional atoms with others. In this paper, we show that the inessential propositional atoms can be decided faster by the local definability technology based on the splitting method, first formed in local belief revision by Parikh in 1999. Hence, the decision-making in robotic large-scale and complex knowledge is more effective.

1. Introduction

With the rapid worldwide development of science and technology over the past decades, an increasing number of intelligent robots have been designed by scientists to help people work in hazardous environments. However, almost all robots with limited resources need to deal with a large amount of knowledge quickly, such as exchanging information with the cloud system and sharing information with neighbouring robotic companions [1, 2, 3, 4, 5]. Evidently, robots working in such special environments as underwater, mines and building sites need more knowledge than robots working in normal environments. In order to reduce the computational and storage tasks of robots, several methods of robotic knowledge localization have been proposed over the last two decades[6]. Due to the real-time knowledge-based exchange in multi-cloud robotic systems[7], each robot in multi-cloud robotic systems working in a hazardous environment needs to exchange localization knowledge with the cloud system and other cloud robots to satisfy the computational and storage tasks. The logical system is an important and useful tool for robotic reasoning, action planning, learning and verification [8, 9, 10, 11]. We use propositional atoms in logic to describe the affecting factors of robotic large-scale knowledge. In order to simplify the representation of our localization method in large-scale and complex robotic knowledge, we describe robotic knowledge by propositional logic in this paper. Definability in logic has shown that some propositional atoms are defined by other propositional atoms. Therefore, definability technology is important in the robotic knowledge field since it can eliminate inessential propositional atoms [12, 13]. At the same time, the splitting technique splits entire robotic knowledge equivalently into the same simple sub-knowledge without sharing propositional atoms with others [14]. This paper shows the definability technique based on the splitting method, first proposed by Parikh [14] in 1999 for the localization in belief revision [15, 16], which can quickly decide which are the inessential propositional atoms.

It has been widely accepted that computational intractability is also one of the major challenges for knowledge base maintenance. Most of the knowledge base maintenance operations, such as belief revision, knowledge updates and counterfactuals, are computationally intractable even if knowledge (or beliefs) is represented in propositional languages [17, 18]. More remarkably, tractability is not granted even if the language is restricted to Horn formulas, given that the inference problem with Horn clauses is decidable in deterministic polynomial time. It was shown by Eiter and Gottlob that for those formula-based operators, the complexity of knowledge base change can be co-NP-hard even in the case that the knowledge bases are represented in Horn formulas and the size of input information is bound by a constant. The main issue, as observed in [17], is that a small change to a knowledge base could have a dramatic effect on the whole knowledge base, including those items that are irrelevant to the trigger events. For instance, if a knowledge base contains $\neg p\vee (q_1\wedge \cdots \wedge q_n)$ and $\neg p$ , then a change of p from $\neg p$ to p forces the originally completely irrelevant conjunction $q_1\wedge \cdots \wedge q_n$ to become true [17].

One of the main solutions we can potentially use to tackle the above problem is the so-called relevance-based belief change, proposed by Parikh in 1999. The idea is that, whenever a belief set incurs a change, we only revise the relevant beliefs and leave the rest of the beliefs unchanged. The key technique Parikh used to implement his idea is the Finest Splitting Theorem, stating that, for any propositional theory, there is a unique finest splitting of the propositional language that splits the theory into a set of pieces, each of which is represented by a sub-language of the splitting. Based on the observation, it is possible to impose a relevance criterion on belief changes through syntactical restrictions: whenever an element of a belief set is separated through the finest language splitting from the new information, it remains an element of the revised belief set. Parikh has demonstrated that a belief change operator exists that satisfies the basic AGM postulates for belief revision and obeys the relevance criterion. However, Parikh argued that the relevance criterion conflicts conceptually with two other AGM postulates (the supplementary postulates).

Parikh's method has been developed further by [19]. Parikh's finest splitting theorem is restricted to the propositional languages with finitely many atoms. Kourousias and Makinson generalized Craig's interpolation theorem to the so-called parallel interpolation theorem, through which they successfully extended the finest splitting theorem to the infinite case. Furthermore, Kourousias and Makinson has shown that the AGM partial meet contraction applied to the finest splitting of a consistent belief set, which satisfies Parikh's relevance postulate. Although the result does not provide a representation theorem for the whole set of the AGM postulates and Parikh's relevance criterion ¹ , it tells us that the AGM partial meet operations can be naturally tuned to meet the relevance criterion.

In this paper, we demonstrate a method for making a fast decision on the essential atoms by adopting Parikh's splitting method. In the next section, we recall some preliminaries, such as parallel interpolation theorem, language splitting over propositional logic, definability and Beth's theorem. In the third section, we present some interesting results on local definability of robotic knowledge using propositional logic in order to increase the efficiency of the computational and store task. In the fourth section, we propose a conjecture to index our future computational method in local base on the basis of splitting. In the last section, we conclude our paper.

2. Preliminaries

In this section we review some preliminary knowledge for this paper. We always assume that we describe robotic knowledge with a propositional logic with a set of infinite or finite elementary literals (or atoms) and the zero-ary falsity ⊥ among the primitive connectives. We use lower-case letters $a\mathrm{,}b\mathrm{,\dots ,}u\mathrm{,}v\mathrm{,}w\mathrm{,}$ $\alpha \mathrm{,}\beta \mathrm{,}\gamma \mathrm{\dots }$ to range over formulas of classical propositional logic. A set of formulas is denoted by upper-case literals $A\mathrm{,}B\mathrm{,\dots ,}U\mathrm{,}V\mathrm{,}W\mathrm{,}\mathrm{\Gamma }\mathrm{,}\mathrm{\Delta }\mathrm{,}\mathrm{\Theta }\mathrm{\dots ,}$ reserving $\mathcal{L}$ for the set of all formulas and $PS$ for the set of all atoms (or elementary literals) of the language. We use upper case letters $X\mathrm{,}Y\mathrm{,}Z$ to range over the subset of $PS$ and lower case letters $x\mathrm{,}y\mathrm{,}z$ to range over an element of $PS$ . For any formula α, we write $E(\alpha )$ to represent the set of elementary literals occurring in α; similarly for a set of formulas. For $X\subseteq PS$ , $\mathcal{L}(X)$ stands for the sub-language generated by X, i.e., $\mathcal{L}(X)=\{\alpha \in \mathcal{L}:E(\alpha )\subseteq X\}$ . Classical logic consequence is written as ⊢ when treated as a relation over $2^{\mathcal{L}}\times \mathcal{L}$ , classical consequence operation is written as $Cn$ when treated as an operation on $2^{\mathcal{L}}$ into itself. In other words, $Cn(A)=\{\phi :A⊢\phi \}$ . The relation of classical equivalence is written as $⊣⊢$ . We say that a set K of formulas is a knowledge set or belief set if it is closed, i.e., $K=Cn(K)$ . To lighten notation, $v(A)=1$ is short for: $v(\alpha )=1$ for all $\alpha \in A$ where a valuation (or an interpretation) v is a total function from the entire set of elementary literals of the language to $\left\{\mathrm{0,1}\right\}$ , while $v(A)=0$ abbreviates: $v(\alpha )=0$ for some $\alpha \in A$ .

Formulas from $\mathcal{L}$ are interpreted in the standard way. A world (or interpretation, or valuation), where a total function is from the propositional symbols $PS$ of the language to $\left\{\mathrm{0,1}\right\}$ , is denoted by $\overrightarrow{\omega }$ and their set is denoted by Ω. Any world satisfying a given formula φ is said to be a model of φ. A world (or interpretation, or valuation), a total function from $X\subseteq PS$ to $\left\{\mathrm{0,1}\right\}$ , is called $X-$ world; their set is denoted by ${\mathrm{\Omega }}_X$ . We shall identify $\overrightarrow{\alpha }$ with the corresponding canonical conjunction of literals over X in order to simplify the notations; for instance, if $X=\left\{a\mathrm{,}b\mathrm{,}c\right\}$ and $\overrightarrow{\alpha }=(a=\mathrm{1,}b=\mathrm{0,}c=1)$ , then we also write $\overrightarrow{\alpha }=a\wedge \neg b\wedge c$ .

We recall some basic notions about essential formulas in [20]. A formula β is an essential formula of α if $\alpha ⊣⊢\beta$ and for every formula γ with $\gamma ⊣⊢\alpha$ satisfied $E(\beta )\subseteq E(\gamma )$ . It is clear that the essential formula of a formula is not unique. However, the essential formulas of a formula have the same atoms by the least atom-set theorem in [20]. We use $EE(A)$ to denote the essential atoms of set A of formulas.

2.1. Interpolation Theorem and Parallel Interpolation Theorem

In mathematical logic, Craig's interpolation theorem is an important result for the relationship between various logical theories. Roughly stated, the theorem says that if a formula φ implies a formula ψ, then there is a third formula θ, called an interpolant, such that every non-logical symbol in θ occurs both in φ and ψ, φ implies θ and θ implies ψ. The theorem was first proved for first-order logic by William Craig in [21]. Variants of the theorem hold for other logics, such as propositional logic. A stronger form of Craig's theorem for first-order logic was proved by Roger Lyndon in 1959 in [22]; the overall result is sometimes called the Craig-Lyndon theorem.

Theorem 1 (Interpolation Theorem [21]) Let $\psi \in \mathcal{L}$ and $A\subseteq \mathcal{L}$ . If $A⊢\psi$ then there is a formula ϕ such that $A⊢\varphi$ , $\varphi ⊢\psi$ and every sentence symbol that occurs in ϕ also occurs in both A and ψ.

In order to prove the finest splitting theorem in any proposition language, Kourousias and Makinson formulated Parallel Interpolation Theorem, which is a new interpolation theorem in [19].

Theorem 2 (Parallel Interpolation Theorem [19]) Let $\psi \in \mathcal{L}$ and ${\displaystyle {\cup }_{i\in I}}\left\{A_i\right\}\subseteq \mathcal{L}$ such that the atom sets $E(A_i)$ are pairwise disjoint. If ${\displaystyle {\cup }_{i\in I}}{A}_i⊢\psi$ , then for each $i\in I$ there is a formula ${\varphi }_i$ such that $A_i⊢{\varphi }_i$ , ${\displaystyle {\cup }_{i\in I}}\left\{{\varphi }_i\right\}⊢\psi$ and every sentence symbol that occurs in ${\varphi }_i$ also occurs in both A_i and ψ for all i.

2.2. Language splitting over propositional logic

It is well known that Parikh's finest splitting theorem plays the fundamental role in local belief revision. He has shown that there was a unique finest splitting for each set of formulas in finite propositional language in [14]. Kourousias and Makinson extended the result to any language that contains an infinite number of propositional variables in [19]. It allows us to carve up a set of formulas into disjoint pieces.

Definition 1 (Splitting formulas) Let $E=\{E_i{\}}_{i\in I}$ be any partition of $PS$ , i.e., a partition of atoms of language $\mathcal{L}$ . $E$ is said to be a splitting of a set, K, of formulas if there is a family ${\left\{B_i\right\}}_{i\in I}$ of formulas, such that ${\displaystyle {\cup }_{i\in I}}\left\{B_i\right\}⊣⊢K$ and $E(B_i)\subseteq E_i$ for all $i\in I$ . In such a case, we said that ${\left\{B_i\right\}}_{i\in I}$ be a splitting witness of K.

We will use a graph to describe the splitting of a set of formulas in Fig 1.

Figure 1.

Graph of Splitting (|I| =2)

Example 1 Assume set $\left\{p\mathrm{,}q\mathrm{,}r\right\}$ be entire propositional symbols of the proposition language. Let $A=Cn(\{p\mathrm{,}p\to q\mathrm{,}p\to r\})$ . Then $\left\{p\mathrm{,}q\mathrm{,}r\right\}$ ( $\left\{\right\{p\mathrm{,}r\left\}\mathrm{,}\right\{q\left\}\right\}$ , $\left\{\right\{p\left\}\mathrm{,}\right\{q\mathrm{,}r\left\}\right\}$ , $\left\{\right\{r\left\}\mathrm{,}\right\{p\mathrm{,}q\left\}\right\}$ , $\left\{\right\{p\left\}\mathrm{,}\right\{r\left\}\mathrm{,}\right\{q\left\}\right\}$ ) is the splitting of A under the language, since $A⊣⊢\{p\mathrm{,}p\to q\mathrm{,}p\to r\}$ ( $A⊣⊢\{q\mathrm{,}p\mathrm{,}p\to r\}$ , $A⊣⊢\{p\mathrm{,}q\mathrm{,}q\to r\}$ , $A⊣⊢\{r\mathrm{,}p\mathrm{,}p\to q\}$ , $A⊣⊢\left\{p\mathrm{,}q\mathrm{,}r\right\}$ ). Moreover, $\{p\mathrm{,}p\to q\mathrm{,}p\to r\}$ ( $\{q\mathrm{,}p\mathrm{,}p\to r\}$ , $\{p\mathrm{,}q\mathrm{,}q\to r\}$ , $\{r\mathrm{,}p\mathrm{,}p\to q\}$ , $\left\{p\mathrm{,}q\mathrm{,}r\right\}$ ) is splitting witness of $\left\{p\mathrm{,}q\mathrm{,}r\right\}$ ( $\left\{\right\{p\mathrm{,}r\left\}\mathrm{,}\right\{q\left\}\right\}$ , $\left\{\right\{p\left\}\mathrm{,}\right\{q\mathrm{,}r\left\}\right\}$ , $\left\{\right\{r\left\}\mathrm{,}\right\{p\mathrm{,}q\left\}\right\}$ , $\left\{\right\{p\left\}\mathrm{,}\right\{r\left\}\mathrm{,}\right\{q\left\}\right\}$ ) splitting of A.

The example shows that a splitting witness of K is not unique and there are many splittings for any set of formulas. The finest splitting draws researchers' attention generally. In other words, people often hope to split a set of formulas as fine as possible such that essential relation matters in same piece possibly. Hence we will recall the fineness of splitting.

Assume that $E=\{E_i{\}}_{i\in I}$ and $F=\{F_j{\}}_{j\in J}$ are two splittings of a set K of formula. Let R_E and R_F be the corresponding equivalence relations of $E$ and $F$ , respectively. We say that $E$ is at least as fine as $F$ , written by $E\le F$ , if $R_E\subseteq R_F$ .

Kourousias and Makinson proved the following finest splitting theorem based on the Parallel Interpolation Theorem in the last subsection:

Theorem 3 (Finest splitting over formula[19]). Every set K of formulas has a unique finest splitting for a given propositional language.

The theorem shows that for every set K of formulas under any finite or infinite proposition language has a unique finest splitting. When discussing the finite proposition language, the results are clear, since we can check all atom subsets. Although with the elementary method, checking all atom subsets, fails when the language is infinite, it also holds when we use the Parallel Interpolation Theorem proposed in [19].

Example 2 Assume as Example 1. $\left\{\right\{p\left\}\mathrm{,}\right\{r\left\}\mathrm{,}\right\{q\left\}\right\})$ is the finest splitting of set A of formulas under the language.

It is obvious that the splitting witness of K is not unique, but they are equivalent. The computation of the finest splitting of a set of formulas refers to [23].

We can know $\{E(A_1)\mathrm{,\dots ,}E(A_n)\}$ is a partition of the set $PS$ of atoms of language $\mathcal{L}$ if $E=\{E_i{\}}_{i\in I}$ is a splitting of a set A of formulas. But ${\left\{A_i\right\}}_{i\in I}$ is not the splitting witness of A by Definition 1. We will give an example to show the result, as follows:

Example 3 Let set $\left\{p\mathrm{,}q\mathrm{,}r\right\}$ be entire propositional symbols of the proposition language and $A=Cn(\{p\mathrm{,}p\to q\})$ . Then set $\{p\mathrm{,}q\mathrm{,}\neg \perp \}$ of formulas is the splitting witness of $\left\{\right\{p\left\}\mathrm{,}\right\{q\left\}\mathrm{,}\right\{r\left\}\right\}$ finest splits A . However, $\left\{\right\{E(p)\left\}\mathrm{,}\right\{E(q)\left\}\mathrm{,}\right\{E(\neg \perp )\left\}\right\}$ , i.e., $\left\{\right\{p\left\}\mathrm{,}\right\{q\}\mathrm{,}\varnothing \}$ is not the finest splitting of A under the language ${\mathcal{L}}_{\left\{p\mathrm{,}q\mathrm{,}r\right\}}$ .

However, the result holds when we revise only the language we discussed.

Proposition 1 Let $A_1\mathrm{,}{A}_2\mathrm{,\dots ,}{A}_n\mathrm{,}A\subseteq \mathcal{L}$ with $E(A_i)\cap E(A_j)=\varnothing$ for $i\ne j$ and ${\displaystyle {\cup }_{i=1}^n}{A}_i⊣⊢A$ with $⊬A_i$ and $A_i⊬\mathcal{L}$ . Then $\{EE(A_1)\mathrm{,\dots ,}EE(A_n)\}$ is a partition of $EE(A)$ , the set of essential atoms of A, if and only if $\left\{\right\{EE(A_i{)\}}_{i\in I}\mathrm{,}\{x_i{\}}_{x_i\in E(A)-EE(A)}\}$ is the finest splitting of A under language ${\mathcal{L}}_A$ . Moreover, $\{EE(A_1)\mathrm{,\dots ,}EE(A_n)\}$ is the finest partition of $EE(A)$ if and only if ${\{E(A_i)\}}_{i\in I}$ is the finest splitting of A under language ${\mathcal{L}}_{EE(A)}$ .

Proof: The proof of this proposition is clear when we focus the non-essential atoms of a set of formulas in a given propositional language by the definition of splitting and essential atoms of language.

2.3. Definability and Beth's theorem

Definability is an important concept and tool in logic reasoning. We will first recall the definition of two forms of definability:

Definition 2 (Implicit Definability). Let $A\subseteq \mathcal{L}$ , $X\mathrm{,}Y\subseteq PS$ and $y\in PS$ .

1. A implicitly defines y in terms of X if and only if $\forall \overrightarrow{\alpha }\in {\mathrm{\Omega }}_X$ , $\overrightarrow{\alpha }\wedge A\models y$ or $\overrightarrow{\alpha }\wedge A\models \neg y$ .

2. A implicitly defines Y in terms of X if and only if A implicitly defines y in terms of X for every $y\in Y$ .

Definition 3 (Explicit Definability; Definition of a propositional symbol). Let $A\subseteq \mathcal{L}$ , $X\subseteq PS$ and $y\in PS$ . A explicitly defines y in terms of X if and only if there exists a formula ${\mathrm{\Phi }}_X\in {\mathcal{L}}_X$ s.t. $A\models {\mathrm{\Phi }}_X\iff y$ . In such a case, ${\mathrm{\Phi }}_X$ is called a definition of y on X in A.

What is the natural relationship between the two definitions of definability? Beth's definability theorem in mathematical logic is a well-known result that connects implicit definability of a property to its explicit definability; specifically, the theorem states that the two senses of definability are equivalent.

Theorem 4 (Propositional projective Beth's theorem [24]). Let $A\subseteq \mathcal{L}$ , $X\mathrm{,}Y\subseteq PS$ and $y\in PS$ . A explicitly defines y in terms of X if and only if A implicitly defines y in terms of X.

Using Definition 2 and Definition 3, the following two results, which we will use in the next section, are evident (for details please refer to [13]).

Proposition 2 Let $A\mathrm{,}\mathrm{\Gamma }\subseteq \mathcal{L}$ , $X\mathrm{,}Z\subseteq PS$ and $y\in PS$ .

1. if A implicitly/explicitly defines y in terms of X and $X\subseteq Z$ , then A implicitly/explicitly defines y in terms of Z, and

2. if A implicitly/explicitly defines y in terms of X and $\mathrm{\Gamma }⊢A$ , then Γ implicitly/explicitly defines y in terms of X.

3. The Local Definability Theorem on Knowledge, Based on Splitting

In the section, we will show some interesting results about the localization of robotic knowledge by propositional definability.

3.1. Implicit local definability theorem, based on splitting

Lemma 1 Let $X\subseteq PS$ and $y\in PS$ . Let ${\left\{E_i\right\}}_{i\in I}$ be the finest splitting of a set A of formulas and the family $\left\{A_1\mathrm{,}{A}_2\mathrm{,\dots ,}{A}_n\right\}$ be a splitting witness of A in ${\mathcal{L}}_{PS}$ . If A implicitly defines y in terms of X, then A_i implicitly defines y in terms of $X\cap E(A_i)$ , where $y\in E_i$ . Moreover, A implicitly defines y in terms of X if and only if A_i implicitly defines y in terms of $X\cap E(A_i)$ where $y\in E_i$ .

Proof: A implicitly defines y in terms of X whenever A_i implicitly defines y in terms of $X\cap E(A_i)$ , where $y\in E_i$ because of Proposition 2, $A⊢A_i$ and $X\cap E(A_i)\subseteq X$ . We then need only to prove if A implicitly defines y in terms of X, then A_i implicitly defines y in terms of $X\cap E(A_i)$ , where $y\in E_i$ .

Let any $\overrightarrow{\beta }\in {\mathrm{\Omega }}_{X\cap E(A_i)}$ and for any extension $\overrightarrow{\alpha }\in {\mathrm{\Omega }}_X$ of $\overrightarrow{\beta }$ . By the definition of definability and A implicitly defines y in terms of X, we know $\overrightarrow{\alpha }\wedge A⊢y$ or $\overrightarrow{\alpha }\wedge A⊢\neg y$ . Without loss of generality, we assume that $\overrightarrow{\alpha }\wedge A⊢y$ . Let $\overrightarrow{\alpha }=L_1\wedge L_2\wedge \mathrm{\dots }\wedge L_m$ and $A_j^{\prime }=A_j\cup \{L_i:E(L_i)\in E(A_j)\}$ . Evidently, we then have $\overrightarrow{\beta }=\{L_i:E(L_i)\in E(A_i)\}$ by $\overrightarrow{\alpha }$ is an extension of $\overrightarrow{\beta }$ and still know $A_1^{\prime }\mathrm{,}{A}_2^{\prime }\mathrm{,\dots ,}{A}_n^{\prime }⊢y$ by $\overrightarrow{\alpha }\wedge A⊢y$ and $\left\{A_1\mathrm{,}{A}_2\mathrm{,\dots ,}{A}_n\right\}⊣⊢A$ . Hence, we know that $A_i^{\prime }⊢y$ by parallel interpolation theorem and atom $y\in E(A_i)$ . Hence, $A_i\wedge \overrightarrow{\beta }⊢y$ . Moreover, A_i implicitly defines y in terms of $X\cap E(A_i)$ , since $\overrightarrow{\beta }=\{L_i:E(L_i)\in E(A_i)\}$ .

Theorem 5 (Localization of Implicit Definability Theorem) Let $X\subseteq PS$ and $y\in PS$ , ${\left\{E_i\right\}}_{i\in I}$ be the finest splitting of a set A of formulas and the family $\{A_i:i\in I\}$ be a splitting witness of A in ${\mathcal{L}}_{PS}$ . A implicitly defines y in terms of X if and only if A_i implicitly defines y in terms of $X\cap E_i$ , where $y\in E_i$ .

Proof: It is evident that the proof holds up by using Lemma 1 repeatedly.

We will use a graph to describe the equal relations between implicit definition and localization of definition on atoms over the finest splitting in Fig 2.

Figure 2.

The Equation Graph about Global-Local Definition on atom over the Finest Splitting

Lemma 2 Let $X\mathrm{,}Y\subseteq PS$ , ${\left\{E_i\right\}}_{i\in I}$ be the finest splitting of a set A of formulas and the family $\{A_i:i\in I\}$ be a splitting witness of A in ${\mathcal{L}}_{PS}$ . $X\subseteq {\displaystyle {\cup }_i}E(A_i)$ and A implicitly defines Y in terms of X if and only if A_i implicitly defines Y_i in terms of X_i for any i where Y_i is a partition of Y and $X_i=X\cap E(A_i)$ .

Proof: From right to left: Let A_i implicitly define Y_i in terms of X_i for any i and $Y_i=Y\cap E(A_i)$ is the partition of Y. Then A_i implicitly defines y in terms of X_i for any $y\in Y_i$ . By Theorem 5 and $X_i=X\cap E(A_i)$ is the partition of X, we have A implicitly defines Y in terms of X. Hence A implicitly defines Y_i in terms of X. Moreover, A implicitly defines Y in terms of X.

From left to right: Let $X\subseteq {\displaystyle {\cup }_i}E(A_i)$ and A implicitly define Y in terms of X. We know that A implicitly defines y in terms of X for any $y\in Y$ . By Lemma 1, we have A_i implicitly defines Y in terms of $X\cap E(A_i)$ where $y\in E_i$ . Let $X_i=X\cap E(A_i)$ . Clearly it is the partition of X by $X\subseteq {\displaystyle {\cup }_i}E(A_i)$ and A_i implicitly defines Y in terms of X_i. Let $Y_i=\{y\in Y:A_i$ implicitly define y in terms of $X_i\}$ . Clearly it is the partition of Y.

The Lemma is not suitable for all conditions because $X\subseteq {\displaystyle {\cup }_i}E(A_i)$ . Hence we show that the following theorem does not satisfy the condition. The proof is easy when we deal with the splitting witness ${\left\{A_i\right\}}_{i\in I}$ .

Theorem 6 (Localization Implicit Definability Theorem over set of propositional symbols) Let $X\mathrm{,}Y\subseteq PS$ , ${\left\{E_i\right\}}_{i\in I}$ be the finest splitting of a set A of formulas and the family $\{A_i:i\in I\}$ be a splitting witness of A in $\mathcal{L}$ . A implicitly defines Y in terms of X if and only if A_i implicitly defines Y_i in terms of X_i for any i where $\{Y_i:i\in I\}$ is a partition of Y and $X_i=X\cap E_i$ .

We will use a graph to describe the equal relations between implicit definition and localization of definition on set over the finest splitting in Fig 3.

Figure 3.

The Equation Graph about Global-Local Definition on set over the Finest Splitting

3.2. Explicit local definability theorem based on splitting

Lemma 3 Let $X\subseteq PS$ and $y\in PS$ . Let ${\left\{E_i\right\}}_{i\in I}$ be the finest splitting of a set A of formulas and the family $\{A_i:i\in I\}$ be a splitting witness of A in ${\mathcal{L}}_{PS}$ . If A explicitly defines y in terms of X, then A_i explicitly defines y in terms of $X\cap E(A_i)$ where $y\in E_i$ . Moreover, A explicitly defines y in terms of X if and only if A_i explicitly defines y in terms of $X\cap E(A_i)$ where $y\in E_i$ .

Proof: A explicitly defines y in terms of X whenever A_i explicitly defines y in terms of $X\cap E(A_i)$ where $y\in E_i$ because of Proposition 2, $A⊢A_i$ and $X\cap E(A_i)\subseteq X$ . We then need only to prove if A explicitly defines y in terms of X, then A_i explicitly defines y in terms of $X\cap E(A_i)$ where $y\in E_i$ .

By A explicitly defines y in terms of X and Beth's Theorem, we have A implicitly defines y in terms of X. We then know that A_i implicitly defines y in terms of $X\cap E(A_i)$ where $y\in E_i$ by Lemma 1. Hence A_i explicitly defines y in terms of $X\cap E(A_i)$ where $y\in E_i$ by Beth's Theorem.

We can prove the Lemma directly without using the results in Lemma 1. However, it is complex.

Theorem 7 (Localization Explicit Definability Theorem over set of propositional symbols) Let $X\mathrm{,}Y\subseteq PS$ , ${\left\{E_i\right\}}_{i\in I}$ be the finest splitting of a set A of formulas and the family $\{A_i:i\in I\}$ be a splitting witness of A in ${\mathcal{L}}_{PS}$ . $X\subseteq {\displaystyle {\cup }_i}E(A_i)$ and A explicitly defines Y in terms of X if and only if A_i explicitly defines Y_i in terms of X_i for any i where ${\{X_i=X\cap E(A_i)\}}_{i\in I}$ and ${\left\{Y_i\right\}}_{i\in I}$ are the partition of X and Y.

Proof: It is evident that the proof uses Lemma 3 repeatedly.

The figure 2 also shows the global-local relation on explicit definability.

Lemma 4 Let $X\mathrm{,}Y\subseteq PS$ , let ${\left\{E_i\right\}}_{i\in I}$ be the finest splitting of a set A of formulas and the family $\{A_i:i\in I\}$ be a splitting witness of A in ${\mathcal{L}}_{PS}$ . $X\subseteq {\displaystyle {\cup }_i}E(A_i)$ and A explicitly defines Y in terms of X if and only if A_i explicitly defines Y_i in terms of X_i for any i where $\{Y_i:i\in I\}$ is a partition of Y and $X_i=X\cap E(A_i)$ .

Proof: From right to left: Let A_i explicitly define Y_i in terms of X_i for any i and $Y_i=Y\cap E(A_i)$ is the partition of Y. Then A_i explicitly defines y in terms of X_i for any $y\in Y_i$ . By Theorem 7 and $X_i=X\cap E(A_i)$ is the partition of X, we have A explicitly defines Y in terms of X. Hence A explicitly defines Y_i in terms of X. Moreover, A explicitly defines Y in terms of X.

From left to right: Let $X\subseteq {\displaystyle {\cup }_i}E(A_i)$ and A explicitly define Y in terms of X. We know that A explicitly defines y in terms of X for any $y\in Y$ . By Theorem 1, we have A_i explicitly defines Y in terms of $X\cap E(A_i)$ where $y\in E_i$ . Let $X_i=X\cap E(A_i)$ . Clearly it is the partition of X by $X\subseteq {\displaystyle {\cup }_i}E(A_i)$ and A_i explicitly defines Y in terms of X_i. Let $Y_i=\{y\in Y:A_i$ explicitly define y in terms of $X_i\}$ . Clearly it is the partition of Y.

The Lemma is not suitable for all conditions because $X\subseteq {\displaystyle {\cup }_i}E(A_i)$ . Therefore, we show the following theorem to miss the condition. The proof is easy when we deal with the splitting witness ${\left\{A_i\right\}}_{i\in I}$ .

Theorem 8 (Localization Explicit Definability Theorem over set of propositional symbols) Let $X\mathrm{,}Y\subseteq PS$ , Let ${\left\{E_i\right\}}_{i\in I}$ be the finest splitting of a set A of formulas and the family $\{A_i:i\in I\}$ be a splitting witness of A in ${\mathcal{L}}_{PS}$ . A explicitly defines Y in terms of X if and only if A_i explicitly defines $\{Y_i:i\in I\}$ in terms of X_i for any i where Y_i is a partition of Y and $X_i=X\cap E_i$ .

The figure 3 also shows the global-local relation on explicit definability for the set.

4. Related and Future Work

In mathematical logic, Beth definability connects the implicit definability of a property and its explicit definability [12]. Specifically, the theorem proposed by Evert Willem Beth states that the two senses of definability are equivalent [24]. It is a well-known technology in logic that definability can reduce irrelevant factors in knowledge base presented by logic. There has been a lot of literature on Beth definability in logic and related fields [12, 25, 11, 13, 26]. In this paper, we first split robotic knowledge base into the finest robotic sub-knowledge base without common propositional atoms each other. We then proposed the relation of definability of robotic knowledge base and robotic sub-knowledge base. New splitting technology was introduced into definability and given some interesting results on the computational task. To our best knowledge, there is no previous literature related to our methods.

Parikh reviews the relationship between interpolation theorem and definition in [13]. Interpolation theorem in mathematical logic was first proved for first-order logic by William Craig in 1957 [21, 12] and is a study on the relationship between various logical theories. Craig's interpolation has many applications, including consistency proofs, model checking, proofs in modular specifications and modular ontologies [11].

Kourousias and Makinson's framework was built upon classical propositional logic. An open question was posted in [19]: How far can the results be established for sub-classical (e.g., intuitionistic) consequence relations or supra-classical ones? This is by no means a trivial question, because Kourousias and Makinson's proof of the Finest Splitting Theorem is based on Craig's Interpolation Theorem, which fails in many non-classical logics [12]. In addition, Parikh's relevance criterion is a syntactical requirement, which is sensitive to variations of languages.

Parikh also discusses the relationship between interpolation theorem and parallel interpolation theorem. A natural question was proposed as follows [13]:

Question:: Is there also a parallel counterpart to the Beth definability theorem?

In the future we will continue to discuss Parikh's open problem.

Now we simply discuss an interesting result in the base computation proposed by [25] using localization method based on splitting technology proposed by Parikh [14]. Because of the equivalence between implicitly defines and explicitly defines, we now use $X{⊑}_{A}Y$ to represent A implicit/explicitly defines Y in terms of X. We will first recall the definition of base about definability in [25].

Definition 4 (Base) Let $A\in \mathcal{L}$ and $X\mathrm{,}Y\subseteq PS$ . X is a minimal defining family, for short a base, for Y w.r.t. A, if and only if $X{⊑}_{A}Y$ holds and there is no proper subset $X^{\prime }$ of X such that $X^{\prime }{⊑}_{A}Y$ . The set of all bases for Y w.r.t. A is denoted by $B{S}_A(Y)$ .

We will show the relation between the set of bases over an entire set of atoms and the set of bases for all its elements in [25].

Lemma 5 Let $A\in \mathcal{L}$ and $Y=\left\{y_1\mathrm{,}{y}_2\mathrm{,\dots ,}{y}_p\right\}\subseteq PS$ .

$B{S}_A(Y)=min\left(\left\{{\displaystyle \underset{i=1}{\overset{p}{\cup }}}{B}_i|B_i\in B{S}_A\left(\left\{y_i\right\}\right)\right\}\mathrm{,}\subseteq \right)\mathrm{.}$

By the lemma, we can propose a conjecture about the computation of base by all atoms set over the relevant sub-knowledge base of the sub-language. This will reduce the computational task after the splitting of the knowledge base.

Conjecture 1 Let $A\in \mathcal{L}$ and $Y=\left\{y_1\mathrm{,}{y}_2\mathrm{,\dots ,}{y}_p\right\}\subseteq PS$ . If ${\left\{E_i\right\}}_{i\in I}$ is the (finest) splitting of A, i.e., $A_1\mathrm{,}{A}_2\mathrm{,\dots ,}{A}_n⊣⊢A$ , $E\left(A_i\right)\cap E\left(A_j\right)=\varnothing \hspace{0.17em}\hspace{0.17em}\hspace{0.17em}\mathrm{for}\hspace{0.17em}any\hspace{0.17em}\hspace{0.17em}i\ne j$ and $E(A_i)\subseteq E_i$ for all $i\in I$ then

$B{S}_A(Y)=min\left(\left\{{\displaystyle \underset{i=1}{\overset{p}{\cup }}}{B}_i|B_i\in B{S}_{A_i}\left(\left\{y_i\right\}\right)\right\}\mathrm{,}\subseteq \right)\mathrm{.}$

In the future, we will continue to discuss the base computation using the localization method based on Parikh's splitting technology.

5. Conclusion

Recently, an increasing number of robots with limited resources for computation and storage need to exchange vast common knowledge using the cloud system and share external environment information quickly with their neighbouring robotic companions. Evidently, it is impossible for all robots to receive knowledge from the cloud system and neighbour robotic companions in real time. Hence, we can only exchange relevant and local knowledge that comes from large-scale and complex knowledge between intelligent robots and the cloud system or neighbour robotic companions. As for the localization of intelligent robots, especially cloud robots or robots working in special environments such as underwater, mines and building sites, knowledge-base change is more important. In order to decide quickly on the definability in propositional logic, we demonstrate two interesting results on the local definability of robotic large-scale and complex knowledge, which uses propositional logic by computing the sub-language's knowledge based on Parikh's splitting method.