Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Debate has been used as a learning method since antiquity notably by sophists such as Protagoras, Plato and Socrates. From that time, the principles of this method remained unchanged: a group of learners explore a common question by exchanging opinions, ideas in the form of arguments and counter-arguments. Such debates are based on a collaborative and progressive learning process. What has changed however are technologies that nowadays enable autonomous and ubiquitous learning.

The literature of educational science witnesses numerous examples of debate-based learning [14, 20]. Furthermore, the use of debate in several areas such as medicine, natural sciences and humanities has been experimentally demonstrated as an effective learning tool [3, 8]. In the fields of mathematics, [15] proposes a description of Lakatos’s method by a dialogue game for collaborative mathematics. In short, we can synthesize main advantages of debate-based learning as follows: (i) it allows a group of heterogeneous learners with different backgrounds to collectively solve a common problem by using their own skills [1], (ii) it improves critical thinking skills, reasoning and communication within a group since each learner has to justify and defend her point of view and constructively criticize others [3, 6], (iii) it increases motivation and involvement of learners by improving self-esteem and promoting social interaction [13], (iv) it makes explicit reasoning processes that led to conclusions. This provides instructors with information to identify misunderstandings and take actions to correct them.

The context. We are interested in this paper in learning how to structure and build mathematical proofs. Mathematical skills are increasingly becoming a central criterion in skills evaluation as they are an important selection criterion for academic and professional applications. Therefore shortcomings in mathematics may be highly detrimental to students in both academic and professional opportunities. In the context of mathematical didactics several works have shown advantages of using debate in classes [5]. The object of the debate can be either to build a mathematical proof or to falsify a claim using sound mathematical deductions.

The problem and contribution. Despite the benefits witnessed in debates-based classes, we can mention some limitations of current approaches. The first limitation concerns learner’s motivation and involvement. Although it has been demonstrated that learners show a high motivation in debate-based courses [8], it has also been acknowledged that this is influenced by instructor’s animation abilities and the fact that these courses are formal and mandatory. In order to promote an autonomous and ubiquitous learning beyond institutional environment, we propose a gamification approach that considers the debate as a genuine game with its intrinsic motivation levers. The second limitation concerns assessment of debate outcomes and its effect on instructors’ workload. In fact, assessment is fundamental in order to provide learners with continuous feedbacks. This task is often performed manually by the instructor who has to understand, evaluate and provide feedbacks based on the state of the debate. However, debate data are often overloaded by details of intermediate and erroneous stages of reasoning. While these stages are important to understand how learners have come to final conclusions, they do overload instructors with unnecessary details during assessment phases. As the basic ingredients in debates are arguments and counter-arguments, we use formal argumentation framework as a means to extract final conclusions from a debate before its assessment by instructors.

The remainder of this paper is structured as follows. In Sect. 2 we provide necessary background on argumentation. In Sect. 3 we introduce our system for debate-based learning through argumentation and games. In Sect. 4 we illustrate our system with an example on a group of learners. Lastly we conclude.

2 Background on Formal Argumentation Frameworks

Artificial intelligence witnesses a large amount of contributions in argumentation theory. In particular Dung’s argumentation framework is a pioneer work in the topic [4].

Definition 1 (Dung’s Framework)

An argumentation framework (AF) is a tuple \(\langle \mathcal {A},\mathrm {{Def}}\rangle \), where \(\mathcal {A}\) is a finite set of arguments and Def \(\subseteq \mathcal {A}\times \mathcal {A}\) is a binary defeatFootnote 1 relation. Given \(A,B\in \mathcal {A}\), A Def B stands for “A defeats B”.

The outcome of Dung’s AF is sets of arguments, called extensions, that are robust against defeats [4]. We say that \(\mathcal {T}\subseteq \mathcal {A}\) defends A if \(\forall B\in \mathcal {A}\) s.t. B \(\mathrm {Def}\) A, \(\exists C \in \mathcal {T}\) such that C \(\mathrm {Def}\) B. We say that \(\mathcal {T}\subseteq \mathcal {A}\) is conflict-free if \(\not \exists A,B\in \mathcal {T}\) such that \(A\,\mathrm {Def}\, B\). A subset \(\mathcal {T}\subseteq \mathcal {A}\) of arguments is an admissible extension iff it is conflict-free and it defends all elements in \(\mathcal {T}\). Different acceptability semantics have been proposed. In particular \(\mathcal {T}\subseteq \mathcal {A}\) is a complete extension of \(\langle \mathcal {A}, {{Def}}\rangle \) iff it is admissible and contains all arguments it defends. \(\mathcal {T}\) is a grounded extension \(\langle \mathcal {A}, {{Def}}\rangle \) iff it is minimal (for set inclusion) complete extension. For other semantics, see [4].

Several authors have considered a new kind of interaction called the support relation [2, 11, 12]. An abstract bipolar argumentation framework is an extension of Dung’s framework such that both defeat and support relations are considered.

Definition 2 (Bipolar argumentation framework)

An abstract bipolar argumentation framework (BAF) is a tuple \(\langle \mathcal {A},\mathrm {{Def}}, \mathrm {{Supp}}\rangle \), where \(\langle \mathcal {A},\mathrm {{Def}}\rangle \) is Dung’s AF and \(\mathrm {{Supp}}\subseteq \mathcal {A}\times \mathcal {A}\) is a binary support relation. For \(A,B\in \mathcal {A}\), A Supp B means “A supports B”.

Defeat and support relations are combined to compute new defeat relations and recover Dung’s framework from which acceptable extensions are computed [2, 11, 12].

In this paper we are interested in deductive reasoning, i.e. a conclusion is derived from a set of premises.

Definition 3 (Argument)

Let \(\Gamma \) be a set of formulas constructed from a given language \(\mathcal {L}\). An argument over \(\Gamma \) is a pair \(A=\langle \Delta , \alpha \rangle \) s.t. (i) \(\Delta \subseteq \Gamma \), (ii) \(\Delta \not \vdash _*\bot \), (iii) \(\Delta \vdash _* \alpha \) and, (iv) for all \(\Delta '\subset \Delta \), \(\Delta '\not \vdash _* \alpha \), where \(\vdash _*\) is the inference symbol.

We say that \(\langle \Delta ,\alpha \rangle \) undercuts \(\langle \Delta ',\alpha '\rangle \) iff for some \(\phi \in \Delta '\), \(\alpha \) and \(\phi \) are contradictory w.r.t. the language at hand. \(\langle \Delta ,\alpha \rangle \) rebuts \(\langle \Delta ',\alpha '\rangle \) iff \(\alpha \) and \(\alpha '\) are contradictory. Then, \(\langle \Delta ,\alpha \rangle \) defeats \(\langle \Delta ',\alpha '\rangle \) iff \(\langle \Delta ,\alpha \rangle \) rebuts/undercuts \(\langle \Delta ',\alpha '\rangle \).

3 A Debate-Based Learning Game

Our system builds on learners who exchange arguments for some purpose. The Oracle represents the instructor of the game. She opens the discussion by providing a first argument of the form \(\langle P, C\rangle \), where P is a set of premises and C is a conclusion. Then learners are engaged in a debate in which they exchange arguments to construct a proof for C given P. A set of relations is provided by the Oracle to connect arguments. A learner may add an argument/relation or pass her turn. The discussion is closed when decided by the learners or stopped by the Oracle. The output of the debate is a debate graph which is composed of arguments and relations constructed during the debate. The graph is submitted to the Oracle for evaluation. We first discuss and give our design choices. Then we propose a game-based modeling of our learning system.

3.1 Design Choices

Different factors need to be considered for the game. Before we present our game-based modeling of the learning system let us expose these factors:

  • Argumentation mechanisms: Three mechanisms have been distinguished to model the exchange of arguments between agents [17]: In a Direct mechanism every agent may propose a set of arguments at once. Then the process terminates. This mechanism is not appropriate in our setting because a learning process needs to be progressive. In a synchronous mechanism every agent may propose any set of arguments at the same time. The process is repeated until no agent wants to make more arguments. In a dialectical mechanism an order is assumed over agents to provide their arguments. Four variants (rigid, non rigid) \(\times \) (single, multiple) can be obtained. A mechanism is rigid when an agent who passed her turn will no longer be allowed to propose arguments. The mechanism is not rigid if the agent is not discarded in such a situation. Also an agent may propose a single argument or multiple arguments when she takes her turn. As the purpose of the game is that all learners progressively collaborate to construct a proof we use a dialectical, non rigid and single argument mechanism.

  • Construction of the arguments & their validity: Arguments may be provided by the Oracle or constructed by learners. In the second case, the Oracle provides a set of propositions upon which arguments will be constructed. We choose the second option. Now whatever arguments are constructed or provided we need to check their validity which refers to the satisfaction of conditions (i)–(iv) in Definition 3. Condition (i) will always be satisfied as arguments will be constructed from a set of propositions provided by the Oracle. An argument that does not satisfy condition (ii) should be removed. An argument that does not satisfy condition (iv) should be modified to make its set of premises minimal. Let us now consider condition (iii). For example the argument \(\langle \{p\},q\rangle \) is not valid w.r.t. (iii) because q does not logically follow from p. This argument should be removed. On the other hand, the argument \(\langle \{(2-\epsilon )(n+2)<2n+1\},2-\epsilon <\frac{2n+1}{n+2}\rangle \) will be considered as valid although \(2-\epsilon <\frac{2n+1}{n+2}\) does not logically follow from \((2-\epsilon )(n+2)<2n+1\) because the set of premises of the argument is not complete. In fact we need an additional constraint, namely \(n+2>0\). Such an argument can however be accepted in a debate. Then learners have to cooperate in order to defeat the argument or defend it by completing its set of premises. This is coherent with a debate-based learning process in which arguments can be both collaboratively and progressively constructed. We distinguish between two ways to deal with an argument that should be removed (e.g. \(\langle \{p\},q\rangle \) or condition (ii) not satisfied) or modified (condition (iv)). First notice that learners in the same group cooperate in order to solve a problem. Therefore they may be allowed to have a chat box by which they can discuss in order to convince a learner that her argument is not valid and should be removed/modified. We expect a cooperation from all learners. If not then the non valid argument will be refused by the Oracle (when the latter evaluates the debate graph at the end of the debate) which leads to the failure of the group to construct a correct proof. Another way to control the validity of an argument is to delegate this task to the Oracle in which case an argument is added to the debate graph only when it is valid. A penalty on the score of the group is applied each time a learner proposes a non valid argument. We choose the first option.

    If constructed arguments do not comply with Definition 3 and not repaired/removed by learners then the group will fail to construct a correct proof.

  • Relations between arguments and their validity:

    1. Defeat relation: This relation is syntactically defined and should be in the background of learners. In contrast to existing works [16, 17] in which the defeat relation is automatically stated by the system as soon as an agent proposes an argument we do believe that this relation should be stated by the learners themselves. This is a part of the learning process. Two ways to control the validity of a defeat relation are possible. Either we authorize defeats on defeats which can be captured by hierarchical argumentation frameworks [10], or the Oracle accepts a defeat relation in the debate graph only when it is valid. We choose the second option in our game.

    2. Support relation: we do not control the support relation because the objective of the game is to construct a proof which is built using the support relation. So it is up to learners to discuss/agree on a given support relation without the intervention of the Oracle.

  • Termination of the game: The game terminates when the group stops or the Oracle decides so. We choose the first option in our game. The debate graph is submitted to the Oracle for evaluation.

  • Score function: A score which is a penalty degree is given to a group of learners when its debate graph is evaluated by the Oracle. We define a penalty degree as the number of irrelevant arguments present in the debate graph plus the number of non valid defeat relations refused by the Oracle during the debate.

3.2 Game-Based Modeling of the Learning System

Our game aims at creating a debate environment for learners so that they can exchange arguments to prove the Oracle’s claim. Learners need to be maintained engaged in a game. For this purpose we use social levers of motivation: we divide learners into groups that will be made in competition. The Oracle initiates the debate by setting the question under the form of an argument. The group that wins the game is the one that manages to build a debate graph accepted by the Oracle with a minimal penalty. To construct such a graph, learners have to use their domain knowledge to build arguments and correctly set relationships between arguments. This section formalizes the game by describing states of the game and actions which are transitions among states.

3.2.1 State of the Game

To construct arguments we use a universe of discourse based on a given \(\mathcal {L}\)-language. We assume that this language is at least equipped with a conjunction operator. Given a set of arguments \(\mathcal {A}\) and a set of relation labels L, a state of a debate is a sequence of relations indexed by natural numbers and labels: \(S: L \times \mathbb {N} \rightarrow 2^{\mathcal {A}\times \mathcal {A}}\). \(S(l,k)_{l \in L, \ k \in \mathbb {N}}\) represents the content of the relation l at the kth step. \(\mathcal {S}\) denotes the set of all states.

3.2.2 Actions of the Game

Adding a relation. This action adds a new relationship between two (new or existing) arguments. This action takes as input the label of the relation and two arguments.

Definition 4

Given a relation label \(l \in L\) and a couple of arguments (AB), the add action is a transition between states such that \(\forall S, S' \in \mathcal {S}, S\overset{add(l,A,B)}{\longrightarrow } S'\) iff

$$\begin{aligned}&\exists k \in \mathbb {N}, \forall r \in L, \left\{ \begin{array}{l} \forall m>k, S'(r,m) = S(r,m) = \emptyset \\ \forall n < k, S(r,n) = S'(r,n) \\ S(r,k) = \emptyset \\ S'(r,k) = S(r,k-1) \;{\textit{for}}\; r\ne l \\ S'(l,k) = S(l,k-1) \cup \{(A,B)\} \end{array} \right. \end{aligned}$$

The add action makes a transition from S to \(S'\) if and only if the following conditions hold: (i) the game states contain only a finite number of known relation graphs. In other words, there exists an integer k for which all relation graphs of subsequent steps are empty, (ii) S and \(S'\) are equal until kth step. This means that \(S'\) copies S until the kth step, (iii) game state S does not contain any information about the relation l at step k, (iv) finally, game state \(S'\) at kth step is equal to the graph of l at the \((k-1)\)th step to which the couple (AB) is added.

Removing a relation. A player can remove a relation between arguments from the debate graph. This action takes as input the label of the relation and the couple to be removed. Specification of the remove action is similar to that of the add action, except that \(S'\) at kth step contains previous graph of l from which the pair (AB) has been removed. That is \(S'(l,k) = S(l,k-1) {\setminus } \{(A,B)\}\).

Append action. The goal of this action is to make an argument’s premises and conclusion more specific. It is an auxiliary action that is built as a composition of a remove and add actions. Before we define this action, let us introduce a connector \((\wedge )\) between arguments. Given \(A=\langle P_1,C_1 \rangle \) and \(B=\langle P_2,C_2 \rangle \), the notation \(A \wedge B\) is an abbreviation for \(\langle P_1 \cup P_2,C_1 \wedge C_2 \rangle \) Footnote 2.

Definition 5

The append relation between states S and \(S'\) is defined as:

$$\begin{aligned} {\forall S, S' \in \mathcal {S}, S \overset{append(l,A,B,C)}{\longrightarrow } S' \; \textit{iff} \;\exists S'', S \overset{remove(l,A,B)}{\longrightarrow } S'' \overset{add(l,A \wedge C,B)}{\longrightarrow }S'.} \end{aligned}$$

Submit action. This action ends the game and submits the final debate state to the Oracle for evaluation.

4 Example: Mathematical Proof

Let Q: “Prove that \(\forall \epsilon >0 \exists N\in \mathbb {N}\) such that \((n \ge N \Rightarrow 2-\epsilon<\frac{2n+1}{n+2}< 2+ \epsilon )\)” to be proved. We have the Oracle and 6 learners (players): \(l_{1},l_{2},l_{3},l_{4},l_{5},l_{6}\).

The Oracle provides a first argument \(A_0\) corresponding to Q. We have \(A_0=\langle \{\epsilon >0, \exists N\in \mathbb {N},n \ge N\},2-\epsilon<\frac{2n+1}{n+2}< 2+ \epsilon )\rangle \). The Oracle also provides a set of labels \(L=\{defeat,support\}\) and a set of propositions \(\mathcal {P}\):

$$\begin{aligned} \begin{array}{llllllllll} \{ n\in \mathbb {N}, &{} \frac{2n+1}{n+2}< 2, &{} 2-\epsilon<\frac{2n+1}{n+2}, &{} \frac{2n+1}{n+2}<2+\epsilon , &{} \lnot (\frac{2n+1}{n+2}<2), \\ n\ge N, &{} \epsilon>0, &{} N>\frac{3}{\epsilon }-2, &{} n>\frac{3}{\epsilon }-2, &{} \\ \epsilon =-1, &{} n=1, &{} \lnot (2-\epsilon<\frac{2n+1}{n+2}), &{} n=-3, &{} \lnot (N=[\frac{3}{\epsilon }-2]+1) &{} \\ \lnot (n=-3), &{} \lnot (\epsilon =-1), &{} \exists N\in \mathbb {N}, &{} (2-\epsilon )(n+2)<2n+1\}. &{} \end{array} \end{aligned}$$

The aim of the game is to demonstrate Q. Let \(Group_{1}\) and \(Group_{2}\) be two groups of learners: \(G_{1}=\{l_{1},l_{2},l_{3}\}\) and \(G_{2}=\{l_{4},l_{5},l_{6}\}\). Each group has to demonstrate the proof individually. Not only the groups have to argue to construct the proof but they also have to do that as fast as possible and with minimal penalty degree. Due to space limitation, we illustrate the game on \(Group_1\) only. Initially, the debate graph contains only \(A_0\). The discussion is dialectical: a random order is defined over the set of learners. Let \(l_1,l_2,l_3\) be this order. Table 1 illustrates first states of the game.

Table 1. First game states during the game.

The complete debate graph is given in Fig. 1, where

$$ \begin{array}{lllcl} A_{1}{:}\; \langle \{\epsilon>0,\exists N\in \mathbb {N},n\ge N\}, 2-\epsilon<\frac{2n+1}{n+2}\rangle &{} A_{2}{:}\; \langle \{\epsilon =-1,n=1,\},\lnot (2-\epsilon<\frac{2n+1}{n+2})\rangle \\ A_{3}{:}\; \langle \{\epsilon>0,\exists N\in \mathbb {N},n\ge N\},\frac{2n+1}{n+2}<2+\epsilon \rangle &{} A_{4}{:}\; \langle \{\epsilon>0, \frac{2n+1}{n+2}<2\},\frac{2n+1}{n+2}<2+\epsilon \rangle \\ A_{5}{:}\; \langle \{\epsilon>0\} ,\epsilon>0\rangle &{} A_{6}{:}\; \langle \{n\in \mathbb {N}\}, \frac{2n+1}{n+2}< 2\rangle \\ A_7{:}\; \langle \{n\in \mathbb {N} \},n\in \mathbb {N}\rangle &{} A_8{:}\; \langle \{n\in \mathbb {N},(2-\epsilon )(n+2)<2n+1\},2-\epsilon<\frac{2n+1}{n+2}\rangle \\ A_9{:}\; \langle \{\epsilon>0,n>\frac{3}{\epsilon }-2\},(2-\epsilon )(n+2)<2n+1\rangle &{} A_{10}{:}\; \langle \{n\ge N,N>\frac{3}{\epsilon }-2\},n>\frac{3}{\epsilon }-2\rangle \\ A_{11}{:}\; \langle \{N>\frac{3}{\epsilon }-2\},N>\frac{3}{\epsilon }-2\rangle &{} A_{12}{:}\; \langle \{n\ge N\},n\ge N\rangle \\ A_{13}{:}\; \langle \{n=-3\}, \lnot (\frac{2n+1}{n+2}<2)\rangle &{} A_{14}{:}\; \langle \{n \in \mathbb {N}\}, \lnot (n=-3)\rangle \\ A_{15}{:}\; \langle \{ n\in \mathbb {N},\epsilon>0\},\frac{2n+1}{n+2}<2+\epsilon \rangle &{} A_{16}{:}\; \langle \{\epsilon >0 \}, \lnot (\epsilon =-1)\rangle \end{array} $$
Fig. 1.
figure 1

Debate graph during the game.

In this example learners may add a symmetric defeat between \(\langle \{\epsilon>0 \},\epsilon >0\rangle \) and \(\langle \{\epsilon =-1\},\epsilon =-1\rangle \). In this case learners need to discuss in a chat box and convince the learner who added the defeat relation from the latter to the former to remove her defeat because \(\epsilon >0\) appears in the premises of \(A_0\) so it is a fact that overrides \(\epsilon =-1\). We do not make any explicit distinction between propositions because distinguishing facts and giving them priority should be done by the learners. This is a part of the learning process. Assuming that the game ends when the learners agree to submit the debate graph to the Oracle. Thus \(Group_1\) submits the graph of the \(state_{final}\) using the action submit. Then the Oracle evaluates the debate graph by computing acceptable arguments. To this aim, she computes the argumentation framework corresponding to the debate graph in order to compute acceptable extensions. The debate graph is composed of nodes representing arguments and two types of relations, namely defeat and support relations. Therefore bipolar AF is suitable. We have \(BAF=\langle \mathcal {A},\mathrm {Def}, \mathrm {Supp}\rangle \), where \(\mathcal {A}=\{A_0,A_1,A_1\wedge A_3,A_2,A_3,A_4,A_5,A_6,\) \(A_5\wedge A_6,A_7,A_8,A_9,\) \(A_7\wedge A_9,\) \(A_{10},A_5\wedge A_{10},A_{11}\wedge A_{12},\) \(A_{13},A_{14},A_{15},A_{16}\}\), \(\mathrm {Def}=\{(A_2,A_1),(A_{16},A_2),(A_{13},A_6),\) \((A_{14},A_{13}) \}\) and \(\mathrm {Supp}=\{(A_1\wedge A_3,A_0),\) \((A_8,A_1),(A_9\wedge A_7,A_8),(A_{10}\wedge A_5,A_9),\) \((A_{11}\wedge A_{12},A_{10}),\) \((A_{15},A_3),\) \((A_4,A_{15}),\) \((A_5\wedge A_6,A_4),\) \((A_7,A_6),(A_5,A_{16}),\) \((A_7,A_{14})\}\) Footnote 3. In this example “A Supp B” is interpreted as “the acceptance of A is necessary for the acceptance of B” [2, 11].

As we previously indicated a bipolar argumentation framework can be translated into Dung’s argumentation framework by combining defeat and support relations. As we are looking for the proof of a given question, we need to compute the set of arguments that all learners agree on. To this aim the grounded extension is suitable as it is the set of arguments that are not defeated and those that are defeated but defended by acceptable arguments. Note that if the debate graph contains several valid proofs then all corresponding arguments will appear in the grounded extension. Given the grounded extension, the path of a proof can be retrieved from the debate graph thanks to the support relations. Without entering in the details of computation, the grounded extension associated to the above BAF is \(\{A_0,A_1,A_3,A_1\wedge A_3,A_4,A_5,A_6,A_5\wedge A_6,A_7,A_8,A_9,A_7\wedge A_9,A_{10},A_5\wedge A_{10},A_{11}\wedge A_{12},A_{14},\) \(A_{15},A_{16}\}\).

The Oracle evaluates the grounded extension. Then she informs the group if it won/failed the game and returns a penalty degree (if any). The wining group is the one that correctly constructed the proof with lowest penalty degree. The Oracle also returns irrelevant arguments to winners and wrong arguments/relationships to losers. In our example the group won the game with a penalty degree 3 due to a non valid defeat (\(A_3 \) Def \(A_1\)) and two irrelevant arguments (\(A_{14}\) and \(A_{16}\)).

5 Conclusion and Ongoing Work

The present paper uses argumentation framework in the context of mathematical proofs. It offers a conceptual formal debate-based learning system whose advantages are twofold: (i) it offers a formal method to analyze and filter (generally huge amount of) information exchanged during the debate and computes valuable information (i.e., acceptable arguments) that serves to evaluate the debate, (ii) it also provides a game-modeling of the argumentation debate as a means to keep learners motivated.

Several works present argumentation as an abstract dialectical game [9, 18]. However there are few genuine games based on the theoretical frameworks developed in AI. We can mention [19] which presents a simple graph of abstract arguments and players must select arguments in the graph to win the debate according to Dung’s semantics [4]. The authors of [17] use structured argumentation framework in order to construct a syntactical path for the support relation. Our work does rely on both syntactical and semantical paths in the support relation in order to fit the mathematical domain. We do also give a greater importance to the output of the argumentation framework which serves to extract valuable information from the debate (which corresponds to the proof).

As perspective we intend to experimentally validate our learning system to assess both its learning value for learners and its acceptance by instructors. At the conceptual level we intend to consider preferences among learners in the argumentation framework [7]. In fact more experts learners need to be favored against less expert ones.