Reasoning about the past is of fundamental importance in several applications in computer science and artificial intelligence, including reactive systems and planning. In this paper we propose efficient temporal knowledge representation algorithms to reason about and implement past time logical operators in neural-symbolic systems. We do so by extending models of the Connectionist Inductive Learning and Logic Programming System with past operators. This contributes towards integrated learning and reasoning systems considering temporal aspects. We validate the effectiveness of our approach by means of case studies.
Neural-symbolic systems address the need of bridging the
gap between the symbolic and connectionist paradigms of
artificial intelligence [
On the other hand, a systematic neural-symbolic method to
treat non-classical logics has only recently been outlined [4;
5; 6]. The Connectionist Inductive Learning and Logic
Programming System (CILP) [
In this section we introduce basic definitions of logic programming and temporal reasoning used in this paper.
eral is an atom A or a negation of an atom (∼ A). A temporal atom is recursively defined by the following: (i) Every atom
α, α, α and α S β are temporal atoms. We define a temporal literal λ as a temporal atom or its negation. A clause is an implication of the form α ← λ1, λ2, ..., λn with n ≥ 0, where α is a temporal atom and λi, for 1 ≤ i ≤ n, are literals.
atoms simply as atoms. A program is a set of clauses.
Definition 2.2 [
Proposition 2.3 [
The semantics of a logic program can be defined by means of
the fixed point of the immediate consequence operator [
Definition 2.4 The immediate consequence operator T t of a P temporal program P at a time t ≥ 1 maps an interpretation It of the temporal atoms of the program to a new interpretatioPn of these atoms, where T t (It )(α) is true if there is a clause of the form α ← λ1, ..., λn andPIt (λi) is true for all 1 ≤ i ≤ n.
P
P When t = 1 (the initial point), past information is not considered, and an atom is considered true iff it is head of a clause of the form α ← λ1, ..., λn. For the other time points, other semantic rules, considering past information, must be taken into consideration to compute the T t operator for t > 1. We P shall define these new rules in the sequel. 2.1 Past time operators The basic operator that makes reference to the past is the previous time operator . It refers to information at the immediately prior point in the time line. A new semantic rule must be considered to deal with this operator in the computation of the immediate consequence operator:
program P maps an interpretation It at time t to a new interpretation assigning true to a atomP of the form α if α is true at time t − 1, i.e. T t (It )( α) = true if FPt−1(α) = true,
P P where FPt−1 is the fixed point of program P at t − 1. The semantics of the remaining past operators may be recursively defined through the use of the previous time operator. These definitions allow a simple representation of these operators in a connectionist setting. We also note that we assume a non-strict definition of past time, i.e. we consider the present time. The operator (always in the past ) denotes that an atom is true at every time point in the past. It is recursively defined as α ↔ α ∧ α. The operator (sometime in the past ) is the dual of the operator. It denotes that an atom is true in some previous time point. It is recursively defined as α ↔ α∨ α. The S binary operator (since) represents that an atom α has been true since the last occurrence of another atom β. It is recursively defined as α S β ↔ β∨(α∧ (α S β)) At time t = 1, (α S β) and α are assigned false, and α is assigned true. At the remaining points, α is interpreted w.r.t. the fixed point of the previous time; i.e. the fixed point at a time t must be calculated before the execution of the T t+1 P operator. Therefore, the following rules must be considered in the computation of the fixed point of a program:
program P maps an interpretation It at time t to a new interpretation assigning true to atoms aPs follows: 12.. TT tt ((IItt ))(( αα)) == ttrruuee iiff IItt ((αα)) == ttrruuee oarndFPFt−P1t−(1(α)α=) =trutreu; e; P P P
P P P 3. T t (It )(α S β) = true if It (β) = true;
P P P 4. T t (It )(α S β) = true if It (α) = true and FPt−1(α S β) = true;P wPhere, by definition, FP0( α) = true, F 0( α) = false
P P and F 0(α S β) = false.
P Lemma 3.1 The application of the T t (It ) operator of a temP P poral program P over an interpretation It and the appliP cation of the T t (It ) operator of a -based program P1 = T empConversionP(PP) over the same interpretation assigns the same valuation for all atoms α ∈ BP.
Proof(sketch): The rules in definitions 2.4 and 2.5 define both T t (It ) and T t (It ), so the result of the immediate con
P P P P sequence operator application for atoms that follow these two definitions is the same. The clauses inserted by the algorithm and Def. 2.5 are enough to ensure the computation of T t according the recursive definition 2.6, without inserting anPy false assignment.
A program P in which the previous time operator only temporal operator is called -based program. is the Definition 2.7 The immediate consequence operator T T (It ) P P of a program P maps any interpretation It at a time t to a new interpretation assigning true to an atom αP iff α follows one of the rules in definitions 2.4, 2.5, 2.6. The restricted operator
T t (It ) maps It to a new interpretation assigning true to an atoPm αP iff α is constructed as in definitions 2.4, 2.5.
P 3
In this section we describe the algorithm that translates a temporal logic program into a recurrent neural network. 3.1
Temporal Conversion The first step of the algorithm consists in converting a temporal logic program P into a new -based program P1. This step is executed in order to adapt the program to the connectionist architecture that shall be used to represent the semantics of the program, since this architecture allows only the computation of the previous time operator. As described in the previous section, each temporal operator can be represented as a recursive function of the fixed point in the previous time. This can be represented by the insertion of clauses in the system, as in Fig. 1. Note that in the new program the temporal atoms where the operator is different from the previous time operator are considered as simple atoms, i.e. the semantics of the remaining operators is not considered.
end
end end return (P) T empConversion(P) foreach γ ∈ Atoms(P) do if γ = α then
AddClause(P, α ← end if γ = α then
AddClause(P, α ←
AddClause(P, α ← α) end if γ = α S β then
AddClause(P, α S β ← β)
AddClause(P, α S β ← (α S β), α)
α, α)
α)
Example 3.2 Suppose the following about the development
of a system: “A program had no errors before the last
modification. Since the last modification, it is producing an
undesired result. Therefore, the last modification has to be
corrected”. Table 1 shows two examples of temporal sequences,
illustrating the assignment of truth values to the atoms. E
represents the existence of an error in the program, L, represents
that the last modification is being made, and Corr, denotes
that a correction must be made over the last modification.
The main step of the translation consists in the application of
CILP’s algorithm[
In Fig 2 maxP(k, μ) is the maximum value among the
number of literals in a clause and the number clauses with the
same head in program P, where k is the number of literals
in the body of a clause, μ is the number of clauses with the
same head; Amin is the minimum activation value for a
neuron to be considered active (or true). Neurons in the input
layer are labelled inα; neurons in the output layer are labelled
Next, we extend CILP’s architecture for temporal
computation making use of delayed recurrent links between output
and input layers, as in NARX models [
Lemma 3.4 Consider a network N = E xecuteCILP(P), where P is a -based program. The computation of the T t P operator by a network N1 = InsRecLinks(N ) is correct if each atom α, such that α appears in P, is correctly represented by an output neuron outα in N .
Proof(sketch): Since the behaviour of the delayed link consists in propagating the output value of a neuron in time t to an input neuron in time t + 1, the correctness of the CILP translation algorithm and the semantics of the operator are sufficient to verify this lemma.
foreach outα ∈ neurons(N ) do if in α ∈ neurons(N ) then
end
end
end
Due to their behaviour, associated with the T operator of
a (propositional) logic program, CILP’s networkPs define only
the propagation of values to a neuron in the output layer when
it represents an atom that appears as head of a clause in the
program. Therefore, in order to guarantee the precondition
in Lemma 3.4, a mechanism is necessary to ensure that the
activation value of an output neuron outα be correctly
associated with the interpretation assigned to the atom α that it
represents. This must be achieved even if the activation does
not occur by means of the computation of a clause of the
program, but through a direct application of a value in an input
neuron inα representing the same atom. Besides the need to
represent the propagation of values inserted from temporal
links, a similar situation can also be noticed in the original
(non-temporal) CILP’s model: the value assigned to an atom
α, represented by the application of a value in the input
neuron inα representing it has no effect over the output neuron
representing the same atom. In the same way, in the model
proposed in [
Case b: Atom
T mp E S L T mp t = 1 F F F F t = 2 F F F F t = 3 T T T T t = 4 T T T T t = 5 T T T T t = 6 T F T T t = 7 T F T T Lemma 3.5 Consider a -based program P1, a program P2 = CorrectProgram(P1) and a network N = E xecuteCILP(P2). For each atom α that is necessary as output, or that appears in the form α in program P1, the network N contains an output neuron outα correctly representing α.
1In the example we considered that the absence of value should be represented as a false assignment to the atom.
CorrectProgram(P) foreach α ∈ atoms(P) do
I sNeeded(α) ← true
I sInput( α) ← true end
end end return P end foreach α ∈ atoms(P) do if (I sNeeded(α) ∨ I sHead(α)) ∧ I sInput(α) then
AddClause(α ← α∗) Proof(sketch): There are 3 cases to consider. If the assignment to α is due to a clause in P, then the translation algorithm guarantees the existence of outα. If the assignment is due to an external assignment, the clause α ← α∗ guarantees the existence of outα and the correct assignment of the external value. If no assignment is defined to α, the atom is not represented on the output layer, and it is assigned false. 3.5 SCTL’s Algorithm The transformation described above for the program requires a slight modification of the last step of the translation algorithm to create correct temporal links to the neuron representing renamed atoms. This algorithm is represented in Fig. 6. Fig. 7 shows the network produced by the algorithm for the S CT L T ranslation(P)
P1 := T empConversion(P) P2 := CorrectProgram(P1) N := E xecuteCILP(P2) foreach α ∈ atomsP2 do if in α∗ ∈ neurons(N ) then
AddDelayedLink(N , outα, in α∗) end else if in α ∈ neurons(N ) then
end end end example. A new analysis of the stable states achieved by the network at each time point for cases a and b in Table 1 shows that the network is computing the expected behaviour of the program, as seen in Table 5.
rithm over a temporal logic program P computes the T t operator of the program at any time point t, provided thaPt the FPt−1 operator is correctly calculated.
The proof of this proposition follows directly from the proofs of lemmas 3.4 and 3.5. Note that one aspect of the translation still must be ensured: the correct computation of the fixed point FPt operator of the program for each time point t. In the next section we show an analysis of the behaviour of the network and propose a method to guarantee this correctness.
Case a: Atom
T mp E S L T mp
E Case b: Atom
T mp
E S L
T mp
E
t = 1
F
F
F
F
F
t = 1
F
F
F
F
F
t = 2
F
F
F
F
F
t = 2
F
F
F
F
T
t = 3
F
T
T
T
T
t = 3
F
F
T
F
T
t = 4
F
T
T
T
T
t = 4
F
F
T
F
T
t = 5
T
F
T
T
T
t = 5
F
F
T
F
T
t = 6
T
F
T
T
T
t = 6
F
F
T
F
T
t = 7
T
F
T
T
T
t = 7
F
F
T
F
T
Next, we describe the behaviour of the generated network in
order to provide a method to execute the propagation of
values and treatment of different recurrent links to guarantee the
correct computation w.r.t. semantics. As depicted in the last
lines of CILP’s algorithm (Fig. 2), some recurrent links are
inserted from the output to the input neurons that represent
the same atoms. This is done in order to apply, in the
input of the network, the values calculated in the feedforward
propagation, allowing the recursive calculation of T . These
P
recurrent links [
Proof(sketch): If an atom α does not appear as head of any clause, its truth value is defined by the external assignment (or assigned to false due to default negation). So, its value is already stable, without the need of any computation of TP operator. Else, if α appear as head of one or more clauses, the acyclic limitation to the program ensures that the interpretation of the body of the clauses does not change after ”maxbody(α)” executions of the TP operator. Therefore, only one more execution of the operator is necessary to compute the stable value of α.
For each acyclic program P, we can define a value ν(P) that is the greatest value between the ν(α) of all atoms α in P. In our example, the value of ν for the atoms that appear as head are described in Table 6. Since the value of ν for the remaining atoms is 0, the value of νP for the program is 3, the maximum value in the table.
ν(E) = ν(E∗) + 1 = 0 + 1 = 1 ν(T mp) = max(ν(L), ν( E)) + 1 = 1 ν( T mp) = max(ν(T mp), ν( T mp)) + 1 = 2 ν(E S L) = max(ν(L), ν( (E S L)), ν(E)) + 1 = 2 ν(Corr) = max(ν(E), ν(E S L), ν( T mp)) + 1 = 3 Lemma 4.2 The execution of νP feed-forward steps of a network N generated by applying CILP’s algorithm over an acyclic program P is equivalent to νP recursive computations of the TP operator, and therefore it computes the fixed point of a program P.
SCTL networks make use of the CILP model to compute the semantics of a logic program, and use delayed recurrent links in order to realise the propagation of past information through time. These links differ from CILP links because the aim of the latter is to allow the recursive computation of the T P operator at a single time point, i.e. without temporal meaning. The behaviour of SCTL networks can be described as follows. At the beginning of the time flow (t = 1), the recurrent links are reset and their value, together with the input vector, are applied to the input layer of the network. During the computation of the same time point, ν feed forward value propagations are executed. Between these propagations, the values in the CILP recurrent links are updated, but the SCTL links are kept unchanged. At the end of the ν propagations 2, a new input vector is presented to the network, and the activation values at the output layer are propagated through SCTL’s recurrent links, starting the computation at a new time point. Theorem 4.3 follows from lemma 4.2 and proposition 3.6.
2If a training algorithm like backpropagation is applied to the network, the back propagation of the error should be performed in this moment.
translation algorithm application over an acyclic temporal logic program P computes the fixed point semantics of P.
We have presented a new approach to incorporate past time operators in neural-symbolic systems. We have analysed several aspects concerning the representation of a temporal logic program in a connectionist system and the behaviour of such system when computing the program. This work has also contributed to the missing links issue in logic-connectionist translation algorithms. This work can be seen as a stepping stone for the construction of an architecture that integrates past temporal reasoning and learning in neural-symbolic systems. As future work we intend to apply the system to reallife problems so as to verify its adequacy as regards knowledge representation, reasoning and learning in intelligent systems.
Acknowledgements This work has been partly supported by CNPq and CAPES, Brazilian Research Foundations.