=Paper=
{{Paper
|id=Vol-1672/paper_5
|storemode=property
|title=Extending the DIAMOND System to work with GRAPPA
|pdfUrl=https://ceur-ws.org/Vol-1672/paper_5.pdf
|volume=Vol-1672
|authors=Matti Berthold
|dblpUrl=https://dblp.org/rec/conf/comma/Berthold16
}}
==Extending the DIAMOND System to work with GRAPPA==
<pdf width="1500px">https://ceur-ws.org/Vol-1672/paper_5.pdf</pdf>
<pre>
        Extending the diamond System
             to work with grappa
                            Matti BERTHOLD
           Computer Science Institute, Leipzig University, Germany

          Abstract The subject of this paper is to extend the diamond system,
          which analyses Abstract Dialectical Frameworks (adfs), such that it will
          be able to work with a variant of adfs called grappa (GRaph-based Ar-
          gument Processing with Patterns of Acceptance). The implementation
          uses answer set programming encodings to analyze acceptance patterns
          of grappa Systems semantically.
          Keywords. abstract argumentation, abstract dialectical frameworks,
          DIAMOND, answer set programming, clingo, potassco, implementation




1. Introduction

Argumentation is the interdisciplinary study of finding conclusions to premises by
logical reasoning. Computer scientists are concerned with automating this process
in a manner that works quickly and for a wide array of instances. Before devel-
oping an algorithm to solve a problem though, one has to come up with a fitting
representation. In 1995 Phan Minh Dung introduced Argumentation Frameworks
(afs) [1]. They constitute a milestone in the field of argumentation because they
are the first abstract argumentation formalism, very intuitive to use and – as
shown in the initial paper – they are capable to express established mathematical
problems such as the stable marriage problem. afs are graphs, whose nodes depict
arguments. Edges between arguments represent a binary attack relation (aRb :,
a attacks b). Arguments are said to be true, if none of their parents are. Since afs
were introduced, there have been many suggestions for formalisms that cover a
wider array of problem instances. Abstract Dialectical Frameworks (adfs) [2] are
one of them. They feature arbitrary acceptance conditions for nodes, which make
it possible to model support and weak attacks between arguments. Semantics of
af have successfully been generalized for adfs. The complexity of finding models
on those abstracted semantics has been examined in detail [3]. The observations
of this examination are promising, because bipolar adfs (which are special adfs)
are in the same complexity class as afs, while still o↵ering more expressiveness.

Labelled graphs are an often used model in Artificial Intelligence (for example
Bayes Nets of probabilistic reasoning). In 2014 Brewka and Woltran introduced a
variant of adfs – grappa (GRaph-based Argument Processing with Patterns of
Acceptance) [4] – to bring established argumentation semantics to labeled graphs.
                                             52
The diamond System is a collection of tools to calculate models of adfs and
variations of them [5]. The subject of this work is to extend diamond to support
grappa inputs. For this matter we will first define an input format to represent
grappa Systems that is suited to be interpreted by Answer Set Programming
(asp) and easy to use. Secondly we will introduce algorithms that process this
input. Our approach is di↵erent to grappavis [6] – the only other software system
that is able to process grappa inputs. Instead of implementing native algorithms
to find models of grappa Systems we will rely on working adf implementations
in diamond. To do this we will convert grappa Systems into adfs in a for-
mat that is accepted by diamond. As diamond is subject of active development
(as seen in [7]) this approach will vastly reduce the need for maintenance. Any
improvement a↵ecting adf-implementations will directly benefit calculations on
grappa Systems. If for example diamond is extended to be capable of finding
models of new semantics on adfs, there is no need to implement the algorithm
again for grappa Systems.

This paper features a working algorithm that functions as a proof of concept as
well as suggestions for improvements to it.


2. Preliminaries

For subsequent algorithms the background will first be set with intuitions and
some formal definitions of adfs and grappa Systems (Section 2.1), Answer Set
Programming and diamond (Section 2.2). Definitions in Section 2.1 are heavily
based on [2] and [4]. Some concepts have purposely been rephrased to o↵er an
easier overview. In particular the definitions of adfs have been brought in line
with grappa, to make their similarities more obvious. The definition of grappa
acceptance patterns has been changed to fit our implementation better. For more
formal details we direct interested readers to the original sources.

2.1. Formal Background

adfs are argumentation graphs, whose nodes depict arguments with fully arbi-
trary acceptance conditions, represented by propositional formulas.

Definition 1. An Abstract Dialectical Framework is a tuple D = (S, E, ⇡) where

   • S is a set of nodes (statements),
   • E ✓ S ⇥ S is a set of edges (dependencies),
   • ⇡ : S ! F OR assigns propositional formulas to nodes as acceptance con-
     dition. Acceptance formulas of nodes contain all parents of the respective
     node and only those parents as atoms.

Valuations on adfs are partial functions that map nodes to true or f alse. The
option to assign no truth value to a node may be used to model missing knowl-
edge. We will represent valuations conveniently as sets of literals containing ele-
                                        53
ments of S which are evaluated to true unnegated and those evaluated to f alse
negated.

Various semantics capture di↵erent intuitions of what makes a valuation sensible.
Most of them are defined on the characteristic operator , which is a function
that maps valuations to valuations. Intuitively it calculates the acceptance condi-
tion of every node in every extension of its input. A valuation e extends another
valuation v, if e is total and v ✓ e. If there is consensus about the truth value
tv of a node s between all extensions of a valuation v, (v)(s) = tv, otherwise
  (v)(s) is undefined.

Definition 2. Let D = (S, E, ⇡) be an adf and v a valuation on D. We say

   • v is admissible in D i↵ v ✓ D (v),
   • v is complete in D i↵ v = D (v),
   • v is grounded in D i↵ v is the least fixed point of D ,
   • v is preferred in D i↵ v is ✓-maximal admissible in D,
   • v is a model of D i↵ v is total and v = D (v),
   • v is a stable model of D i↵ v is a model of D and v restricted to S v (= v \ S)
     is the grounded valuation of Dv = (S v , E v , ⇡ v ), the v-reduct of D, where
     E v = E \ (S v ⇥ S v ), ⇡ v is ⇡ restricted to S v .

grappa Systems were introduced, to bring adf-semantics to labeled argumenta-
tion graphs. Their only di↵erence to adfs is that their edges have labels which
are incorporated in acceptance conditions of nodes [4].

Definition 3. A grappa is a tuple G = (S, E, L, , ⇡) where

   • S is a set of nodes (statements),
   • E is a set of edges (dependencies),
   • L is a set of labels,
   • : E ! L assigns labels to edges,
   • ⇡ : S ! P L assigns acceptance patterns over L to nodes

Definitions of valuations and semantics on grappa can be directly adopted from
adfs. We will call an edge active in a valuation if its origin is true.

The language of acceptance patterns is specifically designed to make quantita-
tive statements about labels of edges entering nodes. Such a statement may read
“There are more than 3 active ‘+’-links” or “Less than half of all ‘ ’-links are
active”. For labels that are integers we can calculate the sum or the least and
greatest element to make statements such as “The sum of all labels is greater
than 0.”. Because acceptance patterns of nodes are tied to labels, several nodes
might receive the same pattern though they have totally di↵erent parents.




                                        54
Definition 4. Let L be a set of labels.

    • A grappa term over L is of the form:
      min, mint , max, maxt , sum, sumt , count, countt or (#l), (#t l) for arbi-
      trary l 2 L
    • A term (over L) is a grappa term, a constant integer or any arithmetic
      combination of the two using the connectors +, , ⇤, div, mod, exp
    • A basic acceptance pattern1 (over L) is of the form term1 ✓ term2 with
      ✓ 2 {<, , =, 6=, , >} or one of the constants ? (false) or > (true)
    • An acceptance pattern (over L) is a basic acceptance pattern or a Boolean
      combination of acceptance patterns.

The value of grappa terms is determined as follows:

Definition 5. Let G = (S, E, L, , ⇡) be a grappa System. For m : L ! N and
s 2 S the value function valsm is defined as:

   valsm (#l) = m(l)                       valsm (#t l) = |{(e, s) 2 E | ((e, s)) = l}|
 valsm (min) = minm                      valsm (mint ) = min{ ((e, s)) | (e, s) 2 E}
 valsm (max) = maxm                      valsm (maxt ) = max{ ((e, s)) | (e, s) 2 E}
 valsm (sum) = ⌃l2L m(l)                 valsm (sumt ) = ⌃(e,s)2E ((e, s))
valsm (count) = |{l | m(l) > 0}|       valsm (countt ) = |{ ((e, s)) | (e, s) 2 E}|

Here m can assign any integer value to labels. Since we are interested in truth
values of nodes in particular valuations m is usually determined by the number
of active links of a valuation.
Values of terms and patterns are determined inductively as one might expect:

     valsm (term1 + term2 ) = valsm (term1 ) + valsm (term2 )
     valsm (term1     term2 ) = valsm (term1 )      valsm (term2 )
                                ..
                                 .
valsm (pattern1 ^ pattern2 ) = valsm (pattern1 ) ^ valsm (pattern2 )
valsm (pattern1 _ pattern2 ) = valsm (pattern1 ) _ valsm (pattern2 )
                                ..
                                 .




  1 The definition of basic acceptance patterns here has been adapted to fit the grappa repre-

sentation in our implementation better. It has to be noted that it is more general than in [4].
Previously it was not possible to connect two grappa terms directly with operators other than
+ or

                                              55
Example 1
These are an adf and a grappa System representing the same argumentation
structure.

           a            b                           a       +    b

                                                        +
                                                            +

           c            d                           c            d


⇡(a) = >            ⇡(b) = b           8s 2 S : ⇡(s) = (#+ = #t +) ^ (#      = 0)
⇡(c) = a ^ b        ⇡(d) = ¬b

2.2. Technical Background

Answer set programming (asp) is a declarative programming language designed
to represent and solve computational problems easily [8]. It uses logical implica-
tions (rules) to deduce models. Rules that contain no premises are facts. We will
use the phrase “rule” only to refer to implications with premises.
It is hard to draw a line between a program and its input, because asp makes
no di↵erence between the two. What we consider a program usually is a set of
implications that predominantly consists of rules. We will use a set of facts as a
program’s input. Models of the aggregation of a program and its input are sets
of facts as well and function as output.

This paper discusses algorithms detached from their implementation. Thus there
is no need to define the syntax and semantics of asp formally, though we strongly
suggest to read about them in [8]. However here is a quick overview of the syn-
tax of facts: Facts in asp are atoms or predicates. Atoms are strings that start
with a lowercase letter, predicates look the same, but are followed by parentheses
that contain the predicates arguments which may also be atoms. Here are some
examples:

it_is_raining.
is_mortal(socrates).

Facts are confined by dots. Predicates also take functions as arguments, which
again are lowercase strings with parentheses that contain arguments. For example:

is_mortal(father_of(socrates)).

This rudimentary introduction to the syntax of facts is sufficient to explain the
inputs of the diamond System.

The diamond system is a collection of tools that are aimed at computing models
of adfs. It is based on asp and o↵ers five di↵erent input formats to define regular
or special kinds of adfs. The two formats that define regular adfs are: propo-
                                        56
sitional formula representation, extensional representation. Both formats use the
binary predicate l/2 to depict edges of adfs.
The formula representation uses the binary predicate ac(N, ) to associate nodes
N with their acceptance formula . is any logical combination (using the connec-
tives _, ^, !, $, , ¬) of parent nodes and the constants > and ? (represented
by c(v) and c(f)).
In the extensional format the truth value of every valuation is stated explicitly
with the help of ci/1, co/1, ci/3, co/3. The predicates ci/1 or co/1 are used
to describe whether a node is true if none of its parents are. A number of ci/3 or
co/3 predicates that use the same arbitrary index as second argument describe
all the other valuations. The way they work is best seen in an example.

Example 2
These two code examples (propositional representation on the left, extensional
representation on the right) are two ways to describe the example adf of Sec-
tion 2.1 in diamond.
l(a,c). l(b,c). l(b,b). l(b,d).          l(a,c). l(b,c). l(b,b). l(b,d).
ac(a,c(v)).                              ci(a). co(b). ci(b,0,b).
ac(b,b).                                 co(c). co(c,1,a). co(c,2,b).
ac(c,and(a,b)).                          ci(c,3,a). ci(c,3,b).
ac(d,neg(b)).                            ci(d). co(d,1,b).


3. Transformations

Subsequently we will introduce the new grappa representation and processes2
that convert it to an input format of diamond. The algorithm in Section 3.2 pur-
posely includes a minimal amount of modifications that improve running times.
It is a proof of concept and sets an upper bound for complexity.
In Section 3.3 we will introduce variants of this algorithm that are aimed at re-
ducing running times. An empirical evaluation of running times and comparisons
to competing systems are subject of future work, as the implementation of these
improvements are still in development.

3.1. The Input Language

The new grappa representation closely resembles the propositional formula rep-
resentation for adfs. Its advantage is that acceptance conditions can be described
by a single formula tree that fits into a single predicate.

Nodes can explicitly be defined by node/1 which is only necessary if there is no
link entering or leaving the node. Links between nodes are defined by l/3 where
the the first argument denotes the parent node, the third argument denotes the
node the link is entering and the second argument represents the link’s label. Ac-
ceptance patterns are assigned to nodes with the help of predicate gac/2 (grappa
  2 Implementations can be viewed at:

https://sourceforge.net/p/diamond-adf/grappa/ref/master/

                                        57
acceptance condition), where the first argument denotes the node and the second
argument the respective acceptance pattern. The language of acceptance patterns
is described by a context free grammar in Figure 1.

<gac>        ::= gac(<node id>,<sf>).
<sf>         ::= and(<sf>,<sf>) | or(<sf>,<sf>) |
                 imp(<sf>,<sf>) | iff(<sf>,<sf>) |
                 xor<sf>,<sf>) | neg(<sf>) |
                 c(v) | c(f)
<sf>         ::= eq(<t>,<t>) | neq(<t>,<t>) |lt(<t>,<t>) |
                 lte(<t>,<t>) | gt(<t>,<t>) | gte(<t>,<t>)
<t>          ::= plus(<t>,<t>) | minus(<t>,<t>) | times(<t>,<t>) |
                 div(<t>,<t>) | mod(<t>,<t>) | exp(<t>,<t>) |
                 c(<whole number>) | <grappaterm>
<grappaterm> ::= count(<label>) | count_t(<label>) | count |
                 count_t | sum | sum_t | max | max_t | min | min_t
<node id>    ::= <arbitrary (lower case) string (without spaces)>
<label>      ::= <arbitrary (lower case) string (without spaces)>

        Figure 1. The language of acceptance patterns given as context free grammar



Example 3
The following knowledge base describes the grappa System that was given as an
example in Section 2.1

l(a,plus,c). l(b,plus,b). l(b,plus,c). l(b,minus,d).
gac(a,and(eq(count(plus),count_t(plus)),eq(count(minus),c(0))).
gac(b,and(eq(count(plus),count_t(plus)),eq(count(minus),c(0))).
gac(c,and(eq(count(plus),count_t(plus)),eq(count(minus),c(0))).
gac(d,and(eq(count(plus),count_t(plus)),eq(count(minus),c(0))).

3.2. A Full Semantic Analysis

The diamond format we are going to interface with is the extensional representa-
tion. To generate an equivalent adf in this format all we have to do is to calculate
the truth value of acceptance patterns.
grappa acceptance patterns are extensional (the value of a pattern is determined
by the value of its subpatterns). Hence to calculate the truth value of a pattern,
we can resort to classical divide and conquer tactics – break the pattern down
into its components and calculate the value one subpattern at a time. To solve an
acceptance pattern for a specific valuation, we start at the smallest subpattern,
find out its value and work our way up until we find out the value of the main
formula.

Before going up the pattern tree in this manner, we need to break the pattern
down, to form a pattern tree in the first place. Doing this, we need to consider
the kind of value that the subpatterns will hold later. Subformulas hold truth
                                            58
values (true/false) and terms hold integer values. For this reason, both kinds are
represented by two di↵erent predicates gacSF/2 (gac subformula) and gacT/2
(gac term). Their first argument describes the node they belong to and the sec-
ond one their actual form. Subpatterns are broken down into subformulas as long
as their main connectives are logical, subformulas whose main connectives are
comparisons are broken down into two terms and terms are divided until atomic
terms are reached.

Example 4
These are the predicates representing the pattern tree for node d in our example:

gacSF(c,and(eq(count(plus),count_t(plus)),eq(count(minus),c(0)).
gacSF(c,eq(count(plus),count_t(plus))).
gacT(c,count(plus)).                      gacT(c,count_t(plus)).
gacSF(c,eq(count(minus),c(0)).
gacT(c,count(minus)).                     gacT(c,c(0)).

For a node with n parents all 2n valuations are generated, represented by
active/3 predicates. For valuation 0 there are no such predicates, for valuation 1
there is one of them, representing the first parent and so on. For valuation 2n 1
there are n of them representing each node. More generally, for each valuation m
with 0  m  2n 1, the representation of m in binary, (m)2 indicates exactly
which parents of the node are active, namely those whose bit is set in (m)2 .

Example 5
Continuing our running example, the following predicates are generated to rep-
resent the valuations of node c:

active(a,1,c).      active(b,2,c).       active(a,3,c).       active(b,3,c).

The way up the pattern tree begins at the atom level, which are grappa functions
or constants. grappa functions are implemented with their matching aggregation
statements in asp. They use active/3 predicates to determine the value of the
grappa terms in each valuation and put them into gacTV/4 predicates (v for
value).

Example 6
The acceptance pattern’s atoms of node c in valuation 2 receive the following
values:

gacTV(c,2,count_t(plus),2).                  gacTV(c,2,count(plus),1).
gacTV(c,2,count(minus),0).                   gacTV(c,2,c(0),0).

After calculating the value of all grappa term the subpatterns are put back
together respecting the valuation specific value. Each time there is a subpattern
predicate gacT/3 or gacSF/3 of a non-atomic subpattern SP and a value holding
predicate gacTV/4 or gacSFV/4 for both children of SP a value holding predicate
for SP respecting the arithmetic or truth function of the main connective of SP is
generated. For example the connective and/2 is implemented in this way: If both
children of the and/2 connective hold value true, their conjunction will as well.
                                        59
If at least one child holds value false, the conjunction will be false as well. The
other connectives are handled analogously.

Example 7
This process generates the following new predicates for node c, valuation 2 in our
example:

gacSFV(c,2,eq((count(plus),count_t(plus)),false).
gacSFV(c,2,eq((count(minus),c(0)),true).
gacSFV(c,2,
  and(eq((count(plus),count_t(plus)),eq((count(minus),c(0)),false).

After the pattern is put back together to its original form, the output for the dia-
mond System is generated. For each valuation there exists a number of active/3
predicates. Depending on the truth value of the overall pattern under a respect-
ing valuation, for each of those active/3 predicates a co/3 or ci/3 predicate
is generated. For the first valuation there is no active/3 predicate (because all
parents are not active), so the parent node independent predicate co/1 or ci/1
is generated.

Example 8
Node c is false in valuation 2, where there is one active node: a, thus the following
output is generated:

co(c,2,a).

The calculation of each node’s models is done entirely hermetically. Hence we can
consider which factors scale the running time for each node independent of all the
other nodes. For the complexity there are two factors to be considered. On one
hand the running time scales with the length of acceptance patterns, on the other
with the number of parent nodes. For each connective in the acceptance pattern
there is one more subpattern that needs to be looked at on the way down and up
the pattern tree, i.e. the running time scales linearly with the number of connec-
tives of the acceptance pattern. For n parent nodes 2n valuations are generated
and evaluated, i.e. running time scales exponentially with the number of parent
nodes. Brewka and Woltrand observed a similar blowup in their transformation
from grappa Systems to adfs [4].

3.3. Improvements – A Partial Semantic Analysis

In the algorithm of Section 3.2 for each possible valuation of a node the value of
the overall pattern was calculated, to explicitly transfer all models to diamond.
This approach is very complex, as the number of valuations scales exponentially
with the number of parent nodes. For some instances we might be able to reduce
the complexity significantly. Consider the following example:

l(p1,plus,a). l(p2,plus,a). . . . l(p50,plus,a).
l(m1,minus,a). l(m1,minus,a). . . . l(m50,minus,a).
gac(a,and(eq(count(plus),count_t(plus)),eq(count(minus),c(0))).
                                         60
a has 100 parents. A full semantic analysis evaluates 2100 valuations while the
first and second conjunct actually are entirely independent of each other – they
depend on disjoint sets of nodes. Separating the evaluation into two groups would
dramatically reduce the number of valuations to be considered to 250 +250 (= 251 ).

In order to achieve this separation we do the following: We apply the previous
algorithm on each of the basic acceptance patterns (bap) separately under con-
sideration which parent nodes they depend on. A bap depends on the aggregation
of parents its leaves depend on: count depends on all parents. count(l) depends
on all l-parents. min, max and sum depend on parents whose links have integers
as labels. The terms count_t(l), count_t, min_t, max_t and sum_t have no
dependencies, as their values are fixed.

An implementation3 that generates propositional formulas in dnf from this in-
formation has been tested and observed to run into some obstacles. asp does not
perform well on deep predicates, which is exactly what needs to be generated
when constructing a dnf. As using the extensional interface is no option either,
all chances to feed the information received from this process into diamond are
depleted. The conclusion of this paper will feature a number of suggestions for
future input formats of diamond one of which is especially suited to handle this
problem.


4. Conclusion and Future Work

This paper o↵ers a new approach to analyze grappa Systems – to rely on ex-
isting algorithms that solve adfs. The algorithms introduced in this paper are
a first step toward a fast conversation from grappa System to adfs. The first
one (a full semantic analysis) is designed as a proof of concept and has a working
implementation. The second one (a partial semantic analysis) which is based on
the first one, is a suggestion on how to reduce the complexity. To make use of it
we suggest an input format similar to the propositional formula format, where
the formula tree of a acceptance formula is represented by several predicates that
are flat. A similar variant of the here newly defined grappa format should also
be added.

Furthermore it should be a goal to adapt principles of special adfs to grappa
Systems – bipolar grappa representation and priority based grappa represen-
tation being two of them. An implementation that converts them to their adf-
counterparts would complement the diamond System.

Adding interfaces to diamond that use the same language as grappavis would
o↵er a common ground for benchmarks.



  3 It can also be found at: https://sourceforge.net/p/diamond-adf/grappa/ref/master/


                                          61
References

[1]   Phan Minh Dung. On the acceptability of arguments and its fundamental role in non-
      monotonic reasoning, logic programming and n-person games. Artif. Intell., 77(2):321–358,
      1995.
[2]   Gerhard Brewka, Hannes Strass, Stefan Ellmauthaler, Johannes Peter Wallner, and Stefan
      Woltran. Abstract dialectical frameworks revisited. In Francesca Rossi, editor, IJCAI 2013,
      Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing,
      China, August 3-9, 2013. IJCAI/AAAI, 2013.
[3]   Hannes Strass and Johannes Peter Wallner. Analyzing the computational complexity of
      abstract dialectical frameworks via approximation fixpoint theory. Artif. Intell., 226:34–74,
      2015.
[4]   Gerhard Brewka and Stefan Woltran. GRAPPA: A semantical framework for graph-based
      argument processing. In Torsten Schaub, Gerhard Friedrich, and Barry O’Sullivan, editors,
      ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014,
      Prague, Czech Republic - Including Prestigious Applications of Intelligent Systems (PAIS
      2014), volume 263 of Frontiers in Artificial Intelligence and Applications, pages 153–158.
      IOS Press, 2014.
[5]   Stefan Ellmauthaler and Hannes Strass. The DIAMOND system for computing with ab-
      stract dialectical frameworks. In Simon Parsons, Nir Oren, Chris Reed, and Federico
      Cerutti, editors, Computational Models of Argument - Proceedings of COMMA 2014, Atholl
      Palace Hotel, Scottish Highlands, UK, September 9-12, 2014, volume 266 of Frontiers in
      Artificial Intelligence and Applications, pages 233–240. IOS Press, 2014.
[6]   Georg Heißenberger. A system for advanced graphical argumentation formalisms. Master’s
      thesis, TU Wien, 2016.
[7]   Stefan Ellmauthaler and Hannes Strass. DIAMOND 3.0 – A native C++ implementation
      of DIAMOND. In Pietro Baroni, editor, Proceedings of the Sixth International Conference
      on Computational Models of Argument (COMMA), Frontiers in Artificial Intelligence and
      Applications, Potsdam, Germany, September 2016. IOS Press.
[8]   Martin Gebser, Benjamin Kaufmann, Roland Kaminski, Max Ostrowski, Torsten Schaub,
      and Marius Thomas Schneider. Potassco: The potsdam answer set solving collection. AI
      Commun., 24(2):107–124, 2011.
[9]   Stephen C. Kleene. Introduction to Metamathematics. D. Van Nostrand Company, Prince-
      ton, New Jersey, 1952.




                                                 62

</pre>