{'fraction_non_alphanumeric': 0.031959106567396374, 'fraction_numerical': 0.004867207467496388, 'mean_word_length': 4.232093023255814, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 1, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Logical Semantics, Dialogical Argumentation, and Textual Entailment

In this chapter, we introduce a new dialogical system for first order classical logic which is close to natural language argumentation, and we prove its completeness with respect to usual classical validity. We combine our dialogical system with the Grail syntactic and semantic parser developed by the second author in order to address automated textual entailment, that is, we use it for deciding whether or not a sentence is a consequence of a short text. This work-which connects natural language semantics and argumentation with dialogical logic-can be viewed as a step towards an inferentialist view of natural language semantics.


Introduction
We propose an approach to the semantics of natural language inspired by the inferentialist theory of meaning. Inferentialism is a philosophical current developed in the 20th century from a certain reading of Wittgenstein's philosophical research [24]. As is well known, the Austrian philosopher declared that the meaning of a linguistic expression is not given by its truth value but by its use in a linguistic context. The inferentialists take up Wittgenstein's theory by claiming that the meaning of a sentence is given by its inferential use within language. That is, the meaning of a sentence lies in its argumentative use, its justifications, its refutations and more generally its deductive relation to other statements. We formally develop this kind of approach to the theory of meaning using dialogical logic. Dialogical logic is an approach to formal semantics developed from Lorenzen's pioneering work in the 1950s [15]. In dialogical logic the concept of validity is not defined starting from David Catta, Richard Moot, Christian Retoré LIRMM, Univ Montpellier, CNRS, Montpellier, France email:firstname.lastname@lirmm.fr that of interpretation in a structure. On the contrary, a formula is considered valid if, and only if, there is an argumentative strategy that, if followed, allows those who claim the formula to win any argumentative dialogue that may arise when the formula is proferred. The link with natural language semantics is obtained using type-logical grammars. Such grammars compute the possible meanings of a sentence viewed as logical formulae. In particular the Grail platform, a wide-scale categorial parser which maps French sentences to logical formulas [17,16,18], will be presented. We then use Grail and dialogical logic to solve some examples of textual entailment from the FraCaS database [6].
This chapter is structured as follows. Section 2 introduces inferentialism and its motivations. Section 3 introduces dialogical logic for classical first order logic and dialogical validity. Section 4 gives a proof of the fact that the class of formulas that are dialogicaly valid is equal to the class of formulas that are valid in the standard meaning of the term i.e. true in all interpretations. Section 5 is an introduction to categorical grammars and Grail. We conclude with the applications of semantics to the problem of textual inference.
We then show applications of this semantics to the problem of textual entailment using examples taken from the FraCaS database.
Hence this paper deepens and extends our first step in this direction "inferential semantics and argumentative dialogues" [5], mainly because of a strengthened link with natural language semantics and textual entailment: • We do not require the formulas to be in a normal negative form as done in [5]. In this way the strategies correspond to derivations in a two-sided sequent calculus, i.e. with multiple hypothesis and multiple conclusions. • We use Grail to connect natural language inference (or textual entailment) to argumentative dialogues: indeed Grail turns natural language sentences into logical formulas (delivered as DRS) -while our previous work only assumed that sentences could be turned into logical formulas. • This lead us closer to inferentialist semantics: a sentence S can be interpreted as all argumentative dialogues (possibly expressed in natural language) whose conclusion is S -under assumptions corresponding to word meaning and to the speaker beliefs.

Inferentialism
A problem with the standard view of both natural language semantics and of logical interpretations of formulas is that the models or possible worlds in which a sentence is true cannot be computed or even enumerated [19]. As far as pure logic is concerned there is an alternative view of meaning called inferentialism [8,9,21,7,2]. Although initially inferentialism took place within a constructivist view of logic [8], there is no necessary conceptual connection between accepting an inferentialist position and rejecting classical logic as explained in [7]. As its name suggests inferentialism takes the inferential activity of an agent to be the primary semantic notion rather then truth. According to this paradigm, the meaning of a sentence is viewed as the knowledge needed to understand the sentence.
This view is clearly stated by Cozzo [7] A theory of meaning should be a theory of understanding. The meaning of an expression (word or sentence) or of an utterance is what a speaker-hearer must know (at least implicitly) about that expression, or that utterance, in order to understand it.
This requirement has some deep consequences: as speakers are only able to store a finite amount of data, the knowledge needed to understand the meaning of the language itself should also be finite or at least recursively enumerable from a finite set of data and rules. Consequently, an inferentialist cannot agree with the Montagovian view of the meaning of a proposition as the possible worlds in which the proposition is true. In particular because there is no finite way to enumerate the infinity of possible worlds nor to finitely enumerate the infinity of individuals and of relations in a single of those possible worlds.
Let us present an example of the knowledge needed to understand a word. If it is a referring word like eat, one should know what it refers to the action that someone eats something, possibly some postulates related to this word like the eater is animated, 1 and how to compose it with other words eat is a transitive verb, a binary predicate; if it is a non referring word like which one should know that it combines with a sentence without subject (a unary predicate), and a noun (a unary predicate), and makes a conjunction of those two predicates.
Observe that this knowledge is not required to be explicit for human communication. Most speakers would find difficult to explicitly formulate these rules, especially the grammatical ones. It does not mean that they do not possess this knowledge.
An important requirement for a theory of meaning is that the speaker's knowledge can be observed, i.e. his knowledge can be observed in the interactions between the speaker(s), the hearer(s) and the environment. This requirement is supported by the famous argument against the private language of Wittgenstein [24] This might be explained as follows. Imagine that two speakers have the same use of a sentence S in all possible circumstances. Assume that one of the two speakers includes as part of the meaning of S some ingredient that cannot be observed. This ingredient has to be ignored when defining the knowledge needed to master the meaning of S. Indeed, according to the inferentialist view, a misunderstanding that can neither be isolated nor observed should be precluded.
Another requirement for a theory of meaning is the distinction between sense and force, on which we shall be brief. Since Frege, philosophy of language introduced the distinction between the sense of the sentence and its force. The sense of a sentence is the propositional content conveyed by the sentence, while its force is its mood -this use of the word "mood" is more general than its linguistic use for verbs. Observe that the same propositional content can be asserted, refuted, hoped etc. as in the three following sentences Is the window open? Open the window! The window is open.. Here we focus on assertions, and questions.

Dialogical Logic
Usually the inferentialist view of meaning is formally developed, as far as logic is concerned, by the use of natural deduction systems [11]. We deviate from this type of treatment by proposing to formally implement the ideas of inferentialist meaning theory through the tools provided by dialogical logic. In our view, the connection with semantics based on the notion of argument is clearer within the latter paradigm: an argument in favor of a statement is often developed when a critical audience, real or imaginary, doubts the truth, or the plausibility of the proposition. In this case, in order to successfully assert the statement, a speaker or proponent of it must be capable of providing all the justifications that the audience is entitled to demand. Taking this idea seriously, an approximation of the meaning of a sentence in a given situation can be obtained by studying the argumentative dialogues that arise once the sentence is asserted in front of such a critical audience. This type of situation is captured, with a reasonable degree of approximation by dialogical logic. In the dialogical logic framework, knowing the meaning of a sentence means being able to provide a justification of the sentence in front of a critical audience. Note that with this type of methodology the requirement of manifestability required to attribute knowledge of the meaning of a sentence to a locutor is automatically met. The locutor who asserts a certain formula is obliged to make his knowledge of the meaning manifest so that he can answer the questions and objections of his interlocutor. In addition, any concessions made by his interlocutor during the argumentative dialogue will form the linguistic context in which to evaluate the initial assertion.
We now gradually present dialogical logic. Although the study of dialectics -the art of correct debate -and logic -the science of valid reasoning -have been intrinsically linked since their beginnings [4,20,3], modern mathematical logic had to wait until the 50s of the last century to ensure that the logical concept of validity was expressed through the use of dialogical concepts and techniques. Inspired by the Philosophical Investigations of Wittgenstein [24], the German mathematician and philosopher Lorenzen [15] proposed to analyze the concept of validity of a formula F through the concept of winning strategy in a particular type of two-player game. This type of game is nothing more than an argumentative dialogue between a player, called Proponent, which affirms the validity of a certain formula F and another player, called opponent, which contends its validity. The argumentative dialogue starts by the proponent affirming a certain formula. The opponent takes turns and attacks the claim made by the proponent according to its logical form. The proponent can, depending on his previous assertion and on the form of the attack made by the opponent, either defend his previous claim or counter attack. The debate evolves following this pattern. The proponent wins the debate if he has the last word, i.e., the defence against one of the attack made by the opponent is a proposition that the opponent can not attack without violating the debate rules.
Dialogical logic was initially conceived by Lorenzen as a foundation for intuitionistic logic (IL). Lorenzen idea was, roughly speaking, the following. It is possible to define a "natural" class of dialogue game in which given a formula F of IL, i the proponent can always win a game on F , no matter how the opponent choose to attack his assertion in the debate, if F is IL-valid. This intuition was formalized as the completeness of the dialogical proof system with respect to provability or validity in any model: Completeness of a dialogical proof system: Given a logical language L and a notion of validity for L (either proof theoretical or model theoretical) and a notion of dialogical game, a formula F is valid in L if and only if, there is a winning strategy for the proponent of F in the class of games under consideration.
Where a winning strategy can be intuitively understood as an algorithm that take as input the moves of the game made so far and outputs proponents moves. Unfortunately, almost 40 years of work were needed to get a first correct proof of the completeness theorem [10]. Subsequently different systems of dialogic logic were developed. We present here a system of dialogical logic that is complete for classical first order logic.

Language, Positive and Negative Subformulas
We consider a first order language L in which the definition of terms and formulas is given as usual, and in which the negation of a formula ¬F is defined by F ⇒ ⊥ where ⊥ is an arbitrary atomic formula. Since we will use the notion of Gentzen's subformula and the positive (negative) occurrence of a subformula in a formula later, let us briefly detail these notions.
In the rest of the paper the term subformula will always be used as a short-cut for the term Gentzen-subformula. The notions of positive and negative subformulas are defined as follows (resp. positive) subformula of F , and F 2 is a positive (resp. negative) subformula of F 5. if ¬F is a positive (resp negative) subformula of F then F is a negative (resp. positive) subformula of F

Attack Rules
Here we define the rules that permit to attack a formula and what counts as a defence against the attack. The symbols in the central column that are not formulas are called auxiliary symbols In the table i ∈ {1, 2}, x stands for an arbitrary variable, and t stands for an arbitrary term. In the attack ?∀[t/x] and in the defence F [t/x], t is called the chosen term. For the sake of clarity we provide a paraphrase of the rules.
⇒ If one of the two participants in the dialogue asserts a conditional F 1 ⇒ F 2 , his opponent may attack this assertion by asserting, in turn, the antecedent of the conditional F 1 and ask him to assert F 2 . The one who asserted the conditional can defend himself against this attack by asserting F 2 , or, he can counterattack on F 1 . If he chose the latter option, the roles of the two players would be reversed. ∧ If one of the two participants in the dialogue affirms a conjunction, his opponent may attack the assertion by choosing one of the two members of the conjunction and asking to continue the dialogue by asserting the chosen member. The one who asserted the conjunction can defend himself by asserting the member chosen by his opponent. ∨ If one of the two participants in the dialogue asserts a disjunction, his opponent attacks the assertion by asking him to choose one of the two members and assert it. The one who asserted the disjunction can defend himself by choosing one of the two members and asserting it. ∀ If one of the two participants in the dialogue asserts universally quantified formula ∀xF his opponent may attack the formula by choosing a term t of the language and asking him to assert F [t/x], i.e., the formula in which the variable x is replaced by the term t. The one who has asserted the universally quantified formula can defend himself against such an attack by asserting F [t/x]. ∃ if one of the two participants in the dialogue asserts a existentially quantified formula ∃xF his opponent may attack the formula by asking him to choose a term t of the language and assert F [t/x], i.e. the formula in which the variable x is replaced by the term t. The one who has asserted the existentially quantified formula can defend himself against such an attack by choosing a term t and asserting F [t/x].
Remark that the rule ∧ and ∀ are similar: the one who attacks the assertion makes the choice of the subformula or of the term respectively. In the same way the rule for ∨ and ∃ are similar. The choice of the subformula, or of the term, is a responsibility of the one who defends.

Rules of Dialogical Games
Moves are pairs (i, s) with i ∈ {?, !} and s being either a formula or an auxiliary symbol. Moves are called attacks whenever i =? and defences whenever i =!.
An attack (?, F ) with F a formula is said to be an assertion. Defences are assertions. A Pre-justified sequence is given by a sequence of moves M = M 0 , M 1 . . . M j . . ., together with a partial function f : An assertion M n is a reprise if and only if there exists another move M j with smaller index and opposite parity that asserts the same formula. An assertion M n is called an existential repetition, if its enabler is of the form (?, ∃) and there is another move of the same parity M n with n < n having the same enabler. A pre-justified sequence in which each move is justified is called justified sequence

Games
. is a justified sequence of in which each oddindex move is enabled by the its immediate predecessor and in which each even-index move is enabled by a preceding odd-index move 2. if an even-index move asserts an atomic formula then it is a reprise. 3. for all even m, n if M m and M n are defence moves that asserts the same subformula occurrence of F and are enabled by the same move M j then m = n Odd-index moves are opponent moves (O-moves) while even index moves are called proponent moves (P-moves). A move M is legal for a game G if the pointing sequence G, M is a game.
A game G is won by the proponent if, and only if, it is finite and there is no O-move which is legal for D. It is won by the opponent otherwise.
Here are some properties needed in the proof of the completeness of our dialogical games. Proposition 2 For all game G, for all formula F for all subformula F of F . If there is an P-move (O-move) in G that asserts F then F is a positive (negative) subformula of F . Proof Let F be any formula and G any game. We show the proposition by induction on the length of G. If the length is 1 then G consist of only one move that is a P-move asserting a formula F and so the proposition holds. Suppose that the proposition holds for all games G having length n and let G be a game having length n + 1. Let M n be the last move of G . Suppose that M n is a P-move (the argument for O-moves runs in a very similar way) We have three cases.
1. If M n is not an assertion the proposition holds automatically by induction hypothesis.
2. if M n is a defence asserting some formula F . Since G is a game the sequence M 1 . . . M n is justified. Thus M n is enabled by some O-move M k with (k < n). If M k := (?, F 1 ) (the other cases are easier) then it is an attack against M k−1 and M k1 is a P-move that asserts F 1 ⇒ F . By induction hypothesis F 1 ⇒ F is a positive subformula of F , and F 1 is a negative subformula of F . Thus F is a positive subformula of F by definition. 3. If M n is an assertion and an attack, let F be the asserted formula. As before there must exists an enabler of M n , call it M k (k < n), M k is necessarily an O-move that asserts the formula F ⇒ F . By induction hypothesis this last formula is a negative subformula of F , thus F is a positive subformula of F by definition.
An easy consequence of the latter proposition is the following Proposition 3 Let G be a game for a formula F and let M n be a P-move in G asserting an atomic formula a(t 1 , . . . t m ). Then this latter formula appears both as a negative and positive subformula of F

Strategies
Informally speaking, a strategy for a player is an algorithm for playing the game that tells the player what to do for every possible situation throughout the game. We informally describe how a strategy should operate and then formalize this notion. Imagine being engaged in a game G, that the last move of G was played according to the strategy, and that it is now your opponent's turn to play. Your opponent could extend the game in different ways: for example if you are playing chess, you are white and you just made your first move by moving a pawn to a certain position of the chessboard, black can in turn move a pawn or move a horse. If you are playing according to the strategy, the strategy should tell you how to react against either type of move. If black moves a pawn to C6 and you just moved your pawn to C3 then move the horse to H3. If black moves a horse to H6 and you just moved your pawn to C3 then move you pawn in B4. This type of pattern can be visualized as a tree in which each node is a move in the game, the moves of my opponent have at most one daughter, and my moves have as many daughters as there are available moves for my opponent. In fact it is rather standard, in the game semantics/dialogical logic literature to define a strategy as a tree of games [10,1,13]. We thus formalize the notion of strategy as follows. Given a game G we say that a variable x appears in the game iff x appears in some asserted formula or is free in the choice of some universal attack. Let (v i ) i∈I be an enumeration of the variables in L. A strategy S is a prefix-closed set of games for the same formula (i.e. a tree of games for the same formula) such that 1. If G belongs to the strategy and the last move of G is a P move that neither an assertion of a universally quantified formula nor an existential attack then for all move M legal for G A strategy S is P-winning iff each game in S is won by P. Considering that a strategy is a tree of games, in what follows we will sometimes speak of nodes of a strategy as a shortcut for moves of a game G that belongs to the strategy.

Validity
Definition 2 Given a first order formula F we say that F is dialogically valid if, and only if, there exists a winning strategy S for the the formula.
Below are three examples of winning strategies. The blue dotted arrow represent the function f that points back from P moves to the O move that enables them. keep in mind that every O-move is enabled by the immediately preceding move.

Dialogical Validity is Classical Validity
In this section we show the equivalence, for a formula F between the dialogical validity of F (the existence of winning strategy for the proponent of F ) and classical validity of F (F being true in all interpretations). To prove this equivalence, we use a particular version of the sequent calculus, GKK (see the table below). The calculus GKK is a variant of the sequent calculus GKm [23], an extension to first order of the propositional calculus LKQ by Herbelin [12]: all those calculi are complete for classical logic (first order for GKK and GKm, propositional for LKQ), in the sense that a sequent Γ ∆ can be derived if and only if the formula Γ ⇒ ∆ classically valid.
Later on, as Herbelin does for LKQ, we shall consider a restriction (strategic derivations) on the use of the left implication introduction rule, a re- ?, a(c) !, ∀ya(y) striction which does not affect the completeness of the sequent calculus with respect to validity.

Definition 3
The sequent calculus GKK is defined by the rules below: Here are some comments and terminology on the calculus GKK: • Greek upper-case letters Γ, ∆, . . . stand for multisets of formulas.
• In the Id-rules A is an atomic formula. Since this rule has no premisse it is also called an axiom. • In the rules ∀R and ∃L the variable y does not occur anymore in their conclusion sequents. • The bold formulas in the conclusion of each rules are called active formulas. • A derivation π of a sequent Γ ∆ is a tree of sequents constructed according to the above rules, in which leaves are axioms Id-rules.
• We say that a sequent Γ ∆ is derivable or provable whenever there exists a derivation of it from axioms.
• A derivation π of Γ ∆ with Γ empty and ∆ reduces to one formula F , is said to be a proof of F .

Proposition 4 A sequent Γ ∆ is derivable in the sequent calculus GKK if and only if is derivable in Gkm.
Proof (Sketch) One just shows that each rule in the above sequent calculus is admissible in Gkm and vice-versa, using contraction and weakening admissibility, adapting the proof from e.g. [23].

From Strategies to Derivations
Because sequent calculus is complete for classical logic, the following proposition shows that a formula F with a winning strategy is true in any interpretation.
Proposition 5 Given a formula F , if there is a winning strategy for F then there is a proof π of F in sequent calculus GKK.
To do so, we associate sequents to nodes of a strategy and we prove that whenever the sequents associated with nodes of height n are provable, so are those of height n + 1. So let's start by associating sequents to some nodes of a strategy. To do this we focus on nodes of a strategy that are O moves.
Let S be a strategy and G be a game in S. Consider the sequence of moves M in G obtained by forgetting all its P-moves i.e if G is M 0 , M 1 , · · · M 2n · · · then M is M 1 , M 3 , . . . M 2n−1 . . .
Call D(S) the prefix closed set (i.e. the tree) of such sequences containing the empty sequence . Given a strategy S we associate a sequent Γ M ∆ M to each M ∈ D(S) in the following way 1. To the empty sequence we associate F . 2. if the sequence ends in an assertion move a. if the assertion is a defence move (!, F ) then we associate the sequent Γ, F ∆ where Γ ∆ is the sequent associated to the prefix of the sequence b. if the assertion is an attack move (?, F ) against (in the game ) an assertion of F → C then we associate the sequent Γ, F C, ∆ where Γ ∆ is the sequent associated to the prefix of the sequence from which we have erased the formula F ⇒ C on the right of 3. if the sequence end in a move that is not an assertion then it should be an attack, (?, s) where s is an auxiliary symbol. We have three type of case a. If s is either ?∨, ∧ 1 or ∧ 2 then we associate the sequent Γ ∆ where Γ is equal to the Γ associated to the prefix of the sequence, and ∆ is the sequent ∆ associated to the prefix of the sequence from which we have erased the formula C asserted by the move that is attacked by (?, s) and to which we have added the sub-formula of C chosen by O in the case of ∧ i and both subformulas of is the subformula of the formula ∀xA asserted by P and attacked by (?, s) and ∆ is obtained by erasing ∀xA from ∆ in the sequent Γ ∆ associated to the prefix of the sequence. c. if s is ∃ then we associate the sequent Γ F (t), ∆ where F (t) is the formula asserted by P in is defence against (?, s) and Γ ∆ is the sequent associated to the prefix of the sequence. Remark that the P-defence must exists by the definition of strategy.
Given a winning strategy S, observe that D(S) can be viewed as a (non empty) finite tree (D(S), ≺) with ≺ defined by (M) ≺ M if and only if M is a suffix of M -≺ is the order associated with the tree structure on D(S).
The above procedure yields D(S), a tree node-labeled with sequentssome object similar to a sequent calculus proof -such that: • the leaf-labels are of the form Γ, A A, ∆ with A an atomic proposition, • any formula in a sequent labeling a node of depth n is a subformula of some formula of the sequent labeling the nodes of depth n + 1.
The following lemma assures us that the labelled tree respects the variable restriction on ∀R ∃L Lemma 1 Let S be a winning strategy and let M be a sequence in D(S). Suppose that M ends in a move that is an attack against a universal quantifier (?, ∀[w/x]) or a defence against an existential attack (!, A[w/x]). Then the variable w does not appears free in the sequent associated to the proper prefix of M A decorated tree D(S) of a strategy S really looks like a derivation in the sequent calculus GKK.
We are now ready to prove the following lemma, which clearly entails proposition 5 above: Lemma 2 To each M ∈ D(S) we can associate a derivation π M of Γ M ∆ M -the sequent associated to M.
Proof By well-founded induction on (D(S), ≺). Suppose that for each suffix M of M the proposition holds. We associate a derivation to M by considering the last move of M 2n Φ(M). Where ΦM is the unique game G in S ending in a P-move such that M is obtained from G by erasing P-moves.
We only present here some non straightforward cases: 1. if M 2n is an attack (?, A) on the assertion A ⇒ C depending on the form of A • if A is atomic then the immediate suffix of M is M(!, C) for which the proposition hold by hypothesis. We associate it with the following derivation then M has two immediate suffixes namely M, (?, A 1 ) and M, (!, C), for which the proposition holds by hypothesis. We associate the following derivation: This proves proposition 5 and thus assures us that that if a formula is dialogically valid then it is provable in sequent calculus, hence true in any interpretation.

From Derivations to Strategies
We have just shown that if a formula is dialogically valid then it is provable in sequent calculus GKK. We now show the converse, by turning a GKK sequent calculus derivation into a winning a strategy, but we shall impose a restriction on GKK derivations -a restriction which derives exactly the same sequents.
Indeed not all derivations in GKK are the image of some winning strategy. For instance, the two derivations below where c(x), a, b are atomic formulas are not the image of any winning strategy S although there are winning strategies for the two formulas (bold formulas are active occurences of formulas in the sequent): , a a, b  a ⇒ b a, a → This leads us to restrict proofs of GKK to strategic proofs which derive the same sequents but always correspond to winning strategies, and to proceed as follows: • We first give a very informal description of the procedure that we use to transform a derivation into a strategy • By looking on how the derivation should be made in order for the procedure to be successful we define a subclass of derivations of GKK called strategic derivations • We show that the subclass is complete, in the sense that if the sequent Γ ∆ is provable then it corresponds to a strategic derivation.
Assume we already converted a derivation into a tree of moves, from conclusion to premises, up to a certain point by associating with each active formula, a set of sequences of moves. Assume that for each node a of depth n in the derivation, the branch of the derivation from a to the root is associated with a game G for the formula that is the root of the derivation. Let a 1 , · · · , a k be the the sons of a having depth n + 1.
We proceed as follows, starting with a 1 1. if a 1 bears a sequent in which the active formula A is on the right then it is obtained by a right rule or an id rule. Add to G one move by P that asserts A obtaining G . If these last assertion can be attacked by O enumerate the attacks M i such that G , M i is a game and obtain i sequences of moves that are games 2. if a 1 's label is a sequent in which the active formula A is on the left then a 1 is obtained by a left rule. Add to G one move by P that consist in attacking A obtaining a game G (if a is a conjunction or a universal quantifier look at the premise of a in order to find the right conjunct/term). Continue by extending G to (respectively) G M 1 , . . . G , M n where the M i are either defences against the last move of G or counter attack and are all O-moves Such a procedure clearly ends. If in (1) the active formula is an existentially quantified formula ∃xB then P asserts the formula and next it is attacked by O with (?, ∃). By definition of a strategy, P has to asserts B[t/x]. This means that a 1 should have just one son a 2 in which the formula B[t/x] is active.
A similar situation occurs in (2) when the active formula is a conditional A ⇒ B: P has to assert A, so A must be the active formula of the left premise of the ⇒ L rule.
In order to overcome this problem, we introduce the following definition: Definition 4 (Strategic derivations) A derivation π in GKK is said to be strategic whenever the two conditions below hold: • for each application of a left rule, the formula occurrence A in the lefthand premise is active.
• for each ∃R rule application the formula occurence A[t/x] is active in the premise: If π is a strategic derivation of F then the procedure above outputs a winning strategy for F Given these last proposition we can conclude our proof by the following Lemma 3 For any multiset of formulas Γ, ∆ there is a derivation of the sequent Γ ∆ iff and only iff there is a strategic derivation of Γ ∆ Proof The direction from right to left is straightforward: each strategic derivation is a derivation in GKK. The other direction results from a structural induction on the derivation π in GKK. All cases are straightforward except when π is obtained by π by the application of a ⇒ L rule or an ∃R rule. Let us discuss the ∃R rule, which together with a similar result in [12] dealing with all the propositional cases entail our proposition.
If π ends in a ∃R rule application then, by induction hypothesis there is a strategic derivation π 1 of its premise Γ A[t/x], ∃xA, ∆. if A[t/x] is active we are done. If not we can suppose, without loss of generality that the rule application in which A[t/x] is active is just above the last rule R of π 1 . The "hard" case is when R is a ∀R rules, A[t/x] = ∃yB(t, y) i.e. π 1 has the following shape: The problem being that the term t can contain a free occurrence of y. In this case we let permute the ∃R upwards in this way: . . . This concludes our proof of the equivalence between winning strategies for our dialogical games and the existence of a proof in classical logic (here viewed, without lost of generality, as a strategic GKK proof).

Categorial Grammars and Automated Theorem Proving
Type-logical grammars are a family of frameworks for the analysis of natural language based on logic and type theory. Type-logical grammars are generally fragments of intuitionistic linear logic, with the Curry-Howard isomorphism of intuitionistic logic serving as the syntax-semantics interface. Figure 2 shows the standard architecture of type-logical grammars.
1. given some input text, a lexicon translates words into formulas the result is a judgment in some logical calculus, such as the Lambek calculus or some variant/extension of it, 2. the grammaticality of a sentence corresponds to the provability of this statement in the given logic (where different proofs can correspond to different interpretations/readings of a sentence), 3. there is a forgetful mapping from the grammaticality proof into a proof of multiplicative, intuitionistic linear logic, 4. by the Curry-Howard isomorphism, this produces a linear lambda term representing the derivational meaning of the sentence (that is, it provides instructions for how to compose the meanings of the individual words), 5. we then substitute complex lexical meanings for the free variables corresponding to the lexical entries to obtain a representation of the logical meaning of the sentence, 6. finally, we use standard theorem proving tools (in first-or higher-order logic) the compute entailment relations between (readings of) sentences.
To make this more concrete, we present a very simple example, using the Lambek calculus. The Lambek calculus has two connectives 2 , A/B, pro-  Table 2 The multiplicative intuitionistic linear logic with linear lambda term labeling nounced A over B, representing a formula looking for a B constituent to its right to form an A, and B\A, pronounce B under A, representing a formula looking for a B constituent to its left to form an A. Table 1 shows the logical rules of the calculus. We'll look at the French sentence 'Un Suédois a gagné un prix Nobel' (A Swede won a Nobel prize). Figure 3 shows a Lambek calculus proof of this sentence. It shows that when we assign the formula n, for (common) noun, to 'prix' and n\n to 'Nobel', we can derive 'prix Nobel' as an n. Similarly, when we assign np/n to 'un' we can combine this with 'prix Nobel' of type n to produce 'un prix Nobel' as a noun phrase np. We can continue the proof as shown in Figure 3 to show that 'Un Suédois a gagné un prix Nobel' is a main, declarative sentence s. The lambda-term of the corresponding linear logic proof is (g(u p))(u s) (we have simplified a bit here, treating 'a gagné' and 'prix Nobel' as units). We then substitute the lexical semantics to obtain the logical representation of the meaning of this sentence. The simple substitutions are suédois for s and prix Nobel for p. The two complicated substitutions are the two occurrences of u which are translated as follows.  Fig. 3 Lambek calculus proof of 'Un Suédois a gagné un prix Nobel' (A Swede won a Nobel prize).
This is the standard Montague-style analysis of a generalised quantifier. It abstracts over two properties P and Q and states that there is an x which satisfies these two properties. Because of our choice of np for the quantifier (instead of a more standard higher-order type like s/(np\s), the type for the transitive verb has to take care of the quantifier scope. The lexical entry for the transitive verb below chooses the subject wide scope reading.
λN (e→t)→t λM (e→t)→t (M λx.(N λy.gagner(x, y))) Substituting these terms in into the lambda term for the derivation and normalising the resulting term produces the following.

∃x∃y.[suédois(x) ∧ prix Nobel(y) ∧ gagner(x, y)]
Even though this is an admittedly simple example, it is important to note that, although slightly simplified for presentation here, the output for this example and other examples in this paper are automatically produced by the wide-coverage French parser which is part of the Grail family of theorem provers [17]: Grail uses a deep learning model to predict the correct formulas for each word, finds the best way to combine these lexical entries and finally produces a representation of a logical formula. The full Grail output for the meaning of the example sentence is shown in Figure 4. Grail uses discourse representation structures [14] for its meaning representation, which is essentially a graphical way to represent formulas in first-order logic. Besides providing a readable presentation of formulas, discourse representation structures also provide a dynamic way of binding, with applications to the treatment of anaphora in natural language.
The variables d 0 , y 0 and z 0 in the top part of the rightmost box represent existentially quantified variables, y 0 is a swede, z 0 is a prize (named after Nobel) and d 0 is a variable for an eventuality -essentially denoting a slice of space-time, the inner box indicates that this 'winning' even must have occurred at a time before 'maintenant' (now ).
(1) Fig. 4 Grail output for the semantics of 'Un Suédois a gagné un prix Nobel' Even though the meaning assigned is in some ways simplistic, the advantage is that it can be automatically obtained and that it is of exactly the right form for logic-based entailment tasks.

Textual Entailment
What can dialogical argumentation contribute to the study of textual entailment? In natural language processing, textual entailment is usually defined as a relation between text fragments that holds whenever the truth of one text fragments follows from another text. Textual entailment recognition is the task of determining, given text fragments, whether the relation of textual entailment holds between these texts.
Our examples below are taken form the FraCaS benchmark, but translated into French; This is due to the fact that our methodology involves the use of Grail and the latter is developed mainly for the French language. The FraCaS benchmark was built in the mid 1990s; the aim was developing a general framework from computational semantics. The data set consists of problems each containing one or more statements and one yes/no-question. An example taken from the date set is the following (1) A Swede won a Nobel prize.
(3) Did a Scandinavian win a Nobel prize? [Yes]

First Example
We illustrate our methodology to solve inference problem using examples. First of all we turn the question (3) into an assertion i.e.
We then translate each sentence in french and use Grail on each sentence in order to get a logical formula. In the enumeration below we report, in order: the sentence in English. A word-for-word translation, then a translation that takes into account the grammar and idiomatic of French and, finally, the logical formula that Grail outputs from the input of the latter (5)  We then construct a winning strategy for the formula H 1 ∧H 2 . . .∧ H n ⇒ C where each H i is the logical formula that Grail associates to each statement from the data set, and C is the formula that Grail associates to the assertion obtained from the pair question-answer in the data-set. In the above formula su stands for suédois, p N for prix Nobel, g pour gagner and sc for scandinave. A winning strategy for the formula F is showed thereafter in two steps. The answer to the question is affirmative. This means that if (8) is true then the sentence "some delegate finished the survey on time" must also be true. survey enquête oǹ a time temps Certains délégues ont términé l'enquêteà temps ∃x∃y(délegué(x) ∧ (enquête(y) ∧ terminé-à-temps(x, y)))

Fourth Example
In the last example we focus on a series of sentences that our system should not solve, because the question asked neither has a positive nor a negative answer. This means that, on the basis of the information in our possession, we can neither say that a Swede has won a Nobel Prize nor that there are no Swedes who have won a Nobel Prize. Call the formula in (19) F 1 and the formula in (20) F 2 . In dialogical logic terms the fact that we do not have enough information neither to answer in a positive fashion nor in a negative fashion to the question (16), means that there is no winning strategy neither for the formula F 1 ∧ F 2 ⇒ F 3 nor for the formula F 1 ∧ F 2 ⇒ ¬F 3 where the formula F 3 is F 3 = ∃w∃z(suédois(w) ∧ (prix N obel(z) ∧ gagne(w, z))) In general given a sentence F of first order logic there it is not decidable whether F is valid. However in some cases we can manage this problem. Luckily the present case is one of those we can manage. We consider how a winning strategy for the formula F 1 ∧ F 2 → F 3 must look like. A winning strategy S for this formula will necessarily contain a dialog whose last move M n is a P-move that asserts suédois(t) for some term t in the language. Since suédois(t) is an atomic formula by proposition 3 above suédois(t) must occur both as a positive and negative gentzen sub-formula of F 1 ∧ F 2 ⇒ F 3 but this is not the case. Thus there is no winning strategy for the latter formula. Let us now discuss why there is no winning strategy for the formula F 1 ∧F 2 ⇒ ¬F 3 . First of all proposition 1 assures us that each game won by P ends by the assertion of some atomic formula and that such assertion is a P-move. By proposition 3 above the only candidate for this is again suédois(t) for all term t in the language. If the move P M k is an assertion of suéduois(t) then it must be an attack. Suppose is not the case then it should be a defence. This means that that there is a formula F of the form ∀wsuédois(w) or ∃w(suédois(w)) or F ∨ suédois(w) or F ∧ suédois(w) or F ⇒ suédois(t) that P asserts F . This imply that such formula F must be positive Gentzen-subformula of F 1 ∧ F 2 ⇒ ¬F 3 . But not suchformula exists. Thus the move M n asserting suédois(t) must be an attack. Since the only formula that can be attacked by this means is the is the formula suédois(t) ⇒ scandinave(t). O can answer back by asserting scandinave(t) thus P cannot win the game. Thus there is no winning strategy for the formula F 1 ∧ F 2 ⇒ ¬F 3

Conclusion
In this paper, we adapted our simple version of argumentative dialogues and strategies of [5] to two-sided sequents (hypotheses and conclusions): this point of view better matches natural language statements, because the assumptions sentences of a textual entailment task can be viewed as sequent calculus hypotheses, while the text conclusion can be viewed as the conclusion of the sequent.
In the present paper, we successfully use the syntactic and semantic platform Grail to "translate" natural language sentences into DRS that can be viewed as logical formulas.
This lead us closer to inferentialist semantics: a sentence S can be interpreted as all argumentative dialogues in natural language whose conclusion is S -under assumptions corresponding to word meaning and to the speaker beliefs.
We are presently working to extend our work with semantics taking place in classical first order logic to a broader setting in which semantics takes place in modal logic. Indeed, modal reasoning is rather common in natural language argumentation.
Regarding the architecture of our model of natural language argumentation we would like to encompass lexical meaning as axioms along the lines of [5] and to use hypotheses to model the way the two speakers differ in their expectations, beliefs and knowledge, taking insights from existing works on functional roles in dialogue modelling.