=Paper=
{{Paper
|id=None
|storemode=property
|title=Compact Crossbar
Variable Binding for Neuro-Symbolic Computation
|pdfUrl=https://ceur-ws.org/Vol-764/paper04.pdf
|volume=Vol-764
|dblpUrl=https://dblp.org/rec/conf/nesy/PinkasLC11
}}
==Compact Crossbar
Variable Binding for Neuro-Symbolic Computation==
<pdf width="1500px">https://ceur-ws.org/Vol-764/paper04.pdf</pdf>
<pre>
Compact Crossbars of Multi-Purpose Binders for Neuro-Symbolic Computation

                                         Work in Progress Report


              Gadi Pinkas                        Priscila M. V. Lima                      Shimon Cohen
          Center for Academic                   Universidade Federal                    Center for Academic
            Studies, Israel                    Rural do Rio de Janeiro                    Studies, Israel
                                                 Seropédica, Brazil
            gadip@mla.ac.il                                                           shamon51@gmail.com
                                                 priscilamvl@ufrrj.br
                     Abstract
We present a compact – yet expressive – Multi-                 1   Introduction
purpose, distributed binding mechanism, which is
useful for encoding complex symbolic knowledge                 1.1 The Binding Problem
and computation, using Artificial Neural Networks              Human cognition is capable of producing combinatorial
(ANNs) or using Satisfiability (SAT) solvers. The              structures. The general binding problem concerns how items
technique is demonstrated by encoding unrestricted             that are encoded in distinct circuits of a massively parallel
First Order Logic (FOL) unification problems as                computing device (such as the brain or ANN) can be com-
Weighted Max SAT problems and then translating                 bined in complex ways for perception, reasoning or for ac-
the later into ANNs (or learning them). It is capa-            tion [Feldman 2010]. Consider for example, a planning
ble of capturing the full expressive power of FOL,             problem, where the task is to pick up an object and move it
and of economically encoding a large Knowledge                 from its current position to another place. In order to meet a
Base either as long term synapses or as clamped                goal, a “brain”-like device, must be able to represent the
units in Working Memory. Given a goal, the mech-               object, its properties, its position and the ways to manipulate
anism is capable of retrieving from the synaptic               it, in such a way that the goal is achieved. The object and its
knowledge just what is needed, while creating nov-             properties must be bound together, and this rather complex
el, compound structures in the Working Memory.                 structure should also be used in conjunction with other enti-
Two levels of size reduction are shown. First, we              ties and rules, such as the action consequences (e.g., moving
build a Working Memory, using a pool of multi-                 X from Y to Z clears position Y while occupying position
purpose binders, based on the assumption that the              Z). In another example, consider the sentence: “Sally ate”:
number of bindings that are actually needed is far             In language processing, the verb “EAT” is a predicate with
less than the number of all theoretically possible             at least two roles - EAT(“Sally”,X). The noun “Sally”
bindings. The second level of compactness is due               should be bound to the first role, while an existentially
to the fact that, in many symbolic representations,            quantified variable (representing “something”) should be
when two objects are bound, there is a many-to-one             bound to the second role. Once we get the information that
relationship between them. This happens because,
frequently, either only one value is pointed by vari-
                                                               “Sally ate salad”, and knowing the rule: EAT(Y,X) DI-   ⇒
                                                               GESTED(X) we should reason that “the salad is digested”.
able or only one variable point to a value. A cross-           In order to do that, we must bind the variable X to the noun
bar binding network of n × k units with such re-               “salad”, while X must be bounded to both EAT(,X) and
striction, can be transformed into an equivalent               DIGESTED(X).
neural structure of size O(n log(k)). We show that,
for performing unrestricted FOL unifications, the
Working Memory created is only log dependent on                1.2 Connectionism and Variable Binding
the KB size; i.e., O(n log(k)). The variable binding
                                                               During the years, connectionist systems have been criticized
technique described is inherently fault tolerant as            for “Propositional Fixation” [McCarthy 1988]. In [Fodor,
there are no fatal failures, when some random neu-
                                                               Phylyshyn 1988] connectionism was criticized for lacking
rons become faulty and the ability to cope with
                                                               abilities to construct combinatorial representations and for
complex structures decays gracefully. Processing               performing processes that are sensitive to complex structure.
is distributed and there is no need for a central con-
                                                               Exactly how compositionality can occur is a fundamental
trol even to allocate binders. The mechanism is
                                                               question in cognitive science and the binding aspect of it has
general, and can further be used for other applica-            been identified as a key to any neural theory of language
tions, such as language processing, FOL inference              [Jackendoff 2002]. Several attempts have been made to ap-
and planning.
                                                               proach the variable binding problem in a connectionist




                                                          14
framework [Shastri, Ajjanagadde 1993], [Browne, Sun                       work; yet, for ANNs with symmetric weights (e.g. Hopfield,
2000], [Zimmer et al. 2006], [Van der Velde, Kamps,                       Boltzmann Machines, MFT) a simple conversion has been
Kamps 2006], [Barret et al. 2008], [Velik 2010]; yet, virtu-              shown for translating any Weighted MAX SAT problem
ally all these suggestions, have limitations, related to either           into symmetric ANN and vice-versa [Pinkas, 1991]. Any
limited expressiveness, size and memory requirements, cen-                such SAT problem could be compiled into an ANN, which
tral control demands, lossy information, etc.                             performs stochastic gradient descent on an energy function
                                                                          that basically counts the number of unsatisfied logical con-
For example, compositionality can be provided using Hol-                  straints. The size of the generated network is linear in the
lographic Reduced Represenations [Plate 1995]; however,                   size of the original formula, though additional hidden units
the convolution operation used, is lossy and errors are intro-            may be required. In addition to compilation, the logical con-
duced as structures become more complex or as more opera-                 straints of a network could be PAC learnt using Hebbian-
tions are done. The BlackBoard Architecture [Van der                      like rule [Pinkas 1995], thus, for small-size constraints, a
Velde, Kamps, Kamps 2006] can form complex structures                     network can efficiently learn its weights and structure from
but does not manipulate those structures to perform cogni-                a training set that is composed of the satisfying models. The
tion. Shastri’s temporal binding has only limited FOL ex-                 performance efficiency of this neural mechanism can be
pressiveness and no mechanism for allocating temporal                     attributed to the similarities of symmetric ANNs to stochas-
binders. Finally, all the above systems need neurons in                   tic local search algorithms, such as WALKSAT [Kautz et al
numbers that is at best linear in the KB; while some use                  2004]. Due to the tight relationship between ANNs and
much more neurons than that.1 For FOL compositionality in                 Weighted Max SAT, our methodology is to specify an ANN
ANNs see [Ballard 1986], [Pinkas 1992], [Shastri 1999],                   designed for certain symbolic computation (e.g. unification),
[Lima 2000], [Garcez, Lamb 2006]. For partial-FOL encod-                  using a set of Boolean variables (the visible units) and a set
ings in Satisfiability, see [Domingos 2008], [Clark et al.                of constraints; i.e., Boolean formulae designed for restrict-
2001].                                                                    ing the values of the visible units. The constraints specified
                                                                          are used to force the visible units to converge to a valid so-
The ability to represent combinatorial structures and reason-             lution that satisfies as many (weighted) formulae as possi-
ing with them, still presents challenges to theories of neuro-            ble. We have written a compiler that translates such specifi-
cognition [Marcus 2001], while the variable binding prob-                 cations into either weighted CNF (for Weighted Max SAT
lem is fundamental to such ability [Feldman 2010].                        Solvers) or for ANN with symmetric weights.

                                                                            We believe that our fault tolerant mechanism and meth-
1.3 Unification                                                           ods for dynamically forming recursive structures will scale
In conventional computing, unification is a key operation                 and be useful for both the engineering of massively parallel
for realizing inference, reasoning, planning and language                 devices, and for modeling of high-level cognitive processes.
processing. It is the main vehicle for conventional symbolic
systems to match rules with facts, or rules with other rules.             2   Improving CrossBar Binding
In unification, two or more distinct hierarchical entities
                                                                          The simplest, most naïve binding techniques is CrossBar
(terms) are merged, to produce a single, unified, tree-like               binding. The term was mentioned in [Barrett et al. 2008],
structure. This unified structure adheres to the constraints of
                                                                          yet it was intuitively used by many connectionist systems in
both the original entities. Formally, unification is an opera-
                                                                          the past [Ballard 1986], [Anandan 1989] and in many SAT
tion which produces from two or more logic terms, a set of                reductions; e.g., [Kautz, at el 2006]. Formally, we define
substitutions, which either identifies the terms or makes the
                                                                          crossbar binding as a Boolean matrix representation of a
terms equal modulo some equational theory. For connec-
                                                                          relation between 2 sets of items, using Characteristic Matrix
tionist approaches to unification see [Hölldobler 1990],                  of the relation; i.e., if A contains m objects and B contains n
[Weber 1992], [Komendantskaya 2010].                                      objects, then the characteristic matrix R has m lines and n
   For easiness of reading, we have chosen to demonstrate
                                                                          columns, containing m × n Boolean variables (neurons). We
our compact variable binding mechanism on the more fun-                   say that item i is bound to item j iff R(i,j)=1. In this naïve,
damental unification function, rather than on full FOL infer-
                                                                          binding mechanism, a neuron should be allocated for each
ence.
                                                                          possible binding, and all theoretic combinations of two
1.4 Artificial Neural Networks and SAT                                    items must be pre-enumerated as rows and columns of the
                                                                          matrix. A crossbar matrix, that needs to represent a complex
ANNs may be seen as constraint satisfaction networks,                     tree or a graph, must bind together not just simple constitu-
where neuron-units stand for Boolean variables, and where                 ents, but all the compounded entities representing partial
the synapse weights represent constraints imposed on the                  trees (or sub-graphs). It is possible to represent a FOL KB
variables. Any ANN may be seen as such a constraint net-                  this way at the cost of using an enormous number of neu-
                                                                          rons, and with an extremely localist approach. Even more
    1
      The BlackBoard architecture uses billions of neurons to rep-        frustrating is the fact that this technique will not be suitable
resent thousands of atomic concepts; HRR Production systems               for dynamically creating novel, nested structures upon de-
[Stewart, Elliasmith 2008] needs about one million neurons.               mand. The number of theoretic bindings, for all possible tree




                                                                     15
structures, grows exponentially with the number of constitu-               representing only those graphs that are actually needed for
ent items and must be computed in advance.                                 computing the goal. It turns out that this approach is con-
We improve this simplistic binding mechanism in several                    sistent with cognitive theories, where a large KB is stored in
steps:                                                                     synapses (long term memory); and a smaller size working
                                                                           memory is used for retrieving only few KB items at a time.
2.1 Using Binders as “pointers” to form Graphs                             Only those items that are necessary to the process4 get to be
   First, we introduce2 a special kind of entities called Gen-             retrieved from the synaptic KB. For example, if our purpose
eral Purpose Binders (GPBs). GPBs are similar to pointers                  is to find a plan for a goal, expressed in FOL, we need to
except for the fact that a single GPB can point to several                 design the WM with enough binders to represent a valid
objects, as the crossbar paradigm permits implementation of                plan. We retrieve the facts and rules of the world from that
arbitrary relations between binders and objects. In the spe-               KB only if they are required by the plan we desire to make.
cial case where binders point to binders, arbitrary directed                  To implement a pool of binders for FOL unification, the
graphs can be built. In this scenario, we can interpret each               WM should contain three crossbar matrices: One for label-
GPB as a node in the graph, and the crossbar, as specifying                ing nodes by symbols (predicates, functions, constants). The
the arcs of the graph (adjacency matrix). In such graph in-                second is for nesting of the nodes in Graphs and labeling the
terpretation, each node may be labeled using a labeling                    arcs according to slots of the predicates and functions. The
crossbar, that ties together binders, with symbols such as,                third crossbar is for retrieving items from the long term
predicates, functions or constants in FOL. Arcs can also be                memory where the KB is stored (e.g., terms, literals or
labeled, as the binder-to-binder crossbar, may have a third                clauses). This third matrix ties a binder to a KB item and
dimension which relates one or more labels to each arc. This               triggers the constraints of that item to be activated so that
enables the formation of arbitrary complex graph structures,               the binder node is forced to assume the structure of the KB
that can be used to represent language constituents and in                 item retrieved. The mechanism starts working as goal acti-
particular, FOL terms, predicates, literals and clauses. Un-               vated constraints cause some binders to be tied to KB items
like in the naïve crossbar approach, unrestricted graphs can               and activate some KB constraints. Those constraints, in
be built directly out of simple constituents, with GPB as the              turn, activate other constraints, till the WM converges to a
mechanism for gluing them together.                                        valid solution. When we implement unification problems,
   Because the binders are general-purpose entities, we can                the size of the WM is O(n ×k) where n is the maximal num-
construct a working memory out of a pool of such binders.                  ber of nodes in a solution; k is the size of the KB and n<<k.
As long as GPBs remain unallocated, they can be used for                   This constitutes a drastic improvement, as the WM size is
dynamic creation of novel, goal oriented structures. To do                 linear in the size of the KB, instead of being quadratic.5 Ac-
so, the “right” constraints should be embedded in the synap-               tually, we can do even better:
ses, forcing binders first to be allocated and then to assume
a desired structure for solving the goal. These constraints,
stored at the synaptic weights, are the driving force that                 2.3 Crossbars with n*log(k) size complexity
causes the visible units to converge to the needed graph-like              In the next size improvement, we further reduce the size of
structures.                                                                many crossbar matrices from O(n*k) to O(n* log(k)). Thus,
                                                                           in our unification example, a WM of O(n* log (k)) is creat-
   Using this technique, we show that arbitrary KB of size k,              ed, where n is the maximal size of a unification tree and k is
can be encoded in a working Memory (WM) with O(k)                          the size of the KB. This means that the WM size is only log
binders and with a total size of O(k2). Unfortunately, when                dependent6 on the KB size; rather than linearly as in previ-
the KB tends to grow, the WM and the set of constraints                    ous section.
may become too large for the mechanism to be used in real                     The key to this log-reduction, is the fact that frequently,
applications. 3                                                            binding relationships have many-to-one or one-to-many
                                                                           restrictions. For example, the crossbar matrix for node label-
2.2 Using a pool of binders “As Needed”                                    ing, allows for a binder to point only to a single symbol
Luckily, we can reduce that size requirement, drastically, as              (whereas many binders could point to the same symbol).
we can assume that, at a certain time, only few binders are                This many-to-one relationship causes the rows of the cross-
actually needed for the processing of a given goal. This is                bar labeling matrix to be Winner-Takes-All (WTA) arrays,
supported by cognitive studies [Cowan 1981] and consti-                    where only one neural unit (if any) may fire. Normally, we
tutes a common assumption of several connectionist sys-                    need mutual exclusion constraints to force the rows of the
tems [Shastri, Ajjanagadde 1993], [Barrett et al 2008]. We                 matrix to be either all-zeros or have a single variable set to
therefore can design a Working Memory of neural units,                     one. In such a scenario, however, we can replace each WTA
which uses only a pool of General Purpose Binders, labeled
and nested within each other; i.e., a small set of binders, for               4
                                                                                 When an item is already in WM, no retrieving is needed.
                                                                              5
                                                                                 The number of constraints needed for unification is O(n2k);
   2
     The method was suggested in [Pinkas 1992] and used in [Li-            linear in the KB size, when n<<k.
                                                                               6
ma 2000], [Lima 2007] for clamping a KB in Working Memory.                       Even, if occurs check is used, the WM size is still linear in
   3
     O(k3) constraints are needed for unification in this paradigm.        the KB size when n<<k.




                                                                      16
line (with k-variables), with a much smaller size line of only              4    Conclusions
O(log(k)) variables. Each such line of log(k) variables (neu-
rons), represents an index (or a signature) to the target label.            We have shown a general purpose binding mechanism that
Therefore, if a binder may point to just a single object (out               uses a pool of general purpose binders, and allocates them to
of k possible objects), we may use only log(k) bit signa-                   KB items, only when they are necessary for achieving the
tures. Fig 1 illustrates, how one binder with WTA line that                 goal. A large KB may be stored in long term connections
points to object 6 (out of 15 objects) is reduced to only 4                 rather than in the Working Memory. KB constraints are ac-
bits LOG WTA array, representing the signature of that                      tivated only upon need, and only if they are supportive for
item. This signature, once it emerges in a binder’s row, acti-              achieving the goal. We then showed that further log reduc-
vates a set of constraints associated with the bounded object.              tion is possible if the binding represents a many-to-one rela-
These constraints force the binder to get the retrieved item’s              tionship. The size of a crossbar matrix is then reduced from
structure and may cause a chain reaction of more con-                       O(n*k) to O(n*log(k)) and the number of constraints is also
straints, retrieving more KB items and so forth.                            reduced.9 We demonstrated the use of the suggested binding
                                                                            technique in ANN that performs FOL unification with size10
    1    2   3   4   5   6   7   8   9   10   11   12   13   14   15        that is O(n×log(k)). The mechanism is distributed since
    0    0   0   0   0   1   0   0   0   0    0    0    0    0    0
                                                                            there is no central control and even binder allocation is done
                             1   2   3   4
                                                                            in a totally distributed way. It is also inherently robust, as no
                             0   1   1   0                                  fatal failures occur when neurons “die”. We have performed
                                                                            initial experiments with the GPB pool mechanism (without
Figure 1. On top: A Standard WTA pointing to the 6th object;                the LOG WTA reduction), these experiments indicate the
Bellow: a LOG WTA array with a binary value of 6 representing               feasibility of the approach on rather complex unification
the 6th object’s signature ‘0110’.                                          tasks including multi-instance parallel-unification and recur-
                                                                            sive occurs checking. LOG WTA and fault tolerance exper-
It should be noted that, once a LOG WTA encoding is used                    iments are the subject of ongoing work. The mechanism
instead of the standard WTA, the constraints imposed on                     described is general and can further be used for other appli-
WM might need to be adjusted. 7                                             cations such as: language processing, FOL inference and
                                                                            planning. We are working on extending the techniques, for
                                                                            full FOL inference and conjecture that these techniques will
                                                                            also improve other SAT encodings that use crossbar-like
3       Fault Tolerance                                                     bindings, e.g. as in [Kautz, et al 2006].

The variable binding mechanism suggested and its applica-
tion to unification are inherently fault tolerant, if each varia-
ble is allocated a processing unit (a neuron). Small random
damage to the neurons does not radically affect the unifica-
tion process (if at all). For example, if a single neuron relat-            References
ed to a binder, in one of the crossbar matrices, becomes                    [Ballard 1986] D. H. Ballard. Parallel logical inference and
faulty and stops firing, then the binder cannot point to a cer-                energy minimization. In Proceedings of the AAAI Na-
tain symbol; however, other binders from the pool can be                       tional Conference on Artificial Intelligence, pages 203–
used for pointing to that symbol if such is needed. In the                     208, 1986.
meantime, this “faulty” binder may still be used, as it can be
allocated to point to other symbols. Even if the faulty neu-                [Barrett et al 2008] Barrett L, Feldman JA, Mac Dermed L.
ron starts firing constantly, it may still participate in the                  A (somewhat) new solution to the binding problem.
process if the symbol that is pointed by that “faulty” binder                  Neural Computation, 20: 2361-237, 2008.
happens to be needed. The binder will simply not be used, if                [Brown, Sun 2000] A. Browne and R. Sun. Connectionist
that symbol is irrelevant to the goal. If the damage to the                    variable binding. Springer, Heidelberg, 2000.
WM neurons is more widespread, so that a binder cannot                      [Clarke et.al 2001] E. Clark, A. Bier, R. Raimi, Y. Zhu,
take part in the process, then this binder will not be allocat-                Bounded Model Checking Using Satisfiability Solving,
ed, and therefore will not be used in the graph construction.                  in Formal Methods in System Design archive, Volume
This may shorten the number of available GPB nodes in the                      19 Issue 1, July 2001.
largest graph but will not destroy the ability of the WTA to
unify less complex terms (shallower trees).8

    7
      E.g., mutual exclusion constraints - for enforcing WTA are            for processing deep structures; e.g. deep syntactic tree pruning in
eliminated. Long OR constraints of O(k) size, become only of                Agrammatism and Broca’s Aphasia [Friedman 2002].
                                                                                9
log(k) length.                                                                    Note, that some constraints may grow in size complexity;
    8
      This property may help in supporting neuro-linguistic theo-           while others may shrink.
                                                                                10
ries that relate certain symptoms of aphasia, with loosing abilities               O(n2 +log(k)) with occurs check.




                                                                       17
[Cowan 2001] N Cowan, The magical number of 4 in short                 [McCarthy 1988] J. McCarthy, Epistemological challenges
    term memory: A reconsideration of mental storage ca-                  for connectionism. Behavioral and Brain Sciences,
    pacity, Behavioral and Brain Sciences, 1(24), 2001.                   11:44, 1988.
[Domingos 2008] P. Domingos, Markov logic: a unifying                 [Pinkas 1991] G. Pinkas, “Symmetric neural networks and
    language for knowledge and information management.                    logic satisfiability,” Neural Computation 3, no. 2,
    CIKM 2008:519.                                                        pp.282-291, 1991.
[Feldman 2010] J. Feldman, The Binding Problem(s),                    [Pinkas 1992] G. Pinkas, “Constructing syntactic proofs in
    http://www.computational-logic.org/content/events/iccl-               symmetric networks” in Advances in Neural Information
    ss-2010/slides/feldman/papers/Binding8.pdf, accessed                  Processing Systems – 4 (NIPS-91), pp.217-224, 1992.
    on May 2010.                                                      [Pinkas 1995] G. Pinkas, “Reasoning, non-monotonicity and
[Fodor, Phylyshyn 1988] J. A. Fodor and Z. W. Phylyshyn,                  learning in connectionist networks that capture proposi-
    Connectionism and cognitive architecture: A critical                  tional knowledge”, Artificial Intelligence Journal 77,
    analysis. In Pinker and Mehler (eds): Connectionism and               (AIJ) pp. 203-247, 1995.
    Symbols, 3-71, MIT Press, 1988.                                    [Plate 1995] T. Plate Holographic Reduced Representa-
[Friedman 2002] Friedmann, N.Syntactic tree pruning and                   tions, IEEE Trans. On Neural Networks 6(3), 623-641
    question production in agrammatism. Brain and Lan-                [Shastri, Ajjanagadde 1993] L. Shastri L. and V. Ajjana-
    guage, 83, 117-120                                                    gadde, From associations to systematic reasoning: A
[Garcez, Lamb, 2006] A. S. d'Avila Garcez and L. C. Lamb.                 connectionist representation of rules, variables and dy-
    A Connectionist Computational Model for Epistemic                     namic bindings using temporal synchrony. Behavioral
    and Temporal Reasoning. Neural Computation                            and Brain Sciences 1993;16(3):417-494.
    18(7):1711-1738, MIT Press, July 2006.                             [Stewart, Eliasmith 2008] T.C. Stewart, C. Eliasmith,
[[Garcez, Lamb 2006] A. S. d'Avila Garcez and L. C. Lamb.                 Building Production Systems with Realistic Spiking
    A Connectionist Computational Model for Epistemic                     Neurons”, Cognitive Science Conference. Washington,
    and Temporal Reasoning. Neural Computation                            DC. August, 2008
    18(7):1711-1738, MIT Press, July 2006.                             [Velik 2010] R. Velik, From single neuron-firing to con-
[Hölldobler 1990] S. Hölldobler, A Connectionist Unifica-                 sciousness- towards the true solution of the binding
    tion Algorithm. International Computer Science Insti-                 problem, Neuroscience Behavioral Rev., 2010, 34(7):
    tute, Berkeley, TR-90-012: 1990.                                      pp. 993-1001.
[Jackendoff 2002] Jackendoff, Ray (2002). Foundations of              [Weber 1992] V Weber, Connectionist Unification with a
    Language: Brain, Meaning, Grammar, Evolution. Ox-                     distributed Representation, In IJCNN-92
    ford: Oxford University Press. pp. 477.                           [Zimmer et. Al. 2006], HD Zimmer, A. Mecklinger, U. Lin-
[Kautz et al 2004] Henry Kautz, Bart Selman, & David                      denberger (eds), Handbook of binding and memory -
    McAllester, Walksat in the 2004 SAT Competition, In-                  Perspectives from cognitive neuroscience. Oxford Uni-
    ternational Conference on Theory and Applications of                  versity Press 2006.
    Satisfiability Testing, Vancouver, 2004
 [Kautz at el 2006] Henry Kautz, Bart Selman, and Joerg
    Hoffmann. SatPlan: Planning as Satisfiability, Abstracts
    of the 5th International Planning Competition, 2006
 [Komendantskaya 2010] E. Komendantskaya, Unification
    neural networks: unification by error-correction learning,
    Logic Jnl IGPL, 2010
[Lima, 2000] P. M. V. Lima: Resolution-Based Inference on
    Artificial Neural Networks. Ph.D. Thesis, Department of
    Computing. Imperial College London, UK (2000).
 [Lima et al 2007] P. M. V. Lima, M. Mariela, M. Morveli-
    Espinoza and F. M. G. França, Logic as Energy: A SAT-
    Based Approach, Advances in Brain, Vision, and Artifi-
    cial Intelligence Lecture Notes in Computer Science,
    2007.
[Marcus 2001] G. F. Marcus, The algebraic mind. Cam-
    bridge, MA: MIT Press, 2001.




                                                                 18

</pre>