Towards reasoning about the past in neural-symbolic systems Rafael V. Borges and Luı́s C. Lamb Artur S. d’Avila Garcez Institute of Informatics Department of Computing Federal University of Rio Grande do Sul City University London Porto Alegre RS, 91501-970, Brazil London EC1V 0HB, UK rvborges@inf.ufrgs.br; LuisLamb@acm.org aag@soi.city.ac.uk Abstract ing the structure of a given network. We introduce Sequen- tial Connectionist Temporal Logic (SCTL), an approach that Reasoning about the past is of fundamental im- deals with past temporal knowledge in CILP and CML-based portance in several applications in computer sci- models, proposing improvements to their translation algo- ence and artificial intelligence, including reactive rithms. Our work builds upon temporal logic programs, us- systems and planning. In this paper we propose ing past operators only, and proposes algorithms to effect the efficient temporal knowledge representation algo- translation of temporal logic programs into a connectionist rithms to reason about and implement past time architecture. logical operators in neural-symbolic systems. We Section 2 contains background information on logics; Sec- do so by extending models of the Connectionist In- tion 3 describes the algorithm that translates temporal pro- ductive Learning and Logic Programming System grams into neural networks; Section 4 analyses the behaviour with past operators. This contributes towards inte- of the networks when computing a program; Section 5 con- grated learning and reasoning systems considering cludes and points out directions for further research. temporal aspects. We validate the effectiveness of our approach by means of case studies. 2 Preliminaries In this section we introduce basic definitions of logic pro- 1 Introduction gramming and temporal reasoning used in this paper. Neural-symbolic systems address the need of bridging the Definition 2.1 An atom A is a propositional variable; a lit- gap between the symbolic and connectionist paradigms of ar- eral is an atom A or a negation of an atom (∼ A). A temporal tificial intelligence [3]. The ability to reason about and learn atom is recursively defined by the following: (i) Every atom with past information is a relevant aspect of intelligent be- A is a temporal atom; (ii) if α and β are temporal atoms, then haviour [5]. In systems as [2] information about the past is α, α, α and α S β are temporal atoms. We define a tem- fundamental in the decision making process of reactive sys- poral literal λ as a temporal atom or its negation. A clause tems. Past time operators have also been shown applicable in is an implication of the form α ← λ1 , λ2 , ..., λn with n ≥ 0, the study of knowledge-based programs [9]. Some connec- where α is a temporal atom and λi , for 1 ≤ i ≤ n, are literals. tionist systems effect temporal reasoning and learning based In the remainder of the paper, we shall refer to the temporal on past information, e.g. [8; 12]. atoms simply as atoms. A program is a set of clauses. On the other hand, a systematic neural-symbolic method to treat non-classical logics has only recently been outlined [4; Definition 2.2 [1] Let BP denote the Herbrand base of a tem- 5; 6]. The Connectionist Inductive Learning and Logic Pro- poral logic program P, i.e., the set of temporal atoms oc- gramming System (CILP) [7] is a neural-symbolic system curring in P. A level mapping for a program P is a func- based on the translation of logic programs into a connec- tion | | : BP → N of ground atoms to natural numbers. tionist architecture with sound semantics and good perfor- For α ∈ BP , |α| is called the level of α and | ∼ α| = |α|. mance in real world applications. Connectionist Modal Log- A sequential temporal logic program P is acceptable w.r.t a ics (CML) proposed in [5; 6] have combined the strengths level mapping | | and a model m of P if, for every clause of non-classical logics and neural networks by offering in- α ← λ1 , ..., λk in P, and 1 ≤ i ≤ k, the following implication tegrated reasoning and learning within the same computa- holds: if m  λ1 ∧ ... ∧ λi−1 then |α| > |λi |. A program P tional model. In CML one is able to compute and learn ex- is acceptable if it acceptable w.r.t. some level mapping and pressive non-classical logics, including modal, temporal, and some model. A propositional program P is acyclic w.r.t a level intuitionistic reasoning [5; 6]. This work follows the same mapping | | if, for every clause α ← λ1 , ..., λk in P, |α| > |λi | line of research. In particular, the approach presented in for 1 ≤ i ≤ k . A program P is acyclic if it is acyclic w.r.t this paper contributes towards networks’ complexity issues. some level mapping. We present an algorithm capable of representing and reason- Proposition 2.3 [1] Every acyclic program P is also accept- ing about temporal information without the need of replicat- able. The semantics of a logic program can be defined by means of A program P in which the previous time operator  is the the fixed point of the immediate consequence operator [10]. only temporal operator is called -based program. For acceptable programs, this operator converges to a unique Definition 2.7 The immediate consequence operator T PT (IPt ) fixed point. Since this operator serves as basis for the trans- of a program P maps any interpretation IPt at a time t to a new lation algorithm, we shall define these notions for sequential interpretation assigning true to an atom α iff α follows one of temporal logic programs. the rules in definitions 2.4, 2.5, 2.6. The restricted operator Definition 2.4 The immediate consequence operator T Pt of a T Pt (IPt ) maps IPt to a new interpretation assigning true to an temporal program P at a time t ≥ 1 maps an interpretation IPt atom α iff α is constructed as in definitions 2.4, 2.5. of the temporal atoms of the program to a new interpretation of these atoms, where T Pt (IPt )(α) is true if there is a clause of 3 Translation Algorithm the form α ← λ1 , ..., λn and IPt (λi ) is true for all 1 ≤ i ≤ n. In this section we describe the algorithm that translates a tem- When t = 1 (the initial point), past information is not consid- poral logic program into a recurrent neural network. ered, and an atom is considered true iff it is head of a clause of the form α ← λ1 , ..., λn . For the other time points, other 3.1 Temporal Conversion semantic rules, considering past information, must be taken The first step of the algorithm consists in converting a tempo- into consideration to compute the T Pt operator for t > 1. We ral logic program P into a new -based program P1 . This step shall define these new rules in the sequel. is executed in order to adapt the program to the connection- 2.1 Past time operators ist architecture that shall be used to represent the semantics of the program, since this architecture allows only the com- The basic operator that makes reference to the past is the pre- putation of the previous time operator. As described in the vious time operator . It refers to information at the immedi- previous section, each temporal operator can be represented ately prior point in the time line. A new semantic rule must as a recursive function of the fixed point in the previous time. be considered to deal with this operator in the computation of This can be represented by the insertion of clauses in the sys- the immediate consequence operator: tem, as in Fig. 1. Note that in the new program the temporal Definition 2.5 The immediate consequence operator of a atoms where the operator is different from the previous time program P maps an interpretation IPt at time t to a new in- operator are considered as simple atoms, i.e. the semantics of terpretation assigning true to a atom of the form α if α is the remaining operators is not considered. true at time t − 1, i.e. T Pt (IPt )(α) = true if FPt−1 (α) = true, where FPt−1 is the fixed point of program P at t − 1. T empConversion(P) The semantics of the remaining past operators may be recur- foreach γ ∈ Atoms(P) do sively defined through the use of the previous time operator. if γ = α then These definitions allow a simple representation of these oper- AddClause(P, α ← α, α) ators in a connectionist setting. We also note that we assume a end non-strict definition of past time, i.e. we consider the present if γ = α then time. The  operator (always in the past) denotes that an AddClause(P, α ← α) AddClause(P, α ← α) atom is true at every time point in the past. It is recursively end defined as α ↔ α ∧ α. The  operator (sometime in the if γ = α S β then past) is the dual of the  operator. It denotes that an atom is AddClause(P, α S β ← β) true in some previous time point. It is recursively defined as AddClause(P, α S β ← (α S β), α) α ↔ α∨α. The S binary operator (since) represents that end an atom α has been true since the last occurrence of another end atom β. It is recursively defined as α S β ↔ β∨(α∧(α S β)) return (P) At time t = 1, (α S β) and α are assigned false, and α end Figure 1: First step of the translation 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 Pt+1 Lemma 3.1 The application of the T Pt (IPt ) operator of a tem- operator. Therefore, the following rules must be considered poral program P over an interpretation IPt and the appli- in the computation of the fixed point of a program: cation of the T Pt (IPt ) operator of a -based program P1 = Definition 2.6 The immediate consequence operator of a T empConversion(P) over the same interpretation assigns the program P maps an interpretation IPt at time t to a new in- same valuation for all atoms α ∈ BP . terpretation assigning true to atoms as follows: 1. T Pt (IPt )(α) = true if IPt (α) = true and FPt−1 (α) = true; Proof(sketch): The rules in definitions 2.4 and 2.5 define both T Pt (IPt ) and T Pt (IPt ), so the result of the immediate con- 2. T Pt (IPt )(α) = true if IPt (α) = true or FPt−1 (α) = true; sequence operator application for atoms that follow these two 3. T Pt (IPt )(α S β) = true if IPt (β) = true; definitions is the same. The clauses inserted by the algorithm 4. T Pt (IPt )(α S β) = true if IPt (α) = true and FPt−1 (α S β) = and Def. 2.5 are enough to ensure the computation of T Pt true; where, by definition, FP0 (α) = true, FP0 (α) = false according the recursive definition 2.6, without inserting any and FP0 (α S β) = false. false assignment.  Example 3.2 Suppose the following about the development ExecuteCILP(P) of a system: “A program had no errors before the last mod- max (k,µ)−1 Define maxPP (k,µ)+1 ≤ Amin < 1 ification. Since the last modification, it is producing an un- min )−ln(1−Amin ) desired result. Therefore, the last modification has to be cor- Define W ≥ maxln(1+A P (k,µ)(Amin −1)+Amin +1 · β2 rected”. Table 1 shows two examples of temporal sequences, foreach Cl ∈ Clauses(P) do illustrating the assignment of truth values to the atoms. E rep- AddHiddenNeuron(N , hl ) resents the existence of an error in the program, L, represents foreach α ∈ body(Cl ) do that the last modification is being made, and Corr, denotes if inα < Neurons(N ) then that a correction must be made over the last modification. AddInputNeuron(N , inα ) ActivationFunction(inα ) ← g(x) Case a: end Atom t=1 t=2 t=3 t=4 t=5 t=6 t=7 AddLink(N , inα , hl , W) end E F F F F T T T foreach ∼ α ∈ body(Cl ) do L F F T T F F F if inα < Neurons(N ) then Corr F F F F T T T AddInputNeuron(N , inα ) Case b: ActivationFunction(inα ) ← g(x) Atom t=1 t=2 t=3 t=4 t=5 t=6 t=7 end E F T T T T T T AddLink(N , inα , hl , −W) end L F F T T T F F α ← head(Cl ) Corr F F F F F F F if outα < Neurons(N ) then Table 1: Temporal sequences describing the example AddOutputNeuron(N , outα ) end AddLink(N , hl , outα , W) Table 2 shows a possible description of this problem as a tem- T hreshold(hl ) ← (1+Amin2)(kl −1) W poral logic program. T mp is an atom which is true if the last T hreshold(outα ) ← (1+Amin2)(1−µl ) W modification is made after a time point where the program ActivationFunction(hl ) ← h(x) has no error. The first two lines show a program representing ActivationFunction(outα ) ← h(x) this problem, and the remaining lines contain the clauses in- end serted in the program by the function T empConversion. Note foreach α ∈ atoms(P) do that two temporal atoms in the program have been translated. if (inα ∈ neurons(N )) ∧ (outα ∈ neurons(N )) then AddLink(N , outα , inα , 1) Atom E S L is represented by clauses 3 and 4, and T mp is end represented by clauses 5 and 6. end return N 1 Corr ← E, E S L, T mp end 2 T mp ← L, ∼ E Figure 2: CILP’s Translation Algorithm 3 ESL←L 4 E S L ← (E S L), E 5 T mp ← T mp outα where α is the atom represented by these neurons. hi 6 T mp ← T mp are hidden neurons representing each clause of the program. AddLink(N , source, target, W) denotes the insertion of a link Table 2: Example of the first step of the algorithm from a neuron source to a neuron target in a network N , with weight W. 3.2 CILP’s Algorithm Application Lemma 3.3 ([7])For each classic logic program P, there The main step of the translation consists in the application of exists an artificial 3-layered neural network N = CILP’s algorithm[7]. The process consists in a localist rep- ExecuteCILP(P) that computes T P . resentation of the program in a three-layered neural network, where each atom is represented by neurons in the input and 3.3 Adding Recurrent Links the output layer and each clause is represented by an hidden Next, we extend CILP’s architecture for temporal computa- neuron. Every temporal atom will be treated by the transla- tion making use of delayed recurrent links between output tion as classical atoms are treated in the original algorithm. and input layers, as in NARX models [12]. This allows the CILP’s algorithm is described in Fig. 2. construction of connectionist models for temporal processing In Fig 2 maxP (k, µ) is the maximum value among the num- without the need of copying networks in time. To integrate ber of literals in a clause and the number clauses with the these models we insert a recurrent (delayed) link from any same head in program P, where k is the number of literals neuron outα in the network’s output (representing an atom α) in the body of a clause, µ is the number of clauses with the to a neuron inα in the network’s input. This connection al- same head; Amin is the minimum activation value for a neu- lows the network to propagate the truth value of α at time t to ron to be considered active (or true). Neurons in the input the neuron representing α at time t + 1. Fig. 3 presents the layer are labelled inα ; neurons in the output layer are labelled algorithm that computes this process. Lemma 3.4 Consider a network N = ExecuteCILP(P), program. Therefore, in order to guarantee the precondition where P is a -based program. The computation of the T Pt in Lemma 3.4, a mechanism is necessary to ensure that the operator by a network N1 = InsRecLinks(N ) is correct if activation value of an output neuron outα be correctly asso- each atom α, such that α appears in P, is correctly repre- ciated with the interpretation assigned to the atom α that it sented by an output neuron outα in N . represents. This must be achieved even if the activation does Proof(sketch): Since the behaviour of the delayed link con- not occur by means of the computation of a clause of the pro- sists in propagating the output value of a neuron in time t to gram, but through a direct application of a value in an input an input neuron in time t + 1, the correctness of the CILP neuron inα representing the same atom. Besides the need to translation algorithm and the semantics of the  operator are represent the propagation of values inserted from temporal sufficient to verify this lemma. 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 neu- InsRecLinks(N ) ron inα representing it has no effect over the output neuron foreach outα ∈ neurons(N ) do representing the same atom. In the same way, in the model if inα ∈ neurons(N ) then proposed in [11], the output neuron that represents atom α AddDelayedLink(N , outα , inα ) does exist in the network, but it does not correspond to the in- end terpretation of α as there is no connection between this output end neuron and the input neuron to which the input value is pre- end sented. This is what we call the missing links issue. Table 4 Figure 3: Insertion of recurrent links shows the fixed point calculated by the network at each time point of Case b in Table 1. Here, one can notice a specific example of the effects of the absence of an output neuron to represent an atom. Since we have no output neuron repre- senting atom E, the input neuron representing E will not receive any value, therefore the semantics of the atom will not be correctly represented1 . Our solution to solve this is- sue consists in inserting clauses in the program, in order to have each necessary atom appearing as head of a clause and keeping the same semantics of the original program, as in Fig. 5. This algorithm uses three different flags for each atom in the program. I sHead identifies if the atom is the head of a clause in the program; I sNeeded identify if the atom is re- quired in the output; I sInput identifies if the atom receives input information (external to the clauses of the program). Figure 4: Network generated for the example problem The later two flags may be defined externally, according the definitions of the problem, or through the algorithm. In our Fig. 4 shows the architecture produced by the application of example, I sNeeded is true for the atom Corr, as it represents the CILP’s translation algorithm and the insertion of delayed the output of the system, and I sInput is defined as true for the recurrent links over the program of Table 2. Table 3 shows two inputs: E and L. After executing the algorithm, one new the fixed point calculated by the network at each time point clause is added to the program: E ← E∗. of Case a in Table 1. Values shown in the table consist of the values represented by each output neuron after they con- verge to a stable state at each time point. This convergence is Case b: described in Section 4. Atom t=1 t=2 t=3 t=4 t=5 t=6 t=7 Corr F F T T T T T Case a: T mp F F T T T F F Atom t=1 t=2 t=3 t=4 t=5 t=6 t=7 ESL F F T T T T T Corr F F F F T T T T mp F F T T T T T T mp F F T T F F F Table 4: Stable states at each time point ESL F F T T T T T T mp F F T T T T T Lemma 3.5 Consider a -based program P1 , a pro- Table 3: Stable states at each time point gram P2 = CorrectProgram(P1 ) and a network N = ExecuteCILP(P2 ). For each atom α that is necessary as output, or that appears in the form α in program P1 , the 3.4 The missing links issue network N contains an output neuron outα correctly repre- Due to their behaviour, associated with the T P operator of senting α. a (propositional) logic program, CILP’s networks define only the propagation of values to a neuron in the output layer when 1 In the example we considered that the absence of value should it represents an atom that appears as head of a clause in the be represented as a false assignment to the atom. CorrectProgram(P) Proposition 3.6 The network N generated by SCTL’s algo- foreach α ∈ atoms(P) do rithm over a temporal logic program P computes the T Pt op- I sNeeded(α) ← true erator of the program at any time point t, provided that the I sInput(α) ← true FPt−1 operator is correctly calculated. end foreach α ∈ atoms(P) do The proof of this proposition follows directly from the proofs if (I sNeeded(α) ∨ I sHead(α)) ∧ I sInput(α) then of lemmas 3.4 and 3.5. Note that one aspect of the translation AddClause(α ← α∗) still must be ensured: the correct computation of the fixed end point FPt operator of the program for each time point t. In end the next section we show an analysis of the behaviour of the return P network and propose a method to guarantee this correctness. end Figure 5: Insertion of clauses in the program Case a: Atom t=1 t=2 t=3 t=4 t=5 t=6 t=7 Proof(sketch): There are 3 cases to consider. If the assign- Corr F F F F T T T ment to α is due to a clause in P, then the translation algo- T mp F F T T F F F rithm guarantees the existence of outα . If the assignment is ESL F F T T T T T due to an external assignment, the clause α ← α∗ guarantees T mp F F T T T T T the existence of outα and the correct assignment of the exter- E F F T T T T T nal value. If no assignment is defined to α, the atom is not Case b: represented on the output layer, and it is assigned false.  Atom t=1 t=2 t=3 t=4 t=5 t=6 t=7 Corr F F F F F F F 3.5 SCTL’s Algorithm T mp F F F F F F F The transformation described above for the program requires ESL F F T T T T T a slight modification of the last step of the translation algo- T mp F F F F F F F rithm to create correct temporal links to the neuron represent- E F T T T T T T ing renamed atoms. This algorithm is represented in Fig. 6. Fig. 7 shows the network produced by the algorithm for the Table 5: Stable states for modified network S CT L T ranslation(P) P1 := T empConversion(P) P2 := CorrectProgram(P1 ) 4 Analysing the networks’ behaviour N := ExecuteCILP(P2 ) foreach α ∈ atomsP2 do if inα∗ ∈ neurons(N ) then Next, we describe the behaviour of the generated network in AddDelayedLink(N , outα , inα∗ ) order to provide a method to execute the propagation of val- end ues and treatment of different recurrent links to guarantee the else if inα ∈ neurons(N ) then correct computation w.r.t. semantics. As depicted in the last AddDelayedLink(N , outα , inα ) lines of CILP’s algorithm (Fig. 2), some recurrent links are end inserted from the output to the input neurons that represent end the same atoms. This is done in order to apply, in the in- end put of the network, the values calculated in the feedforward Figure 6: SCTL Algorithm propagation, allowing the recursive calculation of T P . These recurrent links [11] are used in the CILP networks to achieve example. A new analysis of the stable states achieved by the a stable state of the network representing the fixed point se- network at each time point for cases a and b in Table 1 shows mantics of the translated program. However, the behaviour that the network is computing the expected behaviour of the of such recurrences and the stability of the model has been program, as seen in Table 5. hardly studied. When a positive assignment is externally de- fined for an atom α, it must be kept during all recursive ap- plications of the T P operator (until it reaches the fixed point). However, when the positive assignment of the atom is due to a clause of the program, it is a function of a specific calculation of the T P operator over a specific input interpretation, and can be changed until the convergence of the system. There- fore, a mechanism to ensure the convergence of the network is needed to allow correct computation of the fixed point of the program by the network, and no practical approaches were defined to do that. To provide such mechanism we focus on acyclic programs. We define the number of executions of the Figure 7: Network generated by the final algorithm feedforward step of the network that is enough to ensure the computation of the fixed point of the program as follows. Lemma 4.1 For each atom α in an acyclic program P, the Theorem 4.3 A neural network N generated by SCTL’s number ν(α) of executions of TP (α) that is sufficient to con- translation algorithm application over an acyclic temporal verge to a stable interpretation of this atom is a) ν(α) = 0, logic program P computes the fixed point semantics of P. if α does not appear as head of any clause, or b)ν(α) = maxbody(α) + 1, otherwise. maxbody(α) is defined as the 5 Conclusions maximum ν(β) among all atoms β that appear in the body of We have presented a new approach to incorporate past time any clause where α is the head. operators in neural-symbolic systems. We have analysed sev- Proof(sketch): If an atom α does not appear as head of any eral aspects concerning the representation of a temporal logic clause, its truth value is defined by the external assignment program in a connectionist system and the behaviour of such system when computing the program. This work has also (or assigned to false due to default negation). So, its value contributed to the missing links issue in logic-connectionist is already stable, without the need of any computation of TP translation algorithms. This work can be seen as a stepping operator. Else, if α appear as head of one or more clauses, stone for the construction of an architecture that integrates the acyclic limitation to the program ensures that the inter- past temporal reasoning and learning in neural-symbolic sys- pretation of the body of the clauses does not change after tems. As future work we intend to apply the system to real- ”maxbody(α)” executions of the TP operator. Therefore, only life problems so as to verify its adequacy as regards knowl- one more execution of the operator is necessary to compute edge representation, reasoning and learning in intelligent sys- the stable value of α.  tems. Acknowledgements This work has been partly supported by CNPq For each acyclic program P, we can define a value ν(P) that is and CAPES, Brazilian Research Foundations. the greatest value between the ν(α) of all atoms α in P. In our example, the value of ν for the atoms that appear as head are References described in Table 6. Since the value of ν for the remaining [1] K. R. Apt and D. Pedreschi. Reasoning about termination atoms is 0, the value of νP for the program is 3, the maximum of pure prolog programs. Information and Computation, value in the table. 106:109–157, 1993. [2] Howard Barringer, Michael Fisher, Dov M. Gabbay, Graham ν(E) = ν(E∗) + 1 = 0 + 1 = 1 Gough, and Richard Owens. Metatem: An introduction. For- ν(T mp) = max(ν(L), ν(E)) + 1 = 1 mal Asp. Comput., 7(5):533–549, 1995. ν(T mp) = max(ν(T mp), ν(T mp)) + 1 = 2 [3] A. S. d’Avila Garcez, K. Broda, and D. M. Gabbay. Neural- ν(E S L) = max(ν(L), ν((E S L)), ν(E)) + 1 = 2 Symbolic Learning Systems: Foundations and Applications. ν(Corr) = max(ν(E), ν(E S L), ν(T mp)) + 1 = 3 Perspectives in Neural Computing. Springer-Verlag, 2002. Table 6: Stable states at each time point [4] A. S. d’Avila Garcez and Luı́s C. Lamb. Neural-symbolic sys- tems and the case for non-classical reasoning. In Sergei N. Artëmov, Howard Barringer, Artur S. d’Avila Garcez, Luı́s C. Lemma 4.2 The execution of νP feed-forward steps of a net- Lamb, and John Woods, editors, We Will Show Them! Essays work N generated by applying CILP’s algorithm over an in honour of Dov Gabbay, pages 469–488. College Publica- acyclic program P is equivalent to νP recursive computations tions, 2005. of the TP operator, and therefore it computes the fixed point [5] A. S. d’Avila Garcez and Luis C. Lamb. A connectionist com- of a program P. putational model for epistemic and temporal reasoning. Neural SCTL networks make use of the CILP model to compute the Computation, 18(7):1711–1738, 2006. semantics of a logic program, and use delayed recurrent links [6] A. S. d’Avila Garcez, Luis C. Lamb, and D. M. Gabbay. Con- in order to realise the propagation of past information through nectionist computations of intuitionistic reasoning. Theoretical time. These links differ from CILP links because the aim Computer Science, 358(1):34–55, 2006. of the latter is to allow the recursive computation of the T P [7] A. S. d’Avila Garcez and G. Zaverucha. The connectionist operator at a single time point, i.e. without temporal mean- inductive learning and logic programming system. Applied In- ing. The behaviour of SCTL networks can be described as telligence Journal, 11(1):59–77, 1999. follows. At the beginning of the time flow (t = 1), the re- [8] Jeffrey L. Elman. Finding structure in time. Cognitive Science, current links are reset and their value, together with the input 14(2):179–211, 1990. vector, are applied to the input layer of the network. During [9] R. Fagin, J. Halpern, Y. Moses, and M. Vardi. Reasoning about the computation of the same time point, ν feed forward value Knowledge. MIT Press, 1995. propagations are executed. Between these propagations, the [10] M. Gelfond and V. Lifschitz. The stable model semantics for values in the CILP recurrent links are updated, but the SCTL logic programming. In Proc. ICLP, pages 1070–1080. MIT links are kept unchanged. At the end of the ν propagations 2 , Press, 1988. a new input vector is presented to the network, and the activa- [11] S. Holldobler and Y. Kalinke. Toward a new massively parallel tion values at the output layer are propagated through SCTL’s computational model for logic programming. In Proc. of the recurrent links, starting the computation at a new time point. Workshop on Combining Symbolic and Connectionist Process- Theorem 4.3 follows from lemma 4.2 and proposition 3.6. ing, ECAI 94, pages 68–77, 1994. 2 [12] Hava T. Siegelmann, Bill G. Horne, and C. Lee Giles. Compu- If a training algorithm like backpropagation is applied to the tational capabilities of recurrent narx neural networks. Techni- network, the back propagation of the error should be performed in cal report, College Park, MD, USA, 1995. this moment.