=Paper=
{{Paper
|id=Vol-2090/AIC17_paper7
|storemode=property
|title=On Proving and Argumentation
|pdfUrl=https://ceur-ws.org/Vol-2090/paper7.pdf
|volume=Vol-2090
|authors=Sofia Almpani,Petros Stefaneas
|dblpUrl=https://dblp.org/rec/conf/aic/AlmpaniS17
}}
==On Proving and Argumentation==
<pdf width="1500px">https://ceur-ws.org/Vol-2090/paper7.pdf</pdf>
<pre>
                          On proving and argumentation

                                 Sofia Almpani1 and Petros Stefaneas2
                             1
                              National Technical University of Athens,
                                        salmpani@sch.gr,
                          2
                            National Technical University of Athens,
                                       petros@math.ntua.gr

          Abstract
          In this paper, we demonstrate how argumentation theory can be used to explore cer-
tain aspects of the development of discovery proof-events in time. The concept of proof-event
was introduced by Joseph Goguen, [10], who understood mathematical proof, not as a purely
syntactic object, but as a social event, that takes place in specific place and time and involving
agents or communities of agents. Proof-events are sufficiently general concepts that can be used
to study besides the “traditional” formal proofs, other proving activities, such as incomplete
proofs, purported proofs or attempts to verify a conjecture. Since argumentation is inseparable
from the process of searching for a mathematical proof, we suggest a modified model of the
proof-events calculus, initially suggested by Vandoulakis and Stefaneas [32], based on the
versions of argumentation theories advanced by Pollock [26], Toulmin [28] and Kakas and
Loizos [14]. We claim that the exchange of arguments and counterarguments set forward to
clarify eventual gaps or implicit assumptions occurring in the course of a proof-event can be
formalized by appealing to argumentation theories. Additionally, we highlight the connection
between proving, human reasoning, cognitive processes and creativity.

        Keywords: proof events, argumentation, proving


              Introduction
          The concept of mathematical proof has undergone significant changes in the
20th century. Proof, particularly formalized proof, was initially identified in philoso-
phy of mathematics with truth. However, many mathematicians dealing with real
proofs did not accept the paradigm of formalized proof. Goguen [10] suggested the
broader concept of proof-event, which is actually a social event that takes place in
specific place and time and involves public communication. The concept of proof-
event is designed to embrace any proving activity, such as incomplete proofs or at-
tempts to verify a conjecture. Vandoulakis and Stefaneas [31] described proof-events
as activity of a multi-agent system incorporating their history, insofar as they form
sequences of proof-events evolving in time. Thus, they modelled certain temporal
aspects of proof-events, using the language of the calculus of events developed in
Kowalski’s and Event Calculus [19].
          Our approach combines proof-events with logic-based argumentation to study
in a more adequate way the categories of purported, faulty or incomplete proofs, setting
forward the concept of dialogue between agents with the use of arguments and counter-
arguments. Hence, we extend the calculus of proof-events through argumentation theory
by depicting the relevant stages of a discovery proof-event (incomplete or even false
proofs, ideas, valid or invalid inference steps, comments, etc.) in a form of a dialogue of
agents that use arguments and counterarguments or counterexamples in their attempt to
clarify the validity of a purported proof.
          Many researchers claim that the role of argumentation is central in mathe-
matics. Mathematicians do much more, than simply prove theorems. Most of their
proving activity might be understood as kinds of argumentation [2]. Lakatos’ Proofs
and Refutations [20] is an enduring classic that highlights the role of dialogue be-
tween agents [a teacher and some students) by attempts at proofs and critiques of
these attempts. The comparison between argumentation supporting an assumption or a
purported proof and its proof is based on the case that proof can be regarded as a spe-
cific argumentation in mathematics [22].
          A methodological tool that has been widely used to examine argumentation
is Toulmin’s model [28], in which argument is constituted by “claim”, “data”, and
“warrant” that are considered the substantial elements of applied arguments. The pro-
cedure by which mathematicians evaluate reasoning resembles to argumentation, as
various researchers, such as Alcolea [6], Aberdein [0], Pedemonte [22,23], Aberdein,
Dove [4] tried to show by adapting Toulmin’s model to mathematical examples. We
propose to integrate argumentation theory into the calculus of proof-events. By doing
so, we can depict all the relevant stages that we go through when proving, from the
statement of a problem until its validation or rejection by the relevant community that
uses arguments and counterarguments or counterexamples in checking the validity of
a purported proof.
          To combine the proof-event calculus with argumentation theory, we use the
basic structure of Toulmin’s model for the representation of an argument and Pol-
lock’s logic-based argumentation theory. We rely on Pollock’s view of defeasible
reasoning and we associate the procedure of human reasoning with proving. Defeasi-
ble reasoning has a non-monotonic character. Pollock presented in his work the con-
cept of an argument in the form <Φ,α>, where Φ is a set of data and α is a claim [25].
He separated the rebutting and undercutting defeat and presented one of the first
monotonic logics with concepts of argument and defeat, even though he did not ex-
plicitly distinguish between them [24].
          In this paper, we proceed from a comparison of proof-events and argumenta-
tion. Then, we suggest a formalization of proof-events involving argumentation theo-
ry. We model the argument moves and the calculus of the temporal predicates. The
aforementioned calculus is analyzed through the levels of argumentation. In the last
section, Fermat’s Last Theorem as a proof-event is investigated as a case study illus-
trating the concepts introduced.

         1. Proof-events vs. arguments.
     Comparison of the basic elements of proof-events and argumentation theory
shows similarities in the structure, the sequence of events, the agents, the layers of
communication, and the levels of argumentation.
     Arguments and proof-events have three common fundamental components: a set
of premises for a task or problem, a method of reasoning and a conclusion. Moreover,
each proof-event has temporal extension and, thereby history: it has a starting point
and a termination point and what is posed to be proved, emerges often out of the his-
tory of provings (sequences of proof-events or sequences of arguments and counterar-
guments) [31]. A sequence of a proof-event is complete when the community in-
volved in it concludes that they have understood the proof and agree that a proof has
actually been given or that a proof is invalid, based on a suggested counterargument
(or counterexample).
     Proof-events presuppose the existence of at least two agents: a prover and an in-
terpreter [31]. Similarly, argumentation involves agents or group of agents, enacting
the roles of supporter and opponent of an argument [17]. The layers of communica-
tion, understanding, interpretation, and validation that agents use to disseminate their
knowledge, are common in both approaches. An agent is a proactive and intelligent
system that enacts a specific role. We may consider some software systems as agents,
if they possess these characteristics. Argumentation has encouraged its adoption as a
technology for multi-agent systems developments. The main concept advanced in
agent-based approaches is that of autonomy: agents operate as independent individual
entities trying often to collaborate and coordinate with others [13]. However, the steps
that an individual agent wants to perform in order to accomplish a mathematical proof
may interfere with the steps attempted or already performed by other agents. A num-
ber of significant questions appear from these processes of inter-agent debates, such
as the systematization of atomic agent contributions as phases in a goal-directed plan
(such as proving) and the review in the formalization of logic-based languages in
terms of both syntactic and semantic aspects [16].

    2. Argumentation models
     Argumentation models generally contain the following main elements: an under-
lying logical language with the definition of the concepts of argument, conflict be-
tween arguments and counterarguments, and status of argument. We will outline for-
malizations of proof-events based on argumentation theory, using a list of structures,
which represent arguments and counterarguments. Our approach suggests a multi-
agent system, enacting the roles of provers and interpreters. An argument has premis-
es, sentences, and conclusion. In the definition of an argument given in this section,
the knowledge grounds and claims are formulae in classical logic and the method of
inference by which a claim follows from a set of formulae is deductive inference and
is denoted by ⊢. A proof-event е can be represented as a communicated argument
〈     〉 [26] designated by the pair 〈       〉:
                                                                  ,
    where Φ is the Data of the argument, c is the Claim that refers to a fixed problem
(proposition), specified by certain conditions (predicates) and w are the inference
rules (Warrant) which allow Φ to be connected with c, so that:
     •
     •        ⊢
     •                                          ⊢ c.
    Counterarguments are represented by the corresponding pair                , where Ψ
is the data that the claim β (that refers to the same fixed problem (proposition), speci-
fied by the same conditions (predicates)) of the counterargument is based.
          Argumentation may require chains (or trees) of reasoning, where claims are
used in the assumptions for obtaining further claims [8], so that a proof-event could
be an atomic argument or a sequence of arguments (fluent). Fluents f are sequences of
proof-events (proving instances) evolving in time that refer to a fixed problem, speci-
fied by certain conditions [30]. Let R be a set of rules of inference. A fluent f is a
formula of the form e1,e2,e3 →e, where 〈             〉, 〈      〉 〈         〉 is a finite,
possibly empty, sequence of arguments, such that the conclusion of proof-event ei is
the claim ci, i.e.:                                                    for some rule
          →        [33]. Accordingly, the meaning of the three substantial components
of the argument based on Toulmin’s model [28], which abbreviated by corresponding
prefixes, are defined as follows for the notion of fluent:

                                                                                     (1)
                                                                                     (2)
                                                                                     (3)

   where:
   c (Claim): the statement communicated by the speaker.
   Φ (Data): facts as the ground of the claim.
   w (Warrant): the inference rules, which allows data to be connected to the claim.
     The aforementioned elements are frequently used to define a consequence rela-
tion between the arguments and/or the counter-arguments.

     2.1 Argument moves
          In the course of a proving procedure, we pass through various inference
stages, such as attempts, impasses, confirmed or unconfirmed steps, false suggestions
or implicit assumptions, intuitive ideas, intentions, etc. Arguments can then be speci-
fied as chains of reasoning leading to a conclusion with consideration of possible
counterarguments at each step. With the explicit construction of the chain of reason-
ing (a chain x0, x1,.. , xn where the argument xi attacks the argument xi−1 for i > 0),
distinct concepts of defeat can be conceptualized. When an agent has gained control
of an argument, he must select which argument-move to apply. Gordon [11] refers to
“argument moves” as analogs of three roles for legal cases. This term was also previ-
ously used by Rissland [27], Asley and Aleven [7], Pease et al [21]. We reserve the
term “argument moves” for specific, active tactics or strategy that a prover can choose
to support his claim. We present four fundamental relations that indicate links and
conflicts at the sequence of proof-events. The possible argument moves could provide
support or attack the claim.
          Given a claim c and and an argument communicated during the proof-event
e, possible argument moves, which provide support for c [12] include:
   Equivalent: an argument for a claim, which is equivalent to (or is) c;
   Elaboration: an argument for an elaboration of c, and
          Argument moves, which oppose c [26] include:
   Rebutting: an argument for a claim which disagrees with c;
   Undercutting: an argument for a claim which disagrees with a premise of c.

  2.1.1. Argument moves that support the claim:

                                                                                     (4)

  when Φ=Φ΄, c=c΄ (although it might be w≠w ),
   where the proof-event e1 is equivalent with the proof-event e2, whenever it has the
same data and the same conclusion (although different warrants). Thus, equivalent
proof-events can have different ways of proving. For instance, the Pythagorean Theo-
rem has been proved in numerous ways, such as by Euclid’s geometrical proving or
by James Abram Garfield algebraic proving.
                                                          →           ,            (5)

   where 〈       〉, is a proof-event and S is a set of sentences which elaborate or em-
bellish upon e, iff        ⊢ .
   These moves are used for backing our claim and supporting our proving, so that
                             →                                                     (6)

  2.1.2. Counterargument moves that attack the claim:
                                                    →                              (7)

    where a counterargument communicated during the proof-event e*<Ψ,β> attacks
(rebuts) the conclusion of an argument communicated during the proof-event e<Φ,c>,
iff ⊢β ↔ ¬c,
                                                     →                         (8)

   where a counterargument communicated during the proof-event e*〈           〉 under-
cuts (attacks) some of the premises (defeasible inference) of the argument communi-
cated during the proof-event 〈     〉, iff ⊢ ↔                      {          }
          Given an argument communicated during the proof-event e<Φ,c>, a coun-
terargument communicated during the proof-event e* 〈           〉attacks the argument
communicated during the proof-event e, at time t, iff e* rebuts e or e* undercuts e.
Therefore:
                                →                                                 (9)

   2.2 Temporal predicates
     Even though proof-events can be regarded as taking place instantaneously, the
Event Calculus is actually neutral with respect to whether events have duration or are
instantaneous [19]. RAC is concerned with the study of how fluents change when new
information is acquired and how this view of the problem is affected by the observa-
tion of some events remaining active or terminated at a particular time. The language
in RAC [16] uses causal propositions (c-propositions), of the form “A initiates F
when C” or “A terminates F when C”, which in this paper are represented in more
detailed and specific form with the arguments’ and the counterarguments’ moves that
initiate or terminate a fluent. In most cases, we will take into consideration only the
starting point of a proof-event, with the exception of those proof-events that termi-
nate, or when duration plays a significant role. In these cases, we mention both the
starting and termination points.
     We apply the abovementioned operators combined with the basic temporal pred-
icates from [32]: Happens(e,t),Initiates(e,f,t), Terminates(e,f,t), ActiveAt(f,t),
Clipped(t1,f,t2.)
            Happens(e,t), which means that a proof-event e occurs at time t.         (10)
                              t1               t1 →              t1
                                              t1                                     (11)
                                              t1

which means that if a proof-event e occurs at time t, then there are no counter-
arguments that attack the validity of the outcome of the proof-event and there is ade-
quate support for our claim at the specific time t1.
                  (            )   e1       t1 [
                       ]   [            (               →                  )]        (12)


which means that a proof-event clips when there is no proof-event e2 that attacks the
counter-argument attacking the proof-event e1 between t1 and t2.
                                          [               →
                       ] [ (                     →                  )]           (13)


which means that a fluent terminates when there is a counterargument attacking our
sequence and there is no proof-event e2 that Happens in time t2, with t1<t2, to defend
our claim. The termination of a sequence of proof-events may be caused by the proof
of the falsity of the problem (there are counter-arguments that attack the conclusion of
the proof-event), or the undecidability of the problem (there is a lack of adequate
warrants to prove the desideratum).

                                                        →
                                                                                     (14)

  which means that a fluent is active, if there is an argument to support our claim for
every counterargument attacking our claim,. This means that for every counterargu-
ment e*<Ψi,βi>, i= 1,…,n, nϵ , there is a proof-event en+1(Φn+1, cn+1), which Hap-
pens(en+1,tn+1) and defeats the attack of the counterargument en*<Ψn,βn>, for tn+1>tn.
         From the above-mentioned, we can conclude that:
                                                                                     (15)
                           →

   which means that a fluent remains active at time t2, if a proof-event e has taken
place at time t1, with t1<t2 and has not been terminated at a time between t1 and t2.
                  [                                                          ]
                                                                                      (16)
                              →

   which means that a fluent could consider valid at time tn, if it is active and there is
no counter-arguments to terminate it at time ti for every i=1,…,n, nϵ .
            3. Levels of argumentation
     In order to define the warranted premises that are justified by a set of arguments
in the sequence, we need a mechanism, which by recursion could examine the repre-
sentation of the arguments. Pollock introduces defeasible reasoning where arguments
are chains of reasoning that may lead to a conclusion, whereas additional information
may destroy the chain of reasoning. Kakkas and Moraitis [17] presented three levels
of arguments: Object level arguments, which represent the possible decisions or ac-
tions in a specific domain. First-level priority arguments, which express justifications
on the object-level arguments in order to resolve possible conflicts. Then, higher-
order priority arguments are used to deal with potential conflicts between priority
arguments of the previous level until all conflicts are resolved.
          We can apply the same levels in mathematical proving, in order to under-
stand the history of proof-events, starting from the statement of a problem until its
validation or rejection, including attempts or failures [32]. The data and the claim of
the initial proof-events constitute the object-level arguments. Proof-events constitute
the first-level priority arguments, in which we have preferences and justifications in
the object-level arguments. The proof-events that have fulfilled their purpose termi-
nate, while the rest of them continues to the higher-order priority arguments. As
proof-events continue from lower levels to higher, they constitute fluents. In the ex-
ample below, we describe the possible steps and conflicts for the justification of a
proof-event e through the levels of argumentation.

  Object level arguments
                                                                                   (17)

                  [                      →                             ]
                                                                                   (18)
                                   →
   for i=1,….,m, mϵ , t i ≤t m <t.
         In the object level arguments, we have our claim and the initial representa-
tions of arguments. The proof-events that are not attacked constitute the fluent fo and
continue to the first level priority arguments.

  First-level priority arguments


                                                                                   (19)
                                                                t,
  for every iϵ    that we have:
                                [
                                 →                                   ]
                               [                                                   (20)
                         →                        ]
                         →                                  ]
    so that the proof-events that have been attacked and could not resolve the conflict,
terminate in this fluent. The rest of them remain active, so we have:
                                                             ≠                      (21)
and continues to the second-level priority arguments.
          The same pattern continues for n-level priority arguments and for n fluents fn,
that deal with potential conflicts between priority arguments of the previous level until
all conflicts are resolved or our claim proved invalid. In the final level we have:

    Higher-order priority arguments
    If the proof-events fail to resolve all the conflicts, our claim cannot be proved and
it clips:
                                                                                     (22)

  If the proof –events manage to deal with all the attacks and:
                 [         (                 )                               ]→
                                                                                     (23)
                                                                     ,
   then our claim is proved valid .

            4. An example using the Fermat’s Last Theorem

          We use the famous Fermat’s Last Theorem to illustrate our approach. Fer-
mat's Last Theorem was formulated in 1637 by Pierre de Fermat, who stated that there
are no three distinct positive integers a, b, and c, other than zero, that can satisfy the
equation an+bn=cn , whenever n is an integer greater than two (n> 2). The statement of
the problem marks the starting-point of a proof-event. Even though Fermat claimed to
have proved this theorem, it actually took 358 years and numerous attempts undertak-
en by many famous mathematicians and amateurs to prove it until its final proof by
Andrew Wiles in 1995. Thus, Fermat’s alleged proof cannot be included in the initial
proof-event, since it was never communicated. Fermat communicates the Theorem
only for the cases n=3 and n=4 in his letters and gives a solution for the latter case.
The statement of the problem marks the beginning of a sequence of proof-events that
evolved in time for 358 years. This sequence of proof-events was evolving in time,
since many famous mathematicians and amateurs (agents) were involved in various
distinct proof-events that took place in different places and times in their attempt to
solve the problem posed.
          We cannot expose here the whole sequence of such proof-events. We confine
ourselves to select some of these historical attempts (proof-events) until the proof-
event that includes the communication and validation of the final proof of the theorem
and demonstrate how argumentation is involved in the process of search for proof.
          The first attempts to prove the Theorem were proofs for specific exponents.
The case n = 3 was first explored by Abu-Mahmud Khojandi (c. 940 - 1000), but his
attempt has not survived (and thereby cannot be considered as a proof-event) and it is
conjectured that it was incorrect. Leonhard Euler gave a proof for n = 3 in 1755 and
for n=4 in 1747, but his proof of the former case contained a basic fallacy [9, p.39-
40]. Many other mathematicians proved the theorem for n=3 using various methods.
Gabriel Lamé (1795 –1870) proved it for the case n = 7. In 1847, he communicated a
proof of the Theorem, but it was flawed. Gabriel Lame’s proof failed because it was
claimed incorrectly that complex numbers could be factored into primes uniquely.
This gap was indicated instantly by Joseph Liouville [9, p.76-77]. In 1984, Gerhard
Frey pointed out a connection between the modularity theorem and Fermat’s equa-
tion, but Fermat’s Last Theorem remained to be a conjecture. The Taniyama-
Shimura-Weil conjecture, which was proposed in 1955, was the method that led to a
successful proof of Fermat’s Last Theorem, when Andrew Wiles accomplished a
partial proof of this conjecture in 1994 [29].
           Wiles, after spending six years applying various methods that were proved
unsuccessful, he approached the problem in a new way. He decided to present his
work in June 1993 at the Isaac Newton Institute for Mathematical Sciences [29].
           However, during the peer review, it became evident that there was an incor-
rect critical point in the proof. Wiles tried almost a year to resolve this point, firstly by
himself and then in collaboration with Richard Taylor, but without success [18].
When Wiles was on the verge to quit his attempt, he experienced an insight that the
Kolyvagin–Flach approach and Iwasawa theory were each insufficient on their own,
but in combination they could be strong enough to overcome this final barrier. In
1994, Wiles submitted two papers that established the modularity theorem for the case
of semistable elliptic curves, which was the last step in proving Fermat’s Last Theo-
rem [29].
           This example illustrates the contribution of the agents in the process of prov-
ing. Firstly, the central aim of the proving itself is to convince the rest of the commu-
nity about the justification and the validity of your approach. Moreover, the other
agents also contribute significantly in the procedure. So many people had to partici-
pate in order to reach the initial goal, which was the proving of the Fermat’s Last
Theorem. This participation is depicted with two ways, either with the rejection of
someone else’s attempt by pointing out a fault and/or inaccuracy (ex. Liouville indi-
cated Lame’s gap concerning complex numbers) or with the dialogue between coop-
erators in order to detect and resolve weak or deficiently supported areas in the prov-
ing (ex. Wiles asked other colleagues’ help, like Richard Taylor, whenever he found a
dead-end or fault in his attempt). Argumentation is more efficient in more interactive
contexts, as they let counterarguments to be addressed and stronger arguments to
surface. An audience with mainly common beliefs will generate less differentiated
counterarguments, making them easier to address. Thus, a mathematician is in a fa-
vored position if he wants to ask the assistance of a few colleagues in order to point
out most of the possible counterarguments and resolve them in the final proof. By
doing this, the proving could be more convincing not only to these few colleagues,
but probably to the whole community.
           The arguments and the counterarguments also play an essential role in the
process of proving, contributed equally in the building and the justification of the
proving. The warranted parts of the initial provings acted as a groundwork for the
next provings, while the counterarguments that signalize the faults in those unsuccess-
ful provings open the way for better justified provings and in some cases turn the
interest of the mathematical community in new unexplored areas. Those incomplete
provings may add more or less to the proof of Fermat’s Last Theorem, but the meth-
ods that were created with them lead to major discoveries and creation of new fields
in the era of Mathematics like the foundation of modern algebra. Discoveries that are
even more significant than the proving of the theorem itself and might have not been
found if it weren’t for the warranted proof-events and the counterarguments emerged
from the previous attempts of proving.
          In the next part we present a brief representation of this example through the
                         1
levels of argumentation .

   Object level arguments – Fermat’s Conjecture
         In the object level arguments, we have Fermat’s conjecture as the initial
proof-event           and his claim that he has a proving for this conjecture, without
any claim-counterargument             clearly opposes this conjecture.
                                                                 →

   First-level priority arguments - Proofs for specific exponents
         In the first-level priority arguments, we have proofs for specific exponent n
of the Fermat’s Last theorem from various mathematicians in different time points.
  For the exponent n=3 (en=3), Leonhard Euler (                      ) gave a proof in 1755, so we
have:                            .
Many other well-known mathematicians followed with equivalent proofs that support
the validity of the proof for n=3. Each prover used a different way (warrant) for prov-
ing the conclusion, so their provings are equivalent.
                                    →                                , for i=1,…,14 with:
i=1:(e Euler ,t 1707 ), i=2:(e Kausler ,t 1802 ), i=3:(e Legendre ,t 1823 ),    i=4:(e Calzolari ,t 1855 ),
i=5:(e Lame ,t 1865 ), i=6:(e Tait ,t 1872 ), i=7:(e Gunther ,t 1878 ).
                                                                        [
                       ]                   →                                , for t1755<ti
    Fermat’s Last Theorem was also proved for the exponents n = 5, 6,7, 10, and 14.

   Second-level priority arguments – Lame’s Proving
          In 1847, Gabriel Lame’s proving (eLame) failed because it claimed incorrectly
that complex numbers can be factored into primes uniquely. This gap was indicated
instantly by Joseph Liouville (eLiouville*).
                                 [                         →                 ]

              [                                         →                                     ]
                                →

  Third-level priority arguments – Andrew Wiles
     Andrew Wiles presented his work in June 1993, but it became evident that there
was an incorrect critical point (eWiles*) in the proving. Wiles tried almost a year to

1
  Names of provers and dates are taken from Wikipedia «Fermat’s Last Theorem». Retrieved from:
https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem]
resolve this point, firstly by himself and then with the contribution of Richard Taylor,
but without success.

                                    [
                                        ]    [                                →
                                            ]                        .

     Finally, in 1994, Wiles submitted two papers that combined Kolyvagin–Flach
approach and Iwasawa theory which was the last step in proving Fermat's Last Theo-
rem.
                                                      →


  Higher-order priority arguments-Fermat’s Last Theorem
  The proof–event managed to deal with all the attacks and we have:

                                                                               ]→
                                                       ),
   at the time t1994.
   Thus, Fermat’s Last Theorem is proved valid by Wiles, with the contribution of the
other agents that opened the way before him in this ages-long sequence of proof-events.

            5. Conclusion
          We have developed a model of the proof-events calculus [32] based on Pol-
lock’s [26], Toulmin’s [28] and Kakas’ argumentation theories, extending the proof-
events calculus with the integration of arguments and counterarguments. The combina-
tion of Vandoulakis’s and Stefaneas’s proof-events-based theory and logic-based argu-
mentation has the advantage of highlighting weak areas in a proof. Proof-events are not
considered as infallible facts before their ultimate validation, thus enabling the explora-
tion of flawed approaches and proofs to be found and resolved. We focused on the con-
nection between proving, human reasoning, cognitive processes and creativity. We
presented a calculus for the proof-event argument, argument moves, and temporal pred-
icates and we analyzed them in terms of levels of argumentation. The calculus adds an
additional dimension and performs a significant role in making these connections suffi-
ciently detailed and specific. In our future work, we can apply this model to express the
proof-events sequence and history in specific examples of mathematical proving, as in
the example of Fermat’s Last
    References
1. Aberdein Andrew, (2005), “The Uses of Argument in Mathematics”. Argumentation 19: 287–
   301.
2. Aberdein Andrew, (2008), Mathematics and argumentation. Netherlands, Kluwer Academ-
   ic Publishers.
3. Aberdein Andrew, (2009), “Mathematics and argumentation”. Foundations of Science
   14(1–2):1–8.
4. Aberdein Andrew, Dove Ian J. (Eds.). (2013). The argument of mathematics. Dordrecht:
    Springer.
5. Aczel Amir D. (1996) Fermat's Last Theorem: Unlocking the Secret of an Ancient Math-
    ematical Problem. New York: Dell Publishing.
6. Alcolea Banegas, J. (1998), “L’Argumentació en Matemàtiques”. E. Casaban i Moya (ed.),
    XIIè Congrés Valencià de Filosofia. Valencià, 135–147.
7. Ashley K.D., Aleven V., (1991), “A Computational Approach to Explaining Case-Based
    Concepts of Relevance in a tutorial Contect”. Proc. Case-Based Reasoning workshop,
    Washington, 257-168
8. Besnard Philippe and Hunter Anthony, (2008), “Elements of Argumentation”. The MIT
    Press Cambridge, Massachusetts London, England.
9. Edwards Harold M. (1977) Fermat’s Last Theorem. Springer.
10. Goguen, Joseph, (2001), “What is a proof”, http://cseweb.ucsd.edu/~goguen/papers/proof.html
11. Gordon T. F., (1991), “An abductive theory of legal issues”, International Journal of
    Man-Machine Studies, 35(1):95-118.
12. Haggith, M. (1996), “A meta-level argumentation framework for representing and reason-
    ing about disagreement”. Ph.D. thesis, Dept. of Artificial Intelligence, University of Edin-
    burgh.
13. Kakas A.C., Kowalski R.A., Toni F., (1992), “Abductive logic programming”, J. Logic
    Comput. 2 (6): 719–770.
14. Kakas Antonis, Loizos Michael, (2016), “Cognitive Systems: Argument and Cognition”.
    IEEE Intelligent Informatics Bulletin, 17(1): 15-16
15. Kakas Antonis, Loizos Michael, Toni Francesca, (2016), “Argumentation: Reconciling
    Human and Automated Reasoning”. Proceedings of the Workshop on Bridging the Gap
    between Human and Automated Reasoning, New York, USA.
16. Kakas A., & Miller R. (1997). “A simple declarative language for describing narratives
    with actions”. Journal of Logic and Algebraic Programming, 31, 157–200.
17. Kakas Antonis C., Moraitis Pavlos, (2003), “Argumentation based decision making for
    autonomous agents”. In: Proc. Second International Joint Conference on Autonomous
    Agents & Multiagent Systems, AAMAS 2003, Melbourne, Australia, 883–890.
18. Kolata Gina, (1994), A Year Later, Snag Persists in Math Proof, Published: June 28, 1994,
    http://www.nytimes.com/1994/06/28/science/a-year-later-snag-persists-in-math-proof.html
19. Kowalski Robert, (1992), “Database updates in the event calculus”. The Journal Of Logic
    Programming, Elsevier Science Publishing Co., Inc., 12:121-146.
20. Lakatos, I. (1976), Proofs and Refutations. Cambridge, Cambridge University Press.
21. Pease Alison, Smaill Alan, Colton Simon, Lee John, (2008), Bridging the gap between
    argumentation theory and the philosophy of mathematics, Kluwer Academic Publishers.
22. Pedemonte, B. (2007). “How can the relationship between argumentation and proof be
    analyzed?” Educational Studies in Mathematics, 66: 23–41.
23. Pedemonte B. (2008), “Argumentation and algebraic proof”. ZDM Mathematics Education, FIZ
    Karlsruhe, 40:385–400.
24. Prakken Henry, Horty John, (2012), “An appreciation of John Pollock’s work on the com-
    putational study of argument”, Argument & Computation. 3:1-19.
25. Pollock J. L. (1987), “Defeasible reasoning”. Cognitive Science, 11:481–518.
26. Pollock J. L. (1992), “How to reason defeasibly”. Artif. Intell., 57(1):1–42.
27. Rissland E.L., (1985), “Argument moves and Hypotheticals” In C. Walter (Ed.), Compu-
    ting Power and Legal Reasoning, St. Paul, MN: West Publishing Co.
28. Toulmin S. E. (1993). The use of arguments. Cambridge, Cambridge University Press.
29. Singh Simon, (1997), Fermat’s Last Theorem, Fourth Estate Ltd.
30. Stefaneas, P. & Vandoulakis, I. (2015), “On Mathematical Proving”. Computational Crea-
    tivity, Concept Invention, and General Intelligence Issue. Journal of General AI, 6(1):
    130-149.
31. Vandoulakis Ioannis M., Stefaneas Petros, (2015), “Mathematical Style as Expression of
    the Art of Proving”, Handbook of the 5th World Congress and School on Universal Logic,
    Istanbul, Turkey, UniLog 2015.
32. Vandoulakis Ioannis M., Stefaneas Petros, (2016), “Mathematical Proving as Multi-Agent
    Activity Spatio-Temporal”. 23rd World Congress of Philosophy, Methodology of Mathe-
    matical Modelling and of Applications of Logical Systems in Scientific Knowledge.
33. Vreeswijk Gerard A.W. (1997), “Abstract argumentation systems” AI, 90: 225-279.

</pre>