PhD Loïc Cohen

The outsourcing decision process in humanitarian supply chain management evaluated through

Keywords: Outsourcing decision, TCE, RBV, Humanitarian Logistics, Supply chain Management

the TCE and RBV principles.

In general, the outsourcing decision process has been mainly analysed by researchers through the TCE and RBV lens. In this context, this study is guided by the following research question:

-Given the important differences to be acknowledged between the "humanitarian" and the "commercial" contexts, are TCE and RBV perspectives used in SCM to support the outsourcing decision process, could be transposed to analyse the outsourcing decision in HSCM?

As stated by [START_REF] Jahre | Theory development in humanitarian logistics: a framework and three cases[END_REF], at this stage it is not clearly established which theoretical concepts the HSCM "borrows" its theories from. Therefore, in order to get a better understanding of the HSCM processes and for providing some theoretical perspective to the discipline, it would be interesting to test the applicability of key theories from the SCM to the HSCM.

The overall research methodology includes three different steps. The initial step is to screen the literature relating to the outsourcing decision process. The rationale for this approach is to identify how TCE and RBV principles support the decision to outsource SCM activities. The second step is to undertake an analysis of the humanitarian logistics literature in order to understand the specificity of the HSCM, and also to identify the trends in outsourcing supply chain management activities within the humanitarian sector. In a third stage, we will assess the applicability to the humanitarian supply chain of the two main theories principles governing the outsourcing decision process. In an emerging research field such as the HSCM, researches focusing on the use of theories principles are rare, therefore within the specificity of the HSCM this paper aims to provide a theoretical perspective to support the outsourcing decision process.

SCM OUTSOURCING

In the commercial sector, the outsourcing of SCM activities has been a common practice for decades. In general terms, the reasons invoked by the firms to outsource SCM activities are, to turn fixed costs into variable costs, to avoid heavy investments associated with logistics, to improve operating performance, to gain on flexibility and to focus more on their core business.

The researches on the outsourcing phenomenon take their bases on several different theories, some of them can be complementary and some other are contradictory, which can create some confusion in the analysis of the outsourcing decision process. As stated in the literature [START_REF] Perunovic | Outsourcing process and Theories[END_REF]Mc Ivor, 2009;[START_REF] Neves | Outsourcing from the perspectives of TCE and RBV: A multiple case study[END_REF][START_REF] Halldórsson | Complementary theories to supply chain management revisited -from borrowing theories to theorizing[END_REF] the outsourcing decision process analysis takes ground essentially on the Transaction Cost Economics (TCE) and/or the Resource Based Views (RBV) theories.

-Transaction Cost Economics (TCE)

According to many researches the TCE has traditionally been the theory which provides the best decision-making tool in order to assist organisations to cut costs in deciding which of their operations should be outsourced [START_REF] Ivanaj | Outsourcing Logistics Activities: A Transaction Cost Economics Perspective[END_REF]Mc Ivor, 2009;[START_REF] Spina | Assessing the use of External Grand Theories in Purchasing and Supply Management[END_REF].

Initially, [START_REF] Coase | The Nature of the Firm[END_REF] noted that firm's decision to make an economic exchange, incur some costs. Later, [START_REF] Williamson | Markets and Hierarchies: Analysis and Antitrust Implications[END_REF] defined the transaction costs as "the costs that attend completing transactions by one institutional mode rather than another". These costs can be divided in two types: ex-ante costs (prospecting, evaluation of the partner and the formulation of the contract) and ex-post costs (service provider performance monitoring and contract management).

According to the theory, in considering the behaviour of the economic partners (limited rationality and agent's opportunism), three different sorts of transactions governance are supposed to influence the level of transactions costs. The different types of governance are, the market, the hierarchy and a hybrid form between the market and the hierarchy. As developed by [START_REF] Williamson | Markets and Hierarchies: Analysis and Antitrust Implications[END_REF], three principal variables can affect the level of transaction costs which are assets specificity, uncertainty, and frequency of the exchanges:

-The frequency of exchange refers to the number of times the transaction takes place between the buyer and seller. According to the literature, outsourcing is justified only in case of a high degree of exchange frequency. Consequently, the trend is to outsource frequent recurring activities and to keep in-house non recurrent ones.

-Uncertainty of the transactions refers to the probabilities related to the exchanges type and occurrence. It implies a complex contract definition because all probabilities related to the type of exchange might be difficult to be specified for all situations. Consequently, it would be complex for the buyer and the seller to monitor and control the situation. In logistics, uncertainty causes difficulty for the principal to define and to forecast a highly fluctuating demand.

Generally, there is a tendency to outsource activities in a context of low uncertainty.

-The assets specificity refers to the specific attributes of the transaction due to site, physical or human assets specialisations. For non-specific assets, service providers can achieve economies of scale by providing standardised products or services to several customers. Therefore, the market governance is the most efficient option for non-specifics assets.

To summarize, in order to reduce transaction cost impact, a company would have the tendency to outsource activities having a high frequency of exchange, having a low uncertainty of occurrence and requiring a low assets specificity.

-The Resource-Based View (RBV)

Beside the minimization of the transaction costs ruled by the TCE, outsourcing decisions are evaluated as well through the RBV. This is in order to define the relevancy to keep in-house core competencies and to outsource non-strategic activities (Mc Ivor, 2009). [START_REF] Prahalad | The Core Competence of the Corporation[END_REF] have first established the link between core competencies and outsourcing. [START_REF] Quinn | Strategic outsourcing[END_REF] have systematized the process to identify which activities can be outsourced through the RBV. They recommend that firms should keep in-house and focus on core competencies in which they have definite advantages and to outsource of activities in which the firm has no critical strategic need or special skills. Outsourcing an activity can be seen as the mean to reduce a performance differential between the internal capabilities of the company and the quality of services available externally [START_REF] Grant | The Resource-Based Theory of Competitive Advantage: Implications for Strategy Formulation[END_REF]. The goal is to have access to resources and specific skills that would be difficult to accumulate internally. In this perspective, outsourcing allows the firm to use expert skills from the market and to focus internally on its core competencies.

Resources are strengths or weaknesses of a firm, or tangible and intangible assets tied to a firm.

They are valuable, rare, inimitable and non-substitutable, they provide to the firm a competitive advantage. According to the analysis of the outsourcing decision process through RBV:

-A firm outsources an activity when it is weak in the resources required for this activity.

-A firm outsources an activity when the resources required are not core competencies.

-A firm outsources an activity if capabilities in this activity are not strategic.

The schema below summarizes the outsourcing decision process supported by TCE and RBV:

Schema 1: outsourcing decision process

To conclude on the TCE and RBV attributes, the TCE offers a short-term approach based on costs reduction and the RBV proposes a long-term perspective including a strategic vision in the outsourcing decision. Therefore, TCE and RBV are complementary and can be coupled to guide the "make or buy" decision process (Mc Ivor, 2009;Gerlb et al 2015;[START_REF] Halldórsson | Complementary theories to supply chain management revisited -from borrowing theories to theorizing[END_REF].

THE HUMANITARIAN SUPPLY CHAIN: TEMPORALITY & UNPREDICTBILITY

When it comes to the definition of "humanitarian logistics", the most commonly used definition is the defintion from [START_REF] Thomas | Logistics training: necessity or luxury?[END_REF]: "Humanitarian logistics is the process of planning, implementing and controlling the efficient, cost-effective flow and storage of goods and materials, as well as related information, from point of origin to point of consumption for the purpose of meeting the end beneficiary's requirements".

HSCM is involved in three specifics phases, which are the preparedness, the immediate response and the reconstruction phase. Depending of the phase, different supply chain principles might be applied. Many authors have defined the HSCM as an agile supply chain [START_REF] Charles | A model to define and assess the agility of supply chains: building on humanitarian experience[END_REF][START_REF] Cozzolino | Agile and lean principles in the humanitarian supply chain[END_REF][START_REF] L'hermitte | An integrated approach to agility in humanitarian logistics[END_REF] and have highlighted the distinction between agile response and lean reconstruction. HSCM is the most expensive part of any relief operations and it can make the difference between a successful or failed operation [START_REF] Van Wassenhove | Humanitarian aid logistics: supply chain management in high gear[END_REF].

It is also important to note that the humanitarian sector regroups a wide panel of different types of organisations which range from NGOS, UN agencies, International Organisations, etc.

Although, even if they operate in the same context, the place of the HSCM within the organisation and the level of logistical capabilities vary from one organisation to the other ( [START_REF] Thomas | From Logistics to Supply Chain Management: The Path Forward in the Humanitarian Sector[END_REF]. Some of the largest organisations consider HSCM as a central function in emergency response, at the opposite some other organisations often neglect the importance of the logistics' role (Kovacs and Spens, 2009). Various factors, such as their size, mandate, funding sources and spezialization, define their organizational structure and their operational boundaries, which impact their HSCM strategy.

Many authors [START_REF] Beamon | Humanitarian relief chains, issues and challenges[END_REF][START_REF] Van Wassenhove | Humanitarian aid logistics: supply chain management in high gear[END_REF][START_REF] Kovacs | Humanitarian logistics in disaster relief operations[END_REF][START_REF] Day | Humanitarian and disaster relief supply chains: a matter of life and death[END_REF] have highlighted the differences between business sector SCM and HSCM. They note that there are important differences to be acknowledged between the "humanitarian" and "commercial" contexts. The main specifies of the HSCM are:

. The unpredictability of the demand makes forecasting difficult in terms of timing, location, type, volume of supplies.

. The operational context makes very complex the effective flow of goods and information.

. The imperatives associated with the time constraint for the delivery of supplies.

. The strategic goal is to minimize the loss of life and alleviate suffering, it is not based on profit . The recurrent lack of resources in terms of supply, expertise, technology, capacity, funding.

. The supply chain life span is short term and temporary.

Humanitarian supply chains are driven in project mode and they can be considered as temporary organizations from permanent structures. In order to assemble specific skills in a given time, the use of the service providers is common in this context of project management. Also, it is important to note that relief organisations are in competition to access funding, and donors are demanding greater accountability and better performance. Since logistics accounts for about 60% of a relief operation [START_REF] Van Wassenhove | Humanitarian aid logistics: supply chain management in high gear[END_REF], improving HSCM performance would surely give a ''competitive advantage'' to relief organisations to access funding. One way envisaged by certain organisations to improve the performance of their HSCM activities, is to delegate the conception, the management and the coordination of such activities to logistics service providers.

Given the high level of investment required to own logistics assets, the unpredictability of the demand, the complexity of the operational context and as well the short time life span of the supply chain, most of the organisations spot contract extensively logistics services.

Organisations work already with 3PL (third party logistics) logistics services providers (LSP) but the use of 4PL (fourth party logistics) is not really observed in the HSCM [START_REF] Balcik | Coordination in humanitarian relief chains: Practices, challenges and opportunities[END_REF].

However, it is important to note that there is a changing trend because the role of logistics service provider grows into important players and 4PL can act as an integrator and a coordinator in the HSCM [START_REF] Vega | Humanitarian logistics: the role of logistics service providers[END_REF].

In addition, as discussed by [START_REF] Jensen | Humanitarian cluster leads: lessons from 4PLs[END_REF], the logistics cluster leaded by the World Food Programme can carries tasks related to 4PL role such as services provider, integratorand coordinator. Having such form of 4PL services provision from an ''Insider'', can provide to many organisations the logistics expertise and capacity that they are missing. That would create less contractual complexity, because such services are specifically funded by donors and are dedicated to the humanitarian organisations for a specific emergency response.

RESULT/ FINDING

Based on the two main theories principles used to support the outsourcing decision process and based on the main characteristics of the HSCM, we have developed the two tables below to assess how the two theories principles support the outsourcing decision process in the HSCM.

-TCE

Principles

Outcomes applicable to SCM

HSCM characteristics

Outcomes applicable to HSCM

-Frequency of exchange

Outsource regular and frequent activities.

HSCM activities are not necessary frequent but can be diverse

Outsourcing is not recommended as HSCM activities aren't necessary frequent and recurrent. Contract definition and monitoring will be very complex. This will incur high level of transaction costs.

-Assets specificity

Outsource activities with a low degree of assets specificities

HSCM Assets are not specifics

Outsourcing is recommended as logistics assets are not specific but require a high level of investment. LSP can invest in such assets and make economy of scale by having several customers.

-Uncertainty Outsource in case of low uncertainty.

HSCM is characterized by a high level of uncertainty of demand (scale, location….)

Outsourcing is not recommended. Uncertainty is a key characteristic of the HSCM. Contract definition and monitoring will be very complex, and will incur high level of transaction costs.

We have seen that commercial companies often choose to outsource activities in the aim of reducing transaction costs. Humanitarian organizations are not profit-maximizing entities, but they aim to make their activities cost effective, which makes the application of TCE to this sector slightly different. Outsourcing decision process evaluated through TCE tells us that following the analysis of two TCE principles, which are the frequency and the uncertainty of the exchange, the outsourcing is not recommended. Given the characteristics of the HSCM and the high level of uncertainty, the analysis through the uncertainty principle will always give a negative outcome in the decision process. One of the reason is that the coordination cost would be high in a constantly changing operational context. Considering all the specificities that characterize the HSCM, we can deduct that the outsourcing process of a part or the entire supply chain management can be complex to define, implement and monitor. However, a hybrid form of governance between the hierarchies and the market can be adapted to the HSCM characteristics and can be defined between both parties.

-RBV

From a general point a view, we can deduct from the above table that according the analysis through the RBV principles and considering the HSCM characteristics, the outsourcing is recommended in all the cases. Accordingly, a resource-based view is particularly appropriate for examining HSCM outsourcing because organisation can use outsourcing as a strategy for gaining access to resources and capabilities. However, as we have seen previously, if relief organisations work in the same context, they can be very diverse depending of their mandate, funding, specialties and profile. Therefore, the resources profile, the capabilities and the strategy of an organisation can heavily influence the outcome of the outsourcing evaluation process through In addition, most of organisations are dependents on the funds provided to them by the institutional donors and the constraints of such funding give them a low level of manoeuvre in capabilities development. Consequently, as outsourcing entails buying a service instead of investing in the capabilities development to perform it in-house, the donors funding mechanism influences the decision process by limiting the options in internal capabilities development.

CONCLUSION

There is a growing body of literature arguing that TCE and the RBV are complementary to each other, which is based on the recognition that each theoretical perspective alone cannot fully explain the outsourcing decision. TCE offers a short-term approach based on costs reduction and the RBV propose a long-term perspective including a strategic vision in the outsourcing decision by gaining access to capabilities. However, as noted by Tabakar et al (2015), on a theoretical perspective, the characteristics on speed, agility, and flexibility are difficult to encapsulate in theories that are used in SCM research. Some supply chain decisions, such as outsourcing, are based on comparative analysis of possible alternatives, but these remain statics in the sense that they don't really include the agility and the contingency aspects which are the essential component of the HSCM.

In addition, in this paper we face some limitation because we have been very generalist on the profile of the relief organisations and it appears that mandate, funding, strategy, speciality of each organisation, are key elements in the outsourcing HSCM decision process. We believe that this paper can initiate interesting further researches on HCSM, in which we can define the typologies and the profiles of humanitarian organisations in order to determine if they are prone (or not) to outsource the management of their supply chain.

  SCM strategy (lean or/and agile) TCE -Transaction frequency: Outsource frequent recurring activities -Asset specificities: Outsource activities having a low degree of assets specificities -Transaction uncertainty: Outsource in case of low uncertainty RBV -Core competencies: Outsource if resources required are not core competencies -Resources: Outsource if weak in the resources required -Capabilities: Outsource if capabilities are not strategic


Richard Moot
email: richard.moot@labri.fr

The Grail theorem prover: Type theory for syntax and semantics

Type-logical grammars use a foundation of logic and type theory to model natural language. These grammars have been particularly successful giving an account of several well-known phenomena on the syntax-semantics interface, such as quantifier scope and its interaction with other phenomena. This chapter gives a highlevel description of a family of theorem provers designed for grammar development in a variety of modern type-logical grammars. We discuss automated theorem proving for type-logical grammars from the perspective of proof nets, a graph-theoretic way to represent (partial) proofs during proof search.

Introduction

This chapter describes a series of tools for developing and testing type-logical grammars. The Grail family of theorem provers have been designed to work with a variety of modern type-logical frameworks, including multimodal type-logical grammars [START_REF] Moortgat | Categorial type logics[END_REF], NL cl [START_REF] Barker | Continuations and Natural Language[END_REF], the Displacement calculus [START_REF] Morrill | The displacement calculus[END_REF] and hybrid type-logical grammars [START_REF] Kubota | Gapping as like-category coordination[END_REF].

The tools give a transparent way of implementing grammars and testing their consequences, providing a natural deduction proof in the specific type-logical grammar for each of the readings of a sentence. None of this replaces careful reflection by the grammar writer, of course, but in many cases, computational testing of handwritten grammars will reveal surprises, showing unintended consequences of our grammar and such unintended proofs (or unintended absences of proofs) help us improve the grammar. Computational tools also help us speed up grammar devel-opment, for example by allowing us to compare several alternative solutions to a problem and investigate where they make different predictions.

This chapter describes the underlying formalism of the theorem provers, as it is visible during an interactive proof trace, and present the general strategy followed by the theorem provers. The presentation in this chapter is somewhat informal, referring the reader elsewhere for full proofs.

The rest of this chapter is structured as follows. Section 9.2 presents a general introduction to type-logical grammars and illustrates its basic concepts using the Lambek calculus, ending the section with some problems at the syntax-semantics interface for the Lambek calculus. Section 9.3 looks at recent developments in type-logical grammars and how they solve some of the problems at the syntaxsemantics interface. Section 9.4 looks at two general frameworks for automated theorem proving for type-logical grammars, describing the internal representation of partial proofs and giving a high-level overview of the proof search mechanism.

Type-logical grammars

Type-logical grammars are a family of grammar formalisms built on a foundation of logic and type theory. Type-logical grammars originated when [START_REF] Lambek | The mathematics of sentence structure[END_REF] introduced his Syntactic Calculus (called the Lambek calculus, L, by later authors). Though Lambek built on the work of [START_REF] Ajdukiewicz | Die syntaktische Konnexität[END_REF], [START_REF] Bar-Hillel | A quasi-arithmetical notation for syntactic description[END_REF] and others, Lambek's main innovation was to cast the calculus as a logic, giving a sequent calculus and showing decidability by means of cut elimination. This combination of linguistic and computational applications has proved very influential.

In its general form, a type-logical grammar consists of following components:

1. a logic, which fulfils the role of "Universal Grammar" mainstream linguistics 1 , 2. a homomorphism from this logic to intuitionistic (linear) logic, this mapping is the syntax-semantics interface, with intuitionistic linear logic -also called the Lambek-van Benthem calculus, LP (van Benthem, 1995) -fulfilling the role of "deep structure". 3. a lexicon, which is a mapping from words of natural language to sets of formulas in our logic, 4. a set of goal formulas, which specifies the formulas corresponding to different types of sentences in our grammar. 2 A sentence w 1 , . . . , w n is grammatical iff the statement A 1 , . . . , A n C is provable in our logic, for some A i ∈ lex(w i ) and for some goal formula C. In other words, we use the lexicon to map words to formulas and then ask the logic whether the resulting sequence of formulas is a theorem. Parsing in a type-logical grammar is quite literally a form of theorem proving, a very pure realisation of the slogan "parsing as deduction".

One of the attractive aspects of type-logical grammars is their simple and transparent syntax-semantics interface. Though there is a variety of logics used for the syntax of type-logical grammars (I will discuss the Lambek calculus in Section 9.2.1 and two generalisations of it in Sections 9.3.1 and 9.3.2), there is a large consensus over the syntax-semantics interface. Figure 9.1 gives a picture of the standard architecture of type-logical grammars. The "bridge" between syntax and semantics in the figure is the Curry-Howard isomorphism between linear lambda terms and proofs in multiplicative intuitionistic linear logic.

Theorem proving occurs in two places of the picture: first when parsing a sentence in a given type-logical grammar and also at the end when we use the resulting semantics for inferences. I will have little to say about this second type of theorem proving [START_REF] Chatzikyriakidis | Natural language reasoning using Coq: Interaction and automation[END_REF][START_REF] Mineshima | Higher-order logical inference with compositional semantics[END_REF], provide some investigations into this question, in a way which seems compatible with the syntax-semantics interface pursued here, though developing a full integrated system combining these systems with the current work would be an interesting research project); theorem proving for parsing will be discussed in Section 9.4.

The lexicon plays the role of translating words to syntactic formulas but also specifies the semantic term which is used to compute the semantics later. The lexicon of a categorial grammar is "semantically informed". The desired semantics of a sentence allows us to reverse-engineer the formula and lexical lambda-term which produce it.

Many current semantic theories do not provide a semantic formula directly, but first provide a proto-semantics on which further computations are performed to produce the final semantics (eg. for anaphora resolution, presuppositions projection etc.). In the current context this means at least some inference is necessary to determine semantic and pragmatic wellformedness.

The Lambek calculus

To make things more concrete, I will start by presenting the Lambek calculus [START_REF] Lambek | The mathematics of sentence structure[END_REF]. Lambek introduced his calculus as a way to "obtain an effective rule (or algorithm) for distinguishing sentences from nonsentences", which would be applicable both to formal and to (at least fragments of) natural languages (Lambek, 1958, p. 154). The simplest formulas used in the Lambek calculus are atomic formulas, which normally include s for sentence, n for common noun, np for noun phrase. We then inductively define the set of formulas of the Lambek calculus by saying that, they include the atomic formulas, and that, if A and B are formulas (atomic or not), then A/B, A • B and B\A are also formulas.

The intended meaning of a formula A/B -called A over B -is that it is looking for an expression of syntactic type B to its right to produce an expression of syntactic type A. An example would be a word like "the" which is assigned the formula np/n in the lexicon, indicating that it is looking for a common noun (like "student") to its right to form a noun phrase, meaning "the student" would be assigned syntactic type np. Similarly, the intended meaning of a formula B\A -called B under A -is that it is looking for an expression of syntactic type B to its left to produce an expression of type A. This means an intransitive verb like "slept", when assigned the formula np\s in the lexicon, combines with a noun phrase to its left to form a sentence s. We therefore predict that "the student slept" is a sentence, given the earlier assignment of np to "the student". Finally, a formula A • B denotes the concatenation of an expression of type A to an expression of type B. Basic statements of the Lambek calculus are of the form A 1 , . . . , A n C (with n ≥ 1), indicating a claim that the sequence of formulas A 1 , . . . , A n is of type C; the sequent comma ',' is implicitly associative and non-commutative. Table 9.1 shows the natural deduction rules for the Lambek calculus. Γ , ∆ , etc. denote non-empty sequences of formulas.

Γ B ∆ B\A Γ , ∆ A [\E] B,Γ A Γ B\A [\I]
A simple Lambek calculus lexicon is shown in Table 9.2. I have adopted the standard convention in type-logical grammars of not using set notation for the lexicon, but instead listing multiple lexical entries for a word separately. This corresponds to treating lex as a non-deterministic function rather than as a set-valued function. Proper names, such as "Alyssa" and "Emory" are assigned the category np. Common nouns, such as "student" and "exam" are assigned the category n. Adjectives, such as "difficult" or "erratic" are not assigned a basic syntactic category but rather the category n/n, indicating they are looking for a common noun to their right to form a new common noun, so we predict that both "difficult exam" and "exam" can be assigned category n. For more complex entries, "someone" is looking to its right for a verb phrase to produce a sentence, where np\s is the Lambek calculus equivalent of verb phrase, whereas "whom" is first looking to its right for a sentence which is itself missing a noun phrase to its right and then to its left for a noun.

lex(Alyssa) = np lex(ran) = np\s lex(Emory) = np lex(slept) = np\s lex(logic) = np lex(loves) = (np\s)/np lex(the) = np/n lex(aced) = (np\s)/np lex(difficult) = n/n lex(passionately) = (np\s)\(np\s) lex(erratic) = n/n lex(during) = ((np\s)\(np\s))/np lex(student) = n lex(everyone) = s/(np\s) lex(exam) = n lex(someone) = (s/np)\s lex(who) = (n\n)/(np\s) lex(every) = (s/(np\s))/n lex(whom) = (n\n)/(s/np) lex(some) = ((s/np)\s)/n
Given the lexicon of Table 9.2, we can already derive some fairly complex sentences, such as the following, and, as we will see in the next section, obtain the correct semantics.

(1)

Every student aced some exam.

(2)

The student who slept during the exam loves Alyssa.

One of the two derivations of Sentence (1) is shown in Figure 9.2. To improve readability, the figure uses a "sugared" notation: instead of writing the lexical hypothesis corresponding to "exam" as n n, we have written it as exam n. The withdrawn np's corresponding to the object and the subject are given a labels p 0 and q 0 respectively; the introduction rules are coindexed with the withdrawn hypotheses, even though this information can be inferred from the rule instantiation.

We can always uniquely reconstruct the antecedent from the labels. For example, the sugared statement "p 0 aced q 0 s" in the proof corresponds to np, (np\s)/np, np s. Although it is easy to verify that the proof of Figure 9.2 has correctly applied the rules of the Lambek calculus, finding such a proof from scratch may look a bit complicated (the key steps at the beginning of the proof involve introducing two np hypotheses and then deriving s/np to allow the object quantifier to take narrow scope). We will defer the question "given a statement Γ C, how do we decide whether or not it is derivable?" to Section 9.4 but will first discuss how this proof corresponds to the following logical formula.

The syntax-semantics interface

For the Lambek calculus, specifying the homomorphism to multiplicative intuitionistic linear logic is easy: we replace the two implications '\' and '/' by the linear implication ' ' and the product '•' by the tensor '⊗'. In a statement Γ C, Γ is now a multiset of formulas instead of a sequence. In other words, the sequent comma ',' is now associative, commutative instead of associative, non-commutative. For the proof of Figure 9.2 of the previous section, this mapping gives the proof shown in Figure 9.3.

We have kept the order of the premisses of the rules as they were in Figure 9.2 to allow for an easier comparison. This deep structure still uses the same atomic formulas as the Lambek calculus, it just forgets about the order of the formulas and therefore can no longer distinguish between the leftward looking implication '\' and the rightward looking implication '/'.

To obtain a semantics in the tradition of [START_REF] Montague | The proper treatment of quantification in ordinary English[END_REF], we use the following mapping from syntactic types to semantic types, using Montague's atomic types e (for entity) and t (for truth value). Applying this mapping to the deep structure proof of Figure 9.3 produces the intuitionistic proof and the corresponding (linear) lambda term as shown in Figure 9.4 The computed term corresponds to the derivational semantics of the proof. To obtain the complete meaning, we need to substitute, for each of z 0 , . . . , z 4 , the meaning assigned in the lexicon.

z (e→t)→(e→t)→t 0 z e→t 1 (z 0 z 1 ) (e→t)→t → E [x e ] 2 z e→(e→t) 2 [y e ] 1 (z 2 y) e→t → E ((z 2 y) x) t → E λ y.((z 2 y) x) e→t → I 1 z (e→t)→(e→t)→t 3 z e→t 4 (z 3 z 4 ) (e→t)→t → E ((z 3 z 4 ) λ y.((z 2 y) x)) t → E λ x.((z 3 z 4 ) λ y.((z 2 y) x)) e→t → I 2 ((z 0 z 1 ) (λ x.((z 3 z 4 ) λ y.((z 2 y) x)))) t → E
For example, "every" has syntactic type (s/(np\s))/n and its semantic type is (e → t) → (e → t) → t. The corresponding lexical lambda term of this type is λ P e→t .λ Q e→t .(∀(λ x e .((⇒ (P x))(Q x)))), with '∀' a constant of type (e → t) → t and '⇒' a constant of type t → (t → t). In the more familiar Montague formulation, this lexical term corresponds to λ P e→t .λ Q e→t .∀x.[(P x) ⇒ (Q x)], where we can see the formula in higher-order logic we are constructing more clearly. Although the derivational semantics is a linear lambda term, the lexical term assigned to "every" is not, since the variable x has two bound occurrences.

The formula assigned to "some" has the same semantic type but a different term λ P e→t .λ Q e→t .(∃(λ x e .((∧(P x))(Q x)))).

The other words are simple, "exam" is assigned exam e→t , "student" is assigned student e→t , and "aced" is assigned ace e→(e→t) .

So to compute the meaning, we start with the derivational semantics, repeated below.

((z 0 z 1 ) (λ x.((z 3 z 4 ) λ y.((z 2 y) x))))

Then we substitute the lexical meanings, for z 0 , . . . , z 4 .

z 0 := λ P e→t .λ Q e→t .(∀(λ x e .((⇒ (P x))(Q x)))) z 1 := student e→t z 2 := ace e→(e→t) z 3 := λ P e→t .λ Q e→t .(∃(λ x e .((∧(P x))(Q x)))) z 4 := exam e→t
This produces the following lambda term.

((λ P e→t .λ Q e→t .(∀(λ x e .((⇒ (P x))(Q x)))) student e→t ) (λ x.((λ P e→t .λ Q e→t .(∃(λ x e .((∧(P x))(Q x)))) exam e→t ) λ y.((ace e→(e→t) y) x))))
Finally, when we normalise this lambda term, we obtain the following semantics for this sentence.

(∀(λ x e .((⇒ (student e→t ) x))(∃(λ y e .((∧(exam e→t y))(((ace e→(e→t) y) x)))))

This lambda term represents the more readable higher-order logic formula3 .

∀x.[student(x) ⇒ ∃y.[exam(y) ∧ ace(x, y)]]

Proofs in the Lambek calculus, and in type-logical grammars are subsets of the proofs in intuitionistic (linear) logic and these proofs are compatible with formal semantics in the tradition initiated by [START_REF] Montague | The proper treatment of quantification in ordinary English[END_REF].

For the example in this section, we have calculated the semantics of a simple example in "slow motion": many authors assign a lambda term directly to a proof in their type-logical grammar, leaving the translation to intuitionistic linear logic implicit.

Given a semantic analysis without a corresponding syntactic proof, we can try to reverse engineer the syntactic proof. For example, suppose we want to assign the reflexive "himself" the lambda term λ R (e→e→t) λ x e .((R x) x), that is, a term of type (e → e → t) → e → t. Then, using some syntactic reasoning to eliminate implausible candidates like (np n) n, the only reasonable deep structure formula is (np np s) (np s) and, reasoning a bit further about which of the implications is left and right, we quickly end up with the quite reasonable (though far from perfect) Lambek calculus formula ((np\s)/np)\(np\s).

Going further

Though the Lambek calculus is a beautiful and simple logic and though it gives a reasonable account of many interesting phenomena on the syntax-semantics interface, the Lambek calculus has a number of problems, which I will discuss briefly below. The driving force of research in type-logical grammars since the eighties has been to find solutions to these problems and some of these solutions will be the main theme of the next section.

Formal language theory

The Lambek calculus generates only context-free languages [START_REF] Pentus | Product-free Lambek calculus and context-free grammars[END_REF]. There is a rather large consensus that natural languages are best described by a class of languages at least slightly larger than the context-free languages. Classical examples of phenomena better analysed using so-called mildly context-sensitive language include verb clusters in Dutch and in Swiss German [START_REF] Huijbregts | The weak inadequacy of context-free phrase structure grammars[END_REF][START_REF] Shieber | Evidence against the context-freeness of natural language[END_REF].

The Syntax-Semantics Interface Though our example grammar correctly predicted two readings for Sentence (1) above, our treatment of quantifiers doesn't scale well. For example, if we want to predict two readings for the following sentence (which is just Sentence (1) where "some" and "every" have exchanged position)

(3) Some student aced every exam.

then we need to add an additional lexical entry both for "some" and for "every"; this is easily done, but we end up with two lexical formulas for both words. However, this would still not be enough. For example, the following sentence is also grammatical.

(4) Alyssa gave every student a difficult exam.

(5) Alyssa believes a student committed perjury.

In Sentence (4), "every student" does not occur in a peripheral position, and though it is possible to add a more complex formula with the correct behaviour, we would need yet another formula for Sentence (5). Sentence ( 5) is generally considered to have two readings: a de dicto reading, where Alyssa doesn't have a specific student in mind (she could conclude this, for example, when two students make contradictory statements under oath, this reading can be felicitously followed by "but she doesn't know which"), and a de re reading where Alyssa believes a specific student perjured. The Lambek calculus cannot generate this second reading without adding yet another formula for "a". It seems we are on the wrong track when we need to add a new lexical entry for each different context in which a quantifier phrase occurs. Ideally, we would like a single formula for "every", "some" and "a" which applied in all these different cases.

Another way to see this is that we want to keep the deep structure formula n ((np s) s) and that we need to replace the Lambek calculus by another logic such that the correct deep structures for the desired readings of sentences like ( 4) and ( 5) are produced.

Lexical Semantics

The grammar above also overgenerates in several ways.

1. "ace" implies a (very positive) form of evaluation with respect to the object.

"aced the exam" is good, whereas "aced Emory", outside of the context of a tennis match is bad. "aced logic" can only mean something like "aced the exam for the logic course". 2. "during" and similar temporal adverbs imply its argument is a temporal interval:

"during the exam" is good, but "during the student" is bad, and "during logic" can only mean something like "during the contextually understood logic lecture"

In the literature on semantics, there has been an influential movement towards a richer ontology of types (compared to the "flat" Montagovian picture presented above) but also towards a richer set of operations for combining terms of specific types, notably allowing type coercions [START_REF] Pustejovsky | The generative lexicon[END_REF][START_REF] Asher | Lexical Meaning in Context: A Web of Words[END_REF]. So an "exam" can be "difficult" (it subject matter, or informational content) but also "take a long time" (the event of taking the exam). The theory of semantics outlined in the previous section needs to be extended if we want to take these and other observations into account.

Modern type-logical grammars

We ended the last section with some problems with using the Lambek calculus as a theory of the syntax-semantics interface. The problems are of two different kinds.

1. The problems of the syntax-semantic interface, and, in a sense, also those of formal language theory are problems where the deep structure is correct but our syntactic calculus cannot produce an analysis mapping to the desired deep structure. We will present two solutions to these problems in Sections 9.3.1 and 9.3.2. 2. The problems of lexical semantics, on the other hand require a more sophisticated type system than Montague's simply typed type-logical with basic types e and t and mechanisms like coercions which allow us to conditionally "repair" certain type mismatches in this system. We will discuss a solution to this problem in Section 9.3.3.

Multimodal grammars

Multimodal type-logical grammars [START_REF] Moortgat | Categorial type logics[END_REF] take the non-associative Lambek calculus as its base, but allow multiple families of connectives.

For the basic statements Γ C of the Lambek calculus, we ask the question whether we can derive formula C, the succedent, from a sequence of formulas Γ , the antecedent. In the multimodal Lambek calculus, the basic objects are labeled binary trees4 . The labels come from a separate set of indices or modes I. Multimodal formulas are then of the form A/ i B, A • i B and A\ i B, and antecedent terms are of the form Γ • i ∆ , with i an index from I (we have omitted the outer brackets for the rules, but the operator • i is non-associative). Sequents are still written as Γ C, but Γ is now a binary branching, labeled tree with formulas as its leaves.

Given a set of words w 1 , . . . , w n and a goal formula C, the question is now: is there a labeled tree Γ with formulas A 1 , . . . , A n as its yield, such that Γ C is derivable and A i ∈ lex(w i ) for all i (the implementation of Section 9.4.1 will automatically compute such a Γ ).

The rules of multimodal type-logical grammars are shown in Table 9.3. In the rules, Γ [∆ ] denotes an antecedent tree Γ with distinguished subtree ∆ -the subtree notation is a non-associative version of the Lambek calculus antecedent Γ , ∆ ,Γ , where ∆ is a subsequence instead of a subtree as it is in Γ

[∆ ].
Each logical connective with mode i uses a structural connective • i in its rule. For the /E, •I and \E rules, reading from premisses to conclusions, we build structure. For the /I, •E and \I rules we remove a structural connective with the same mode as the logical connective. The natural deduction rules use explicit antecedents, although, for convenience, we will again use coindexation between the introduction rules for the implications '/' and '\' and its withdrawn premiss (and similarly for the •E rule and its two premisses).

Logical Rules

∆ A • i B Γ [A • i B] C Γ [∆ ] C [• i E] Γ A ∆ B Γ • i ∆ A • i B [• i I] Γ A/ i B ∆ B Γ • i ∆ A [/ i E] Γ • i B A Γ A/ i B [/ i I] Γ B ∆ B\ i A Γ • i ∆ A [\ i E] B • i Γ A Γ B\ i A [\ i I] Structural Rules Γ [Ξ [∆ 1 , . . . , ∆ n ]] C Γ [Ξ [∆ π 1 , . . . , ∆ πn ]] C [SR] Table 9.3 Natural deduction for NL R
The main advantage of adding modes to the logic is that modes allow us to control the application of structural rules lexically. This gives us fine-grained control over the structural rules in our logic.

For example, the base logic is non-associative. Without structural rules, the sequent a/b, b/c a/c, which is derivable in the Lambek calculus is not derivable in its multimodal incarnation a/ a b, b/ a c a/ a c. The proof attempt below, with the failed rule application marked by the ' ' symbol, shows us that the elimination rules and the introduction rule for this sequent do not match up correctly.

a/ a b a/ a b b/ a c b/ a c c c b/ a c • a c b [/E] a/ a b • a (b/ a c • a c) a [/E] (a/ a b • a b/ a c) • a c a a/ a b • a b/ a c a/ a c [/I] Γ [∆ 1 • a (∆ 2 • a ∆ 3 )] C Γ [(∆ 1 • a ∆ 2 ) • a ∆ 3 ] C Ass Γ [(∆ 1 • 1 ∆ 3 ) • 0 ∆ 2 ] C Γ [(∆ 1 • 0 ∆ 2 ) • 1 ∆ 3 ] C MC
The first structural rule is one of the structural rules for associativity. It is the simplest rule which will make the proof attempt above valid (with Γ [] the empty context, ∆ 1 = a/ a b, ∆ 2 = b/ a c and ∆ 3 = c). This structural rule keeps the order of the ∆ i the same.

The rule above on the right is slightly more complicated. There, the positions of ∆ 2 and ∆ 3 are swapped as are the relative positions of modes 0 and 1. Rules like this are called "mixed commutativity", they permit controlled access to permutation. One way to see this rule, seen from top to bottom, is that is "moves out" a ∆ 3 constituent which is on the right branch of mode 1. Rules of this kind are part of the solution to phenomena like Dutch verb clusters [START_REF] Moortgat | Adjacency, dependency and order[END_REF].

Many modern type-logical grammars, such as the Displacement calculus and NL cl can be seen as multimodal grammars [START_REF] Valentín | The hidden structural rules of the discontinuous Lambek calculus[END_REF][START_REF] Barker | Continuations and Natural Language[END_REF].

First-order linear logic

We have seen that multimodal type-logical grammars generalise the Lambek calculus by offering the possibility of fine-tuned controlled over the application of structural rules. In this section, I will introduce a second way of extending the Lambek calculus.

Many parsing algorithms use pairs of integers to represent the start and end position of substrings of the input string. For example, we can represent the sentence (6) Alyssa believes someone committed perjury.

as follows (this is a slightly simplified version of Sentence (5) from Section 9.2.3); we have treated "committed perjury" as a single word. The basic idea of first-order linear logic as a type-logical grammar is that we can code strings as pairs (or, more generally, tuples) of integers representing string positions. So for deciding the grammaticality of a sequence of words w 1 , . . . , w n C, with a goal formula C, we now give a parametric translation from A i i-1,i for each lexical entry w i and C 0,n for the conclusion formula.

Given these string positions, we can assign the noun phrase "Alyssa" the formula np(0, 1), that is a noun phrase from position 0 to position 1. The verb "believes", which occurs above between position 1 and 2, can then be assigned the complex

formula ∀x 2 .[s(2, x 2 ) ∀x 1 .[np(x 1 , 1) s(x 1 , x 2 )]],
meaning that it first selects a sentence to its right (that is, starting at its right edge, position 2 and ending anywhere) and then a noun phrase to its left (that is, starting anywhere and ending at its left edge, position 1) to produce a sentence from the left position of the noun phrase argument to the right position of the sentence argument.

We can systematise this translation, following [START_REF] Moot | Linguistic applications of first order multiplicative linear logic[END_REF], and obtain the following translation from Lambek calculus formulas to first-order linear logic formulas. p x,y = p(x, y)

A/B x,y = ∀z. B y,z A x,z B\A y,z = ∀x. B x,y A x,z A • B x,z = ∃y. A x,y ⊗ B y,z
Given this translation, the lexical entry for "believes" discussed above is simply the translation of the Lambek calculus formula (np\s)/s, with position pair 1, 2, to first-order linear logic. Doing the same for "committed perjury" with formula np\s and positions 3, 4 gives ∀z.[np(z, 3) s(z, 4)]. For "someone" we would simply translate the Lambek calculus formula s/(np\s), but we can do better than that: when we translate "someone" as ∀y 1 .∀y 2 . [(np(2, 3) s(y 1 , y 2 )) s(y 1 , y 2 )], we improve upon the Lambek calculus analysis.

As we noted in Section 9.2.3, the Lambek calculus cannot generate the "de re" reading, where the existential quantifier has wide scope. Figure 9.5 shows how the simple first-order linear logic analysis does derive this reading. np(0, 1) Besides the Lambek calculus, first-order linear logic has many other modern type-logical grammars as fragments. Examples include lambda grammars [START_REF] Oehrle | Term-labeled categorial type systems[END_REF], the Displacement calculus [START_REF] Morrill | The displacement calculus[END_REF] and hybrid type-logical grammars [START_REF] Kubota | Gapping as like-category coordination[END_REF]. We can see first-order linear logic as a sort of "machine language" underlying these different formalisms, with each formalism introducing its own set of abbreviations convenient for the grammar writer. Seeing first-order linear logic as an underlying language allows us to compare the analyses proposed for different formalisms and find, in spite of different starting points, a lot of convergence. In addition, as discussed in Section 9.4.2, we can use first-order linear logic as a uniform proof strategy for these formalisms.

[np(2, 3)] 1 ∀A.[np(A, 3) s(A, 4)] np(2, 3) s(2, 4) ∀E s(2, 4) E ∀B.[s(2, B) ∀C.[np(C, 1) s(C, B)]] s(2, 4) ∀C.[np(C, 1) s(C, 4)] ∀E ∀C.[np(C, 1) s(C, 4)] E np(0, 1) s(0, 4) ∀E s(0, 4) E np(2, 3) s(0, 4) I1 ∀D.∀E.[(np(2, 3) s(D, E)) s(D, E)] ∀E.[(np(2, 3) s(0, E)) s(0, E)] ∀E (np(2, 3) s(0, 4)) s(0, 4) ∀E s(0, 4) E

Syntax-Semantics Interface

As usual, we obtain the deep structure of a syntactic derivation by defining a homomorphism from the syntactic proof to a proof in multiplicative intuitionistic linear logic. For first-order linear logic, the natural mapping simply forgets all first-order

A ⊗ B [A] i [B] i . . . . C C ⊗E i A B A ⊗ B ⊗I A A B B E [A] i . . . . B A B I ∃x.A [A] i . . . . C C ∃E * i A[x := t] ∃x.A ∃I ∀x.A A[x := t] ∀E A ∀x.A
∀I * * no free occurrences of x in any of the free hypotheses quantifiers and replaces all atomic predicates p(x 1 , . . . , x n ) by propositions p. Since the first-order variables have, so far, only been used to encode string positions, such a forgetful mapping makes sense. However, other solutions are possible. When we add semantically meaningful terms to first-order linear logic, the Curry-Howard isomorphism for the first-order quantifiers will give us dependent types and this provides a natural connection to the work using dependent types for formal semantics [START_REF] Ranta | Intuitionistic categorial grammar[END_REF][START_REF] Pogodalla | Controlling extraction in abstract categorial grammars[END_REF]Luo, 2012b[START_REF] Luo | A Lambek calculus with dependent types[END_REF].

The Montagovian Generative Lexicon

In the previous sections, we have discussed two general solutions to the problems of the syntax-semantics interface of the Lambek calculus. Both solutions proposed a more flexible syntactic logic. In this section, we will discuss a different type of added flexibility, namely in the syntax-semantics interface itself.

The basic motivating examples for a more flexible composition have been amply debated in the literature [START_REF] Pustejovsky | The generative lexicon[END_REF][START_REF] Asher | Lexical Meaning in Context: A Web of Words[END_REF]. Our solution is essentially the one proposed by [START_REF] Bassac | Towards a type-theoretical account of lexical semantics[END_REF], called the Montagovian Generative Lexicon. I will only give a brief presentation of this framework. More details can be found in Chapter 6.

Like many other solutions, the first step consists of splitting Montague's type e for entities into several types: physical objects, locations, informational objects, eventualities, etc. Although there are different opinions with respect to the correct granularity of types [START_REF] Pustejovsky | The generative lexicon[END_REF][START_REF] Asher | Lexical Meaning in Context: A Web of Words[END_REF]Luo, 2012a), nothing much hinges on this for the present discussion.

The second key element is the move to the second-order lambda calculus, system F (Girard et al, 1995), which allows abstraction over types as well as over terms. In our Lambek calculus, the determiner "the" was assigned the formula np/n and the type of its lexical semantics was therefore (e → t) → e, which we implement using the ι operators of type (e → t) → e, which, roughly speaking, selects a contextually salient entity from (a characteristic function of) a set. When we replace the single type e by several different types, we want to avoid listing several separate syntactically identical by semantically different entries for "the" in the lexicon, and therefore assign it a polymorphic term Λ α.ι (α→t)→α of type Π α.((α → t) → α), quantifying over all types α. Though this looks problematic, the problem is resolved once we realise that only certain function words (quantifiers, conjunctions like "and") are assigned polymorphic terms and that we simply use universal instantiation to obtain the value of the quantifier variable. So if "student" is a noun of type human, that is of type h → t, then "the student" will be of type h, instantiating α to h. Formally, we use β reduction as follows (this is substitution of types instead of terms, substituting type h for α).

((Λ α.ι (α→t)→α ){h} student h→t ) = β (ι student) h
The final component of the Montagovian Generative Lexicon is a set of lexically specified, optional transformations. In case of a type mismatch, an optional transformation can "repair" the term.

As an example from [START_REF] Moot | Second order lambda calculus for meaning assembly: on the logical syntax of plurals[END_REF] and [START_REF] Mery | Plurals: individuals and sets in a richly typed semantics[END_REF], one of the classic puzzles in semantics are plurals and collective and distributive readings. For example, verbs like "meet" have collective readings, they apply to groups of individuals collectively, so we have the following contrast, where collectives like committees and plurals like students can meet, but not singular or distributively quantified noun phrases. The contrast with verbs like "sneeze", which force a distributive reading is clear.

(7)

The committee met.

(8) All/the students met (9) *A/each/the student met.

(10) All/the students sneezed.

(11) A/each/the student sneezed.

In the Montagovian Generative lexicon, we can models these fact as follows. First, we assign the plural morphology "-s" the semantics Λ αλ

P α→t λ Q α→t .|Q| > 1 ∧ ∀x α .Q(x) ⇒ P(x), then "students" is assigned the following term λ Q h→t .|Q| > 1 ∧ ∀x h .Q(x) ⇒ student(x)
, that is the sets of cardinality greater than one such that all its members are students. Unlike "student" which was assigned a term of type h → t, roughly a property of humans, the plural "students" is assigned a term of type (h → t) → t, roughly a property of sets of humans. Consequently, the contrast between "the student" and "the students" is that the first is of type h (a human) and the second of type h → t (a set of humans) as indicated below.

phrase syntactic type lambda-term the student np (ιstudent) h the students np

(ι(λ Q h→t .|Q| > 1 ∧ ∀x h Q(x) ⇒ student(x))) h→t
Therefore, the meaning of "the students" is the contextually determined set of humans, from the sets of more than one human such that all of them are students.

Then we distinguish the verbs "meet" and "sneeze" as follows, with the simpler verb "sneeze" simply selecting for a human subject and the collective verb "meet" selecting for a set of humans (of cardinality greater than one) as its subject.

word syntactic type lambda-term met np\s

λ P h→t .|P| > 1 ∧ meet(P) # Λ αλ R (α→t)→t λ S (α→t)→t ∀P α→t .S(P) ⇒ R(P) met # np\s λ R (h→t)→t ∀P h→t .R(P) ⇒ |P| > 1 ∧ meet(P) sneezed np\s λ x h .sneeze(x) * Λ αλ P α→t λ Q α→t ∀x α .Q(x) ⇒ P(x) sneezed * np\s λ P h→t .∀x h .P(x) ⇒ sneeze(x)
Given these basic lexical entries, we already correctly predict that "the student met" is ill-formed semantically (there is an unresolvable type mismatch) but "the students met" and "the student sneezed" are given the correct semantics.

The interesting case is "the students sneezed" which has as its only reading that each student sneezed individually. Given that "the students" is of type h → t and that "sneezed" requires an argument of type h, there is a type mismatch when we apply the two terms. However, "sneeze" has the optional distributivity operator '*', which when we apply it to the lexical semantics for "sneeze" produces the term λ P h→t .∀x h .P(x) ⇒ sneeze(x), which combines with "the students" to produce the reading.

∀x h .(ι(λ Q h→t .|Q| > 1 ∧ ∀y h Q(y) ⇒ student(y)) x) ⇒ sneeze(x)
In other words, all of the members of the contextually determined set of more than human which are all students, sneeze.

The basic idea for the Montagovian Generative Lexicon is that lexical entries specify optional transformations which can repair certain sorts of type mismatches in the syntax-semantics interface. This adaptability allows the framework to solve many semantic puzzles.

Though a proof-of-concept application of these ideas exists, more robust and scalable applications, as well as efforts incorporate these ideas into wide-coverage semantics, are ongoing research.

Theorem proving

When looking at the rules and examples for the different logics, the reader may have wondered: how do we actually find proofs for type-logical grammars? This question becomes especially urgent once our grammars become more complex and the consequences of our lexical entries, given our logic, become hard to oversee. Though pen and paper generally suffice to show that a given sentence is derivable for the desired reading, it is generally much more laborious to show that a given sentence is underivable or that it has only the desired readings. This is where automated theorem provers are useful: they allow more extensive and intensive testing of your grammars, producing results more quickly and with less errors (though we should be careful about too naively assuming the implementation we are using is correct: when a proof is found it is generally easy to verify its correctness by hand, but when a proof isn't found because of a programming error this can be hard to detect).

Though the natural deduction calculi we have seen so far can be used for automated theorem proving [START_REF] Carpenter | A natural deduction theorem prover for type-theoretic categorial grammars[END_REF][START_REF] Moot | The Logic of Categorial Grammars: A Deductive Account of Natural Language Syntax and Semantics[END_REF], and though [START_REF] Lambek | The mathematics of sentence structure[END_REF] already gave a sequent calculus decision procedure, both logics have important drawbacks for proof search.

Natural deduction proofs have a 1-1 correspondence between proofs and readings, though this is somewhat complicated to enforce for a logic with the •E rule (and the related ♦E rule). For the sequent calculus, the product rule is just like the other rules, but sequent calculus suffers from the so-called "spurious ambiguity" problem, which means that it generates many more proofs than readings.

Fortunately, there are proof systems which combine the good aspects of natural deduction and sequent calculus, and which eliminate their respective drawbacks. Proof nets are a graphical representation of proofs first introduced for linear logic [START_REF] Girard | Linear logic[END_REF]. Proof nets suffer neither from spurious ambiguity nor from complications for the product rules.

Proof nets are usually defined as a subset of a larger class, called proof structures. Proof structures are "candidate proofs": part of the search space of a naive proof search procedure which need not correspond to actual proofs. Proof nets are those proof structures which correspond to sequent proofs. Perhaps surprisingly, we can distinguish proof nets from other proof structures by looking only at graphtheoretical properties of these structures.

Proof search for type-logical grammars using proof nets uses the following general procedure.

1. For each of the words in the input sentence, find one of the formulas assigned to it in the lexicon. 2. Unfold the formulas to produce a partial proof structure. 3. Enumerate all proof structures for the given formulas by identifying nodes in the partial proof structure. 4. Check if the resulting proof structure is a proof net according to the correctness condition.

In Sections 9.4.1 and 9.4.2 we will instantiate this general procedure for multimodal type-logical grammar and for first-order linear logic respectively.

Multimodal proof nets

[/E] C C/ i B B i [/I] C/ i B i B C [\E] C A\ i C A i [\I] A\ i C i A C [•E] A i B A • i B [•I] A • i B B A i
Table 9.5 Links for multimodal proof nets Table 9.5 presents the links for multimodal proof nets. The top row list the links corresponding to the elimination rules of natural deduction, the bottom row those corresponding to the introduction rules. There are two types of links: tensor links, with an open center, and par links, with a filled center. Par links have a single arrow pointing to the main formula of the link (the complex formula containing the principal connective). The top and bottom row are up-down symmetric with tensor and par reversed. The tensor links correspond to the logical rules which build structure when we read them from top to bottom, the par links to those rules which remove structure.

The formulas written above the central node of a link are its premisses, whereas the formulas written below it are its conclusions. Left-to-right order of the premisses as well as the conclusions is important.

A proof structure is a set of formula occurrences and a set of links such that:

1. each formula is at most once the premiss of a link, 2. each formula is at most once the conclusion of a link.

A formula which is not the premiss of any link is a conclusion of the proof structure. A formula which is not the conclusion of any link is a hypothesis of the proof structure. We say a proof structure with hypotheses Γ and conclusions ∆ is a proof structure of Γ ∆ (we are overloading of the ' ' symbol here, though this use should always be clear from the context; note that ∆ can contain multiple formulas).

After the first step of lexical lookup we have a sequent Γ C, and we can enumerate its proof structures as follows: unfold the formulas in Γ ,C, unfolding them so that the formulas in Γ are hypotheses and the formula C is a conclusion of the resulting structure, until we reach the atomic subformulas (this is step 2 of the general procedure), then identify atomic subformulas (step 3 of the general procedure, we turn to the last step, checking correctness, below). This identification step can, by the conditions on proof structures only identify hypotheses with conclusions and must leave all formulas of Γ , including atomic formulas, as hypotheses and C as a conclusion. To turn this proof structure into a proof structure of a/ a b, b/ a c a/ a c, we identify the atomic formulas. In this case, there is only a single way to do this, since a, b and c all occur once as a hypothesis and once as a conclusion, though in general there may be many possible matchings. Figure 9.7 shows, on the left, the proof structure after identifying the a and b formulas. Since left and right (linear order), up and down (premiss, conclusion) have meaning in the graph, connecting the c formulas is less obvious: c is a conclusion of the /I link and must therefore be below it, but a premiss of the /E link and must therefore be above it. This is hard to achieve in the figure shown on the left. Though a possible solution would be to draw the figure on a cylinder, where "going up" from the topmost c we arrive at the bottom one, for ease of type-setting and reading the figure, I have chosen the representation shown in Figure 9.7 on the right. The curved line goes up from the c premiss of the /E link and arrives from below at the /I link, as desired. One way so see this strange curved connection is as a graphical representation of the coindexation of a premiss with a rule in the natural deduction rule for the implication.

Figure 9.7 therefore shows, on the right, a proof structure for a/ a b, b/ a c a/ a c. However, is it also a proof net, that is, does it correspond to a proof? In a multimodal logic, the answer depends on the available structural rules. For example, if no structural rules are applicable to mode a then a/ a b, b/ a c a/ a c is underivable, but if mode a is associative, then it is derivable. We decide whether a proof structure is a proof net based only on properties of the graph. As a first step, we erase all formula information from the internal nodes of the graph; for administrative reasons, we still need to be able to identify which of the hypotheses and conclusion of the structure correspond to which formula occurrence 5 . All relevant information for correctness is present in this graph, which we call an abstract proof structure.

We talked about how the curved line in proof structures (and abstract proof structure) corresponds to the coindexation of discharged hypotheses with rule names for 5 We make a slight simplification here. A single vertex abstract proof structure can have both a hypothesis and a conclusion without these two formulas necessarily being identical, e.g. for sequents like (a/b) • b a. Such a sequent would correspond to the abstract proof structure

(a/b)•b • a .
So, formally, both the hypotheses and the conclusions of an abstract proof structure are assigned a formula and when a node is both a hypothesis and a conclusion it can be assigned two different formulas. In order not to make the notation of abstract proof structure more complex, we will stay with the simpler notation. [START_REF] Moot | Proof nets for the multimodal Lambek calculus[END_REF] present the full details.

the implication introduction rules. However, the introduction rules for multimodal type-logical grammars actually do more than just discharge a hypothesis, they also check whether the discharged hypothesis is the immediate left (for \I) or right (for /I) daughter of the root node, that is, that the withdrawn hypothesis A occurs as A • i Γ (for \I and mode i) or Γ • i A (for /I and mode i). The par links in the (abstract) proof structure represent a sort of "promise" that will produce the required structure. We check whether it is satisfied by means of contractions on the abstract proof structure.

[/I] i i [•E] i i [\I] i i Table 9.6 Contractions -multimodal binary connectives
The multimodal contractions are shown in Table 9.6. All portrayed configurations contract to a single vertex: we erase the two internal vertices and the paired links and we identify the two external vertices, keeping all connections of the external vertices to the rest of the abstract proof structure as they were: the vertex which is the result of the contraction will be a conclusion of the same link as the top external vertex (or a hypothesis of the abstract proof structure in case it wasn't) and it will be a premiss of the same link as the bottom external vertex (or a conclusion of the abstract proof structure in case it wasn't).

The contraction for /I checks if the withdrawn hypothesis is the right daughter of a tensor link with the same mode information i, and symmetrically for the \I contraction. The •E contraction contracts two hypotheses occurring as sister nodes.

All contractions are instantiations of the same pattern: a tensor link and a par link are connected, respecting left-right and up-down the two vertices of the par link without the arrow.

To get a better feel for the contractions, we will start with its simplest instances. When we do pattern matching on the contraction for /I, we see that it corresponds to the following patterns, depending on our choice for the tensor link (the par link is always /I).

C/ i B C/ i B A (A • i B)/ i B A C/ i (A\ i C)
A proof structure is a proof net iff it contracts to a tree containing only tensor links using the contractions of Table 9.6 and any structural rewrites, discussed below - [START_REF] Moot | Proof nets for the multimodal Lambek calculus[END_REF] present full proofs. In other words, we need to contract all par links in the proof structure according to their contraction, each contraction ensuring the correct application of the rule after which it is named. The abstract proof structure on the right of Figure 9.8 does not contract, since there is no substructure corresponding to the /I contraction: for a valid contraction, a par link is connected to both "tentacles" of a single tensor link, and in the figure the two tentacles without arrow are connected to different tensor links. This is correct, since a/ a b, b/ a c a/ a c is underivable in a logic without structural rules for a.

However, we have seen that this statement becomes derivable once we add associativity of a and it is easily verified to be a theorem of the Lambek calculus. How can we add a modally controlled version of associativity to the proof net calculus?

We can add such a rule by adding a rewrite from a tensor tree to another tensor tree with the same set of leaves. The rewrite for associativity is shown in Figure 9.9. To apply a structural rewrite, we replace the tree on the left hand side of the arrow by the one on the right hand side, reattaching the leaves and the root to the rest of the proof net.

Just like the structural rules, a structural rewrite always has the same leaves on both sides of the arrow -neither copying nor deletion is allowed6 , though we can reorder the leaves in any way (the associativity rule doesn't reorder the leaves). We start with a structural rewrite, which rebrackets the pair of tensor links. The two hypotheses are now the premisses of the same link, and this also produces a contractible structure for the /I link. Hence, we have shown the proof structure to be a proof net. In the Grail theorem prover, the representation of abstract proof structures looks as shown in Figure 9.11 (this is an automatically produced subgraph close to the graph on the left of Figure 9.10, though with a non-associative mode n and therefore not derivable). This graph is used during user interaction. The graphs are drawn using GraphViz, an external graph drawing program which does not guarantee respecting our desires for left, right and top/bottom, so tentacles are labeled 1, 2 and 3 (for left, right and top/bottom respectively) to allow us to make these distinctions regardless of the visual representation. Vertices are given unique identifiers for user interaction, for example to allow specifying which pair of atoms should be identified or which par link should be contracted.

Although the structural rules give the grammar writer a great deal of flexibility, such flexibility complicates proof search. As discussed at the beginning of Section 9.4, theorem proving using proof nets is a four step process, which in the current situation looks as follows: 1) lexical lookup, 2) unfolding, 3) identification of atoms, 4) graph rewriting. In the current case, both the graph rewriting and the identification of atoms are complicated7 and since we can interleave the atom connections and the graph rewriting it is not a priori clear which strategy is optimal for which set of structural rules. The current implementation does graph rewriting only once all atoms have been connected.

The Grail theorem prover implements some strategies for early failure. Since all proofs in multimodal type-logical grammars are a subset of the proofs in multiplicative linear logic, we can reject (partial) proof structures which are invalid in multiplicative linear logic, a condition which is both powerful and easy to check.

As a compromise between efficiency and flexibility, Grail allows the grammar writer to specify a first-order approximation of her structural rules. Unlike the test for validity in multiplicative linear logic which is valid for any set of structural rules, specifying such a first-order approximation is valid only when there is a guarantee that all derivable sequents in the multimodal grammar are a subset of their approximations derivable in first-order linear logic. Errors made here can be rather subtle and hard to detect. It is recommended to use such methods to improve parsing speed only when a grammar has been sufficiently tested and where it is possible to verify whether no valid readings are excluded, or, ideally, to prove that the subset relation holds between the multimodal logic and its first-order approximation.

The next section will discuss first-order proof nets in their own right. Though these proof nets have been used as an underlying mechanism in Grail for a long time, we have seen in Section 9.3.2 that many modern type-logical grammars are formulated in a way which permits a direct implementation without an explicit set of structural rules.

As to the proof search strategy used by Grail, it is an instance of the "dancing links" algorithm (Knuth, 2000): when connecting atomic formulas, we always link a formula which has the least possibilities and we rewrite the abstract proof structures only once a fully linked proof structure has been produced. Though the parser is not extremely fast, evaluation both on randomly generated statements and on multimodal statements extracted from corpora show that the resulting algorithm performs more than well enough [START_REF] Moot | Wide-coverage French syntax and semantics using Grail[END_REF].

First-order proof nets

Proof nets for first-order linear logic [START_REF] Girard | Quantifiers in linear logic II[END_REF] are a simple extension of the proof nets for standard, multiplicative linear logic [START_REF] Danos | The structure of multiplicatives[END_REF]. Compared to the multimodal proof nets of the previous section, all logical links have the main formula of the link as their conclusion but there is now a notion of polarity, corresponding to whether or not the formula occurs on the left hand side of the turnstile (negative polarity) or on the right hand side (positive polarity).

We unfold a sequent A 1 , . . . , A n C by using the negative unfolding for each of the A i and the positive unfolding for C. The links for first-order proof nets are shown in Table 9.7.

- A + A - A + A - ∀x.A - A[x := t] + ∀x.A + A x - ∃x.A - A x - A ⊗ B - A - B + A ⊗ B + A + B + ∃x.A + A[x := t] - A B + A - B + A B - A + B
Table 9.7 Logical links for MILL1 proof structures Contrary to multimodal proof nets, where a tensor link was drawn with an open central node and a par link with a filled central node, here par links are drawn as a connected pair of dotted lines and tensor links as a pair of solid lines.

As before, premisses are drawn above the link and conclusions are drawn below it. With the exception of the cut and axiom links, the order of the premisses and the conclusions is important. We assume without loss of generality that every quantifier link uses a distinct eigenvariable.

A set of formula occurrences connected by links is a proof structure if every formula is at most once the premiss of a link and if every formula is exactly once the conclusion of a link. Those formulas which are not the premiss of any link are the conclusions of the proof structure -note the difference with multimodal proof nets: a proof structure has conclusions but no hypotheses and, as a consequence, each formula in the proof net must be the conclusion of exactly one (instead of at most one) link.

For polarised proof nets, unfolding the formulas according to the links of Table 9.7 no longer produces a proof structure, since the atomic formulas after unfolding are not the conclusions of any link. Such "partial proof structures" are called a modules. To turn a module into a proof structure, we connect atomic formulas of opposite polarity by axiom links until we obtain a complete matching of the atomic formulas, that is until every atomic formula is the conclusion of an axiom link.

The negative ∀ and the positive ∃ link, are defined using substitution of an arbitrary term t for the eigenvariable of the link. In actual proof search, we use unification of these variables when the axiom links are performed.

As usual, not all proof structures are proof nets. However, since the logical rules for the quantifiers make essential use of the notion of "free occurrence of a variable", this should be reflected in out correctness condition. [START_REF] Girard | Quantifiers in linear logic II[END_REF] uses a notion of switching for proof structures which extends the switchings of [START_REF] Danos | The structure of multiplicatives[END_REF].

A switching is, for each of the binary par links a choice of its left or right premiss and for each of the unary par links with eigenvariable x a choice of one of the formulas in the structure with a free occurrence of x or of the premiss of the rule.

Given a switching, a correction graph replaces a binary par link by a connection from the conclusion of the link to the premiss chosen by the switching, and it replace a unary par link by a link from the conclusion to the formula chosen by the switching.

Finally, a proof structure is a proof net when all its correction graphs are both acyclic and connected [START_REF] Girard | Quantifiers in linear logic II[END_REF].

As an example, look at the proof structure of a ∃x.b(x) ∃y.[a b(y)] shown in Figure 9.12. This statement is not derivable in first-order linear logic (nor in intuitionistic logic). Consider therefore the switching connecting the binary par link to its left premiss a and the link for x to the formula a b(x) (it has a free occurrence of x, so this like is a valid switching). This switching produces the correction graph shown in Figure 9.13. It contains a cycle, drawn with bold edges, and is therefore not a proof structure (in addition, the b axiom is disconnected from the rest of the structure, giving a second reason for rejecting the proof structure).

Contractions

Though switching conditions for proof nets are simple and elegant, they don't lend themselves to naive application: already for the example proof structure of Figure 9.12 there are six possible switchings to consider and, as the reader can verify, only the switching shown in Figure 9.13 is cyclic (and disconnected). In general, it is often the case that all switchings but one are acyclic and connected, as it is here. Though there are efficient ways of testing acyclicity and connectedness for multiplicative proof nets [START_REF] Guerrini | Correctness of multiplicative proof nets is linear[END_REF][START_REF] Murawski | Dominator trees and fast verification of proof nets[END_REF] and it seems these can be adapted to the first-order case (though some care needs to be taken when we allow complex terms), the theorem prover for first-order linear logic uses a extension of the contraction criterion of [START_REF] Danos | La logique linéaire appliquée à l'étude de divers processus de normalisation (principalement du λ -calcul)[END_REF].

Given a proof structure we erase all formulas from the vertices and keep only a set of the free variables at this vertex. We then use the contractions of Table 9.8 to contract the edges of the graph. The resulting vertex of each contraction has the union of the free variables of the two vertices of the redex (we remove the eigenvariable x of a ∀ contraction, " ⇒ u "). A proof structure is a proof net iff it contracts to a single vertex using the contractions of Table 9.8.

v i v j v i ⇒ p v i v j x v i ⇒ u v i v j v i ⇒ c
Table 9.8 Contractions for first-order linear logic. Conditions: v i = v j and, for the u contraction, all free occurrences of x are at v j .

To give an example of the contractions, Figure 9.14 shows the contractions for the underivable proof structure of Figure 9.12. The initial structure, which simply takes the proof structure of Figure 9.12 and replaces the formulas by the corresponding set of free variables, is shown on the left. Contracting the five solid edges using the c contraction produces the structure shown in the figure on the right. No further contractions apply: the two connected dotted links from the binary par link do not end in the same vertex, so the par contraction p cannot apply. In addition, the universal contraction u cannot apply either, since it requires all vertices with its eigenvariable x to occur at the node from which the arrow is leaving and there is another occurrence of x at the bottom node of the structure. We have therefore shown that this is not a proof net.

Since there are no structural rewrites, the contractions for first-order linear logic are easier to apply than those for multimodal type-logical grammars: it is rather easy to show confluence for the contractions (the presence of structural rules, but also the unary versions of the multimodal contractions, means confluence is not guaranteed for multimodal proof nets). We already implicitly used confluence when we argued that the proof structure in Figure 9.14 was not a proof net. The theorem prover uses a maximally contracted representation of the proof structure to represent the current state of proof search and this means less overhead and more opportunities for early failure during proof search.

Like before, the theorem proving uses four steps, which look as follows in the first-order case: 1) lexical lookup, 2) unfolding, 3) axiom links with unification, 4) graph contraction. Unlike the multimodal proof nets of the previous section, the graph contractions are now confluent and can be performed efficiently (the linear time solutions for the multiplicative case may be adaptable, but a naive implementation already has an O(n 2 ) worst-case performance). After lexical lookup, theorem proving for first-order linear logic unfolds the formulas as before, but uses a greedy contraction strategy. This maximally contracted partial proof net constrains further axiom links: for example, a vertex containing a free variable x cannot be linked to the conclusion of the edge of its eigenvariable (the vertex to which the arrow of the edge with variable x points) or to one of its descendants, since such a structure would fail to satisfy the condition that the two vertices of a ∀ link for the u contraction of Figure 9.8 are distinct. Another easily verified constraint is that two atomic formulas can only be connected by an axiom link if these formulas unify8 . Like for multimodal proof nets, the first-order linear logic theorem prover chooses an axiom link for one of the atoms with the fewest possibilities.

Tools

Table 9.9 lists the different theorem provers which are available. Grail 0 [START_REF] Moot | The Logic of Categorial Grammars: A Deductive Account of Natural Language Syntax and Semantics[END_REF] and Grail 3 (Moot, 2015a) use the multimodal proof net calculus of Section 9.4.1, whereas LinearOne [START_REF] Moot | Linear one: A theorem prover for first-order linear logic[END_REF] uses the first-order proof nets of Section 9.4.2. GrailLight (Moot, 2015b) is a special-purpose chart parser, intended for use with an automatically extracted French grammar for wide-coverage parsing and semantics [START_REF] Moot | Wide-coverage French syntax and semantics using Grail[END_REF][START_REF] Moot | Wide-coverage semantics for spatio-temporal reasoning[END_REF]. All provers are provided under the GNU Lesser General Public License -this means, notably, there is no warranty, though I am committed to making all software as useful as possible; so contact me for any comments, feature requests or bug reports. All theorem provers can be downloaded from the author's GitHub site. https://github.com/RichardMoot/ The columns of table Table 9.9 indicate whether the theorem provers provide natural deduction output, graph output (of the partial proof nets), whether there is an interactive mode for proof search, whether the implementation is complete and whether the grammar can specify its own set of structural rules; "NA" means the question doesn't apply to the given system (GrailLight doesn't use a graphs to represent proofs and first-order linear logic does not have a grammar-specific set of structural rules). The table should help you select the most adequate tool for your purposes.

LinearOne provides natural deduction output not only for first-order linear logic, but also for the Displacement calculus, hybrid type-logical grammars and lambda grammars. That is, the grammar writer can write a grammar in any of these formalisms, LinearOne will do proof search of the translation of this grammar in firstorder linear logic and then translate any resulting proofs back to the source language. The syntactic example proofs in this chapter have been automatically generated using these tools and the corresponding grammars files, as well as many other example grammars, are included in the repository.

Fig. 9 . 1

 91 Fig. 9.1 The standard architecture of type-logical grammars

  ∀x.[student(x) ⇒ ∃y.[exam(y) ∧ ace(x, y)]]

Fig. 9 . 3

 93 Fig. 9.3 Deep structure of the derivation of Figure 9.2.

Fig. 9 . 4

 94 Fig. 9.4 Intuitionistic proof and lambda term corresponding to the deep structure of Figure 9.3.

Fig. 9

 9 Fig. 9.5 "De re" reading for the sentence "Alyssa believes someone committed perjury".

  Fig. 9.6 Lexical unfolding of a/ a b, b/ a c a/ a c

  Fig. 9.8 The proof structure of Figure 9.7 (left) and its abstract proof structure (right)

  Fig.9.9 Structural rewrites for associativity of mode a.

Figure 9 .

 9 Figure 9.10 shows how the contractions and the structural rewrites work together to derive a/ a b, b/ a c a/ a c.We start with a structural rewrite, which rebrackets the pair of tensor links. The two hypotheses are now the premisses of the same link, and this also produces a contractible structure for the /I link. Hence, we have shown the proof structure to be a proof net.

  Fig. 9.10 Structural rewrite and contraction for the abstract proof structure of Figure 9.8, showing this is a proof net for a/ a b • a b/ a c a/ a c

Fig. 9 .

 9 Fig. 9.12 Proof structure for a ∃x.b(x) ∃y.[a b(y)].

Fig. 9 .

 9 Fig. 9.13 Correction graph for the proof structure of Figure 9.12 with the cycle indicated, showing a ∃x.b(x) ∃y.[a b(y)] is underivable

  Fig. 9.14 Contractions for the underivable a ∃x.b(x) ∃y.[a b(y)].

Table 9

 9

.1 Natural deduction for L

Table 9

 9

.2 Lambek calculus lexicon

Table 9

 9

.4 Natural deduction rules for MILL1

∆ A • B Γ , A, B,Γ C Γ , ∆ ,Γ C [•E] Γ A ∆ B Γ , ∆ A • B [•I] Γ A/B ∆ B Γ , ∆ A [/E] Γ , B A Γ A/B [/I]

We have used the standard convention in Montague grammar of writing (p x) as p(x) and ((p y) x) as p(x, y), for a predicate symbol p.

We can also allow unary branches (and, more generally n-ary branches) and the corresponding logical connectives. The unary connectives ♦ and are widely used, but, since they will only play a marginal role in what follows, I will not present them to keep the current presentation simple. However, they form an essential part of the analysis of many phenomena and are consequently available in the implementation.

This is where the structural rules, shown at the bottom of Table9.3 come in. The general form, read from top to bottom, states that we take a structure Γ containing a distinguished subtree Ξ which itself has n subtrees ∆ 1 , . . . , ∆ n , and we replace this subtree Ξ with a subtree Ξ which has the same number of subtrees, though not necessarily in the same order (π is a permutation on the leaves). In brief, we replace a subtree Ξ by another subtree Ξ and possibly rearrange the leaves (subtrees) of Ξ , without deleting or copying any subtrees. Examples of structural rules are the following.

The Grail theorem prover: Type theory for syntax and semantics

From the point of view of linear logic, we stay within the purely multiplicative fragment, which is simplest proof-theoretically.

Lexical ambiguity is a major problem for automatically extracted wide-coverage grammars as well, though standard statistical methods can help alleviate this problem[START_REF] Moot | Wide-coverage French syntax and semantics using Grail[END_REF].

As discussed in Section

9.4.1, the multimodal theorem prover allows the grammar writer to specify first-order approximations of specific formulas. So underneath the surface of Grail there is some first-order reasoning going on as well.