In Artificial Intelligence, multi agent systems constitute an interesting typology of society modeling, and have vast fields of application. Logic is often used to model such kind of systems as it is provides explainability and verifiabilty. In this paper1 we talk about the cognitive aspect of autonomous systems, and we propose a particular logical framework (Logic of “Inferable” (L-DINF)) which introduces aspects of self-awareness, which is fundamental for reaching explainability. In fact, the proposed logic allow agents to reason about actions that they are able to perform, which is the logical inference chain that allows each action to be performed, and in how many steps. We consider resource-bounded agents, that can execute an action only if possessing the necessary resources to do so.
[
The logic of inference stems from Vela´zquez-Quesada [16] and the logical system
DES4n by Duc [
Our constructive approach to explicit beliefs also distinguishes L-INF from Active
logics [
For our logic we we drew inspiration from the approach of Self-aware
computing: quoting [15], Self-aware and self-expressive computing describes an emerging
paradigm for systems and applications that proactively gather information; maintain
knowledge about their own internal states and environments; and then use this
knowledge to reason about behaviors, revise self-imposed goals, and self-adapt.: : : Systems
that gather unpredictable input data while responding and self-adapting in uncertain
environments are transforming our relationship with and use of computers. Reporting
from [
The introspective abilities of our agents as described in the proposed logic are limited. I.e., an agent is aware of the actions it can execute, and how many steps are needed to reach an objective. Nonetheless, our logic constitutes a first step towards self-aware agents.
The paper is organized as follows. In Section 2 we introduce the Syntax and the Semantic of our logic. In Sections 3 we show the axiomatization and the proof of soundness, instead in 4 we show the proof of strongl completeness. In Section 5 we propose a brief discussion on future work and conclude. 2
L-DINF is a logic which consists of a static component and a dynamic one. The static component, called L-INF, is a logic of explicit beliefs and background knowledge. The dynamic component, called L-DINF, extends the static one with dynamic operators capturing the consequences of the agents’ inferential operations on their explicit beliefs as well as a dynamic operator capturing what an agent can conclude by performing some inferential operation in her repertoire. 2.1
Assume a countable set of atomic propositions Atm = fp; q; : : :g. By P rop we denote the set of all propositional formulas, i.e. the set of all Boolean formulas built out of the set of atomic propositions Atm. A subset AtmA of the atomic propositions represent the actions that an agent can perform.
The language of L-DINF, denoted by LL-DINF , is defined by the following grammar in Backus-Naur form:
::= `('; ) j \('; ) j #('; ) ; ::= p j exec( ) j :' j ' ^ j B ' j K ' j
[ ]' j ' j do( A) j can do( A) where the language of inferential actions of type is denoted by LACT (and a finite set of inferential actions X stems from LACT), and p ranges over Atm. Notice the expression do( A), where it is required that A 2 AtmA. This expression indicates actual execution of action A. In fact do is not axiomatized, as it is what has been called in [18] a semantic attachment, i.e., a procedure which connects an agent with its external environment in a way that is unknown at the logical level. can do( A), where again A 2 AtmA, is a reserved syntax that, as seen later, will allow an agent to reason about its own capabilities.
Obviously the static part, L-INF, has the same definition save removing the
inferential actions. The other Boolean constructions are defined from p, : and ^ in the
standard way. The formula B ' is read “the agent explicitly believes that ' is true” or,
more shortly, “the agent believes that ' is true”. Explicit beliefs are accessible in the
working memory and are the basic elements of the agents’ reasoning process,
according the logic of local reasoning by Fagin & Halpern [
Unlike explicit beliefs, background knowledge is assumed to satisfy ‘omniscience’ principles like closure under conjunction and known implication, closure under logical consequence and introspection. Specifically, K is nothing but the well-known S5 operator for knowledge widely used in computer science. The fact that background knowledge is closed under logical consequence is justified by the fact that we conceive it as a kind of deductively closed belief base. Specifically, we assume background knowledge to include all facts that the agent has stored in her long-term memory (LTM), after having processed them in her working memory (WM), as well as all logical consequences of these facts.
The formula [ ]' should be read “' holds after the inferential operation (or
inferential action) is performed by the agent”. Borrowing from and extending [
A. In fact, we assume that when inferring do( A) the action is actually executed, and the corresponding belief asserted, possibly augmented with a time-stamp. Actions are supposed to succeed by default, in case of failure a corresponding failure event will be perceived by the agent. Therefore, the occurrence of physical actions (performed via the procedure do) is recorded through the formation of new beliefs.
The atomic formulas exec( ) have to be read “ is an inferential action that the agent can perform”, meaning one of the above.
Remark 2. Specifying executability of actions pertains to the fact that we intend to consider agents with limited resources. Specific instances ' OP1 where one of the two formulas is an action may or may not be executable depending upon the agent having the necessary resources for performing that action. Executability is defined for inferential actions because such actions, if executable, may enact ‘physical’ actions. Remark 3. Explainability in our approach can be directly obtained from proofs. If, for instance, the user asks an explanation of why the action A has been performed, the system can respond by exhibiting the proof that has lead to A, of the form (exec('1OP1 1) ^ ('1OP1 1)) ^ : : : ^ (exec('nOPn A) ^ 'N OPn do( A)) where each OPi is one of the (mental) actions discussed above. The proof can possibly be translated into natural language, and declined either top-down or bottom-up.
Finally, the formula ' has to be read “the agent can ensure ' by executing some inferential action in her repertoire”. The interesting aspect of our language is that, at least in perspective (as the formalization is not complete yet), it allows us to express the concept of “being able to infer ' in k inferential steps”. Specifically, let us inductively define: 0' = ', k+1 = k'. The formula kB ' represents the fact that the agent is capable of inferring ' in k steps. 2.2
The main semantics notions are outlined in the following definition of L-INF model which provides the basic components for the interpretation of the static version of the logic: Definition 1. We define a model to be a tuple M = (W; N; R; E; V ) where: – W is a set of worlds or situations; – R W W is an equivalence relation on W ; – N : W ! 22W is a neighborhood function such that for all i 2 Agt, w; v 2 W and X W : (C1) if X 2 N (w) then X R(w), (C2) if wRv then N (w) = N (v); – E : W ! 2LACT is an executability function such that for all w; v 2 W : (D1) if wRv then E(w) = E(v); – V : W ! 2Atm is a valuation function.
For every w 2 W , R(w) = fv 2 W j wRvg identifies the set of situations that the agent considers possible at world w. In cognitive terms, R(w) can be conceived as the set of all situations that the agent can retrieve from her long-term memory and reason about them. More generally, R(w) is called the agent’s epistemic state at w.
For every w 2 W , N (w) defines the set of all facts that the agent explicitly believes at world w, a fact being identified with a set of worlds. More precisely, if A 2 N (w) then, at world w, the agent has the fact A under the focus of her attention and believes it. N (w) is called the agent’s explicit belief set at world w.
E(w) is the set of mental operations that the agent can execute at w, as it has the resources to do so.
Constraint (C1) just means that an agent can have explicit in her mind only facts which are compatible with her current epistemic state. According to Constraint (C2), if world v is compatible with the agent’s epistemic state at world w, then the agent should have the same explicit beliefs at w and v. Constraint (D1) means that an agent always knows the actions which she can perform and those that she cannot.
Truth conditions of L-DINF formulas are inductively defined as follows: for a model M = (W; N; R; E; V ), a world w 2 W , a formula ' 2 LL-INF , and an action , we define the truth relation M; w j= ' and a new model M by simultaneous recursion on and ' as follows. Below, we write
k'kwM = fv 2 W : wRv and M; v j= 'g whenever M; v j= ' is well-defined. Then, we set: – M; w j= p iff p 2 V (w) – M; w j= exec( ) iff 2 E(w) – M; w j= :' iff M; w 6j= ' – M; w j= ' ^ iff M; w j= ' and M; w j=
M – M; w j= B ' iff jj'jjw 2 N (w) – M; w j= K ' iff M; v j= ' for all v 2 R(w) – M; w j= [ ]' iff M ; w j= ' – M; w j= ' iff 9 2 E(w) s.t. M ; w j= ' where M
= (W; N ; R; E; V ) and N is defined as follows. For w 2 W , set
We write j=L-DINF ' to denote that ' is true in all worlds w of every L-DINF model M .
8N (w) [ fjj jjw g
M > N #( ; )(w) = < >:N (w) >:N (w) >:N (w) 8N (w) [ fjj ^ jjw g
M > N \( ; )(w) = < 8N (w) [ fjj jjw g
M > N `( ; )(w) = < if M; w j= B K ( ! ) otherwise
^ if M; w j= B B otherwise
^ if M; w j= B B ( ! ) otherwise ^ Property 1. As consequence of previous definitions we have the following: – j=L-INF (K(' ! )) ^ B ') ! [#('; )] B .
Namely, if an agent has ' as one of its beliefs and has K(' ! ) in its background knowledge, then as a consequence of the action #('; ) the agent starts believing ; – j=L-INF (B' ^ B ) ! [\('; )]B(' ^ ).
Namely, if an agent has ' and as beliefs, then as a consequence of the action \('; ) the agent i starts believing ' ^ ; – j=L-INF (B(' ! )) ^ B ') ! [`('; )] B . Namely, if an agent has ' as one of its beliefs and has B(' ! ) in its working memory, then as a consequence of the action `('; ) the agent starts believing ; 3
The L-INF and L-DINF axioms are: 1. (K ' ^ K(' ! )) ! K ; 2. K ' ! '; 3. :K (' ^ :'); 4. K ' ! K K '; 5. :K ' ! K :K '; 6. B ' ^ K (' $ ) ! B ; 7. B ' ! K B '; 8. K'' ; 9. [ ]p $ p; 10. [ ]:' $ :[ ]'; 11. exec( ) ^ [ ]' ! '; 12. exec( ) ! K (exec( )); 13. [ ](' ^ ) $ [ ]' ^ [ ] ; 14. [ ]K ' $ K ([ ]'); 15. [#('; )]B $ B ([#('; )] ) _ ((B ' ^ K (' ! )) ^ K ([#('; )] $ )); 16. [\('; )]B $ B ([\('; )] ) _ ((B ' ^ B ) ^ K ([\('; )] $ (' ^ )); 17. [`('; )]B $ B ([`('; )] ) _ ((B ' ^ B (' ! )) ^ B ([`('; )] $ )); 18. '$'[ = ] ;
$
19. p ! p;
20. (' ^ ) ! ' ^ ;
21. ' ! ';
22. B ' ! B ';
23. K ' ! K '.
24. ([ ]') ! 1'.
25. ([
This with the exception of the last axioms concerning k that, in this formal setting,
cannot be generalized, as we do not have the equivalence of “transitive closure”.
Therefore, in the present version one has to establish the maximum number of execution step
to be considered (in the above formulation, just three steps) and write the
corresponding axioms. These axioms are however of great practical utility for a self-aware agent:
if the agent is able to prove k ', where ' = can do( A), then it becomes aware of
being able to perform a certain action in k steps. As seen in the axioms, k can do( A)
is proved by finding a sequence of mental actions ([
A is eventually performed. This at the condition that all the [ i]’s are executable in the agent’s present state. 4
For the proof that L-INF is strongly complete we limit ourselves, as we do not consider the operator, that is still an experimental feature that we aim to better formalize in future work. We can achieve the proof by means of a standard canonical model argument. Definition 2. The canonical L-INF model is a tuple Mc = hWc; Nc; Rc; Vc; Eci where: – Wc is the set of all maximal consistent subsets of LL-INF; – For every w 2 Wc, wRcv if and only if K ' 2 w iff K ' 2 v; i.e., Rc is an equivalence relation on knowledge; as before, we define Rc(w) = fv 2 Wc j wRcvg. – For w 2 Wc, ' 2 LL-INF we define A'(w) = fv 2 Rc(w) j ' 2 vg. Then, we put Nc(w) = fA'(w) j B ' 2 wg. – Vc is a valuation function defined as before; – EC is the executable function defined as before.
There are the following immediate consequences of the above definition: if w 2 Wc then – given ' 2 LL-INF, it holds that K ' 2 w if and only if 8v 2 Wc such that wRcv we have ' 2 v; – for ' 2 LL-INF, if B ' 2 w and wRcv then B ' 2 v; – for 2 Ec(w), if wRcv then 2 Ec(v).
Thus, Rci -related worlds have the same knowledge and Nc-related worlds have the same beliefs, i.e. there can be Rci -related worlds with different beliefs. The following results hold: Lemma 1. For all w 2 Wc and B '; B 2 LL-INF, if B ' 2 w but B follows that there exists v 2 Rc(w) such that ' 2 v $ 62 v. 62 w, it Proof. Let w 2 Wc and '; be such that B ' 2 w and Bi 2= w. Assume now that for every v 2 Rc(w) we have ' 2 v, 2 v or ' 2= v, 2= v; then, from previous statements it follows that K(' $ ) 2 w so that by axiom 6 in (3) B 2 w which is a contradiction.
Lemma 2. For all ' 2 LL INF and w 2 Wc it holds that ' 2 w if and only if Mc; w '.
Proof. We have to prove the statement for all ' 2 LL-INF.
– ' = p, w 2 Wc, if p 2 w then p 2 Vc(w) so for the truth conditions in definition (1) we have Mc; w p; to prove the opposite implication we have to proceed with the same reasoning; – ' = exec( ), w 2 Wc, if exec( ) 2 w then 2 Ec(w) so for the truth conditions in definition (1) we have Mc; w exec( ); – all the other cases have the same proof except ' = B '. Assume B ' 2 w and w 2 Wc:
A'(w) = fv 2 Rc(w) j ' 2 vg = = by definition (1) =
=k ' kwMc \Rc(w)
Nc(w) = fA'(w) j B' 2 wg so for the previous definition of canonical model: than k ' kwMc 2 Nc(w) and for definition (1) Mc; w B '.
Suppose B ' 2= w so :B ' 2 w and we have to prove k ' kwMc \ Rc(w) 2= Nc(w). Choose A 2 Nc(w), by definition we know A = A (w) for some with B 2 w. By Lemma (1) there is some v 2 Rc(w) such thatM'c2\vR$c(w)) n A (w); 2= v, so we have: 1. for (!) thanks to the induction hp v 2 (k ' kw 2. for ( ) thanks to the induction hp vI 2 A (w) n (k ' kwMc \ Rc(w)); than for (1) and (2) A (w) 6=k ' kwMc \ Rc(w) and since A = A (w) was arbitrary in Nc(w) we conclude that k ' kwMc \ Rc(w) 2= Nc(w), and so than Mc; w 2 B '.
Lemma 3. For all ' 2 LL-DINF there exists '~ 2 LL-INF such that L (for any L-DINF formula we can find an equivalent L-INF formula).
DINF ` $ '~ [ ]p with p in '.
Proof. We have to prove the sentence for all ' 2 LL-INF but we show the proof only for ' = p because the others are proved analogously. By the axioms in Section (3) we have [ ]p $ p and by axiom (18) we have [ ]p $ p which means that we can replace ' $ '[[ ]p=p] The previous lemmas allow us to prove the following theorems.
Theorem 1. L-INF is strongly complete for the class of L-INF models. Proof. Any consistent set ' may be extended to a maximal consistent set of formulas w? 2 Wc and Mc; w? by Lemma (2). Then, L-INF is strongly complete for the class of L-INF models.
Theorem 2. L-DINF (without ) is strongly complete for the class of L-INF models. Proof. If K is a consistent set of LL-DINF formulas then K~ = f'~ j ' 2 Kg is a consistent set of LL-INF formulas by Lemma (3). By Theorem (1) there is a model Mc with a world w such that Mc; w K~ . But since L-DINF is sound and for each ' 2 K, L DINF ` ' $ '~, it follows Mc; w K then L-DINF is strongly complete for the class of L-INF models.
In this paper we discussed some cognitive aspects of autonomous system, concerning execution steps and executability. To model these aspects we have proposed the modal logic L-INF, and we have proved some useful properties among which strong completeness, though under significant restrictions.
In future work we mean to extend our logic to the multi-agents case and to prove,
without restrictions, that L-INF is strongly complete. We will then extend L-INF to the
multi-agents case and there is an intention to insert the concept of budget, as a value
that represents how much an agent can spend of his own resources in the world w. This
is important to better represent the fact that the agent is resource-bounded. Moreover,
we have to compute the complexity and extend the group of inferential actions that we
consider. Also, the temporal aspects of an agent’s operation has not been considered
here, but we tackled this aspects in [
EPTCS, Volume 306 (2019) 452–460 14. Savic, N., Studer, T.: Relevant justification logic. FLAP 6(2), 397–412 (2019) 15. Tørresen, J., Plessl, C., Yao, X.: Self-aware and self-expressive systems. IEEE Computer 48(7) (2015) 18–20 16. Vela´zquez-Quesada, F.R.: Explicit and implicit knowledge in neighbourhood models. In: Grossi, D., Roy, O., Huang, H. (eds.) Logic, Rationality, and Interaction - 4th International Workshop, LORI 2013, Hangzhou, China, October 9-12, 2013, Proceedings. pp. 239–252.
Springer (2013). https://doi.org/10.1007/978-3-642-40948-6-19 17. Vela´zquez-Quesada, F.R.: Dynamic epistemic logic for implicit and explicit beliefs. Journal of Logic, Language and Information 23(2), 107–140 (2014). https://doi.org/10.1007/s10849014-9193-0 18. Richard W. Weyhrauch Prolegomena to a Theory of Mechanized Formal Reasoning Artificial Intelligence, 13(1-2) (1980) 133–170