=Paper=
{{Paper
|id=Vol-230/paper-5
|storemode=property
|title=Towards reasoning about the past in neural-symbolic systems
|pdfUrl=https://ceur-ws.org/Vol-230/05-borges.pdf
|volume=Vol-230
|dblpUrl=https://dblp.org/rec/conf/ijcai/BorgesLG07
}}
==Towards reasoning about the past in neural-symbolic systems==
https://ceur-ws.org/Vol-230/05-borges.pdf
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.