Bekki Laboratory

Research Projects

The Bekki Laboratory specializes in mathematical linguistics, an interdisciplinary field at the intersection of linguistics, logic, philosophy, and natural language processing. The laboratory has produced three principal research achievements in this field. First, in formal syntax, we have constructed a comprehensive, formal, and integrated theory of Japanese grammar based on Combinatory Categorial Grammar (CCG). Second, in formal semantics, we have proposed a new framework called "Dependent Type Semantics (DTS)," a compositional proof-theoretic discourse semantics grounded in dependent type theory. Third, in natural language processing, we have completed an entailment recognition system, "ccg2lambda," which combines a robust CCG parser with higher-order logic-based automated reasoning. Taken together, these three research strands provide a unified research program capable of addressing the question of theoretical linguistics—how strings of symbols correspond to meanings—the question of philosophy of language—what meaning is—and the question of natural language processing—by what mechanism humans understand the meaning of sentences.

The study of the syntax and semantics of natural languages such as Japanese and English—that is, the study of the mechanisms by which strings of symbols are mapped to meanings—can be approached from two research perspectives: theoretical linguistics and natural language processing. The former is "linguistics as a natural science," typified by generative grammar initiated by Chomsky and formal semantics initiated by Montague. The latter is computer science aimed at processing natural language computationally—for example, realizing artificial intelligence that understands human language, or improving the quality of services that use natural language as an interface.

Ideally, the theory provided by the former, or an approximation thereof, should also provide solutions in the latter. In reality, however, the two diverged in the late 1980s to mid-1990s and became almost entirely unrelated, both in content and in personnel. The mathematical models used in natural language processing departed greatly from the formal language theory and higher-order intensional logic employed by theoretical linguistics, and machine learning methods using statistical and neural models became dominant. In recent years, language processing based on deep learning has attracted particular attention, but—contrary to the impression generally held—the scope of "meaning" that current Japanese language processing can understand is limited, in general, to the relationships between predicates and names within simple sentences (called predicate-argument structure). Beyond that, it can only make rough inferences, and there is currently no prospect of systematically handling the various semantic relations that formal semantics has aimed to account for (negation, modality, tense, conditionals, anaphora, presupposition, conventional implicature, etc. (†described below)).

When given a sentence of natural language, humans understand its meaning and can be conscious of it, but they are not conscious of the process by which they understand the sentence. Consequently, what it means to "understand a sentence" is not self-evident even to researchers in language processing. It is theoretical linguistics that provides analytical methods for approaching this problem.

On the side of theoretical linguistics, several conceptual advances have been made since the split from natural language processing up to the present. 1) Theoretical foundations of formal syntax: A rich relationship (Ono 1990) was discovered between formal syntax and logic, especially proof theory, and research on "categorial grammar"—a framework that captures universal constraints on language more naturally than Chomsky's generative grammar—progressed. In particular, with the advent of Combinatory Categorial Grammar (CCG: Steedman 1996), the problem of coordination constructions, which had been a major shared problem for both generative grammar and natural language processing, was resolved. 2) Empirical foundations of formal syntax: The data and verification methods in generative grammar were reinterpreted, laying the groundwork for advancing introspective linguistics as a rigorous science (Hoji 2015). 3) The emergence of dependent type theory and proof assistants: Dependent type theory (DTT: Martin-Löf 1984), known as a foundational theory for constructive mathematics, became better understood in terms of its computational properties, and proof assistants/theorem provers based on dependent type theory, such as Coq, emerged.

Against this background, the present research aims to build a theory that elucidates the structure of the syntax and meaning of natural language, while striving toward the realization of "artificial intelligence that understands human language." Such a theory is divided into three components: (A) syntax, (B) semantics and pragmatics, and (C) implementation. The theories in (A) and (B) must simultaneously possess comprehensiveness for linguistic phenomena, formal rigor sufficient for computer implementation, and computational efficiency.

For the syntactic component, we completed a formal grammar of Japanese based on Combinatory Categorial Grammar and higher-order dynamic logic, and published it in 2010 as a book: The Formal Theory of Japanese Grammar—Inflectional System, Syntactic Structure, and Semantic Composition (Kuroshio Publishers). This theory has been evaluated as "research unprecedented in the history of Japanese grammar" for simultaneously satisfying "comprehensiveness for linguistic phenomena in Japanese," "formal rigor sufficient for computer processing," and "theoretical integration spanning the inflectional system, syntactic structure, and semantic composition." We also conduct research on the theoretical study of combinatory categorial grammar, the analysis of scrambling phenomena in Japanese using CCG, and the analysis of honorifics, among other topics.

For the semantic computation component, we announced Dependent Type Semantics (DTS), a discourse semantics using dependent type theory, in 2014. As a textbook providing the background knowledge needed to understand the DTS framework, we also published Mathematical Logic (University of Tokyo Press) in 2012. DTS is a theory of meaning grounded in proof-theoretic semantics (derived from Gentzen, Prawitz, and Dummett) rather than the model-theoretic semantics that is mainstream in linguistics (derived from Tarski, Davidson, and Montague). A particular feature of DTS is that the phenomenon of "anaphora resolution and presupposition binding"—known to be inexpressible in first-order predicate logic—can be computed using general techniques developed in functional programming (type checking and type inference). DTS is also a theory capable of describing the full range of semantic phenomena in natural language mentioned in (†) above; it has achieved results in the analysis of phenomena such as "generalized quantifiers"—a form of quantification inexpressible in first-order predicate logic—modality-involving anaphora and presupposition, factive predicates, and the challenging phenomena of "bridging inference" and "coercion" in anaphora resolution. Research on other semantic frameworks, including categorical semantics and delimited continuations, is also conducted.

In the pragmatic computation component, for example, "conventional implicature" is a phenomenon that exhibits an inference pattern distinct from entailment and presupposition. By analyzing it from the perspective of proof-theoretic semantics, we showed that the problem of semantic composition that had remained unsolved in prior research could be resolved. This is an outcome of the Grant-in-Aid for Scientific Research (C), "Computational semantics and pragmatics of politeness phenomena" (Principal Investigator: Professor Eric McCready), in which we served as a co-investigator.

For the implementation component, we constructed an inference system "ccg2lambda" that, for multiple natural language sentences, computes semantic composition in higher-order logic representations from the output of a robust CCG parser and then performs automated reasoning using the theorem prover Coq. This is an outcome of the "Establishment of Knowledge-Intensive Structural Language Processing and Construction of a Knowledge Infrastructure" project (FY2013–2018, Principal Investigator: Professor Sadao Kurohashi, JST CREST "Research Area: Creation and Systematization of Next-Generation Fundamental Technologies for Big Data Integration and Utilization"), conducted jointly with members of the Bekki Laboratory at Ochanomizu University (publicly available at: https://github.com/mynlp/ccg2lambda). Verification was performed using the FraCaS test suite (Cooper et al. 1996), achieving an accuracy of 69% against 50% for the state-of-the-art reasoning system based on first-order predicate logic (Nutcracker, Bos et al. 2008).

What is Formal Semantics?

Formal semantics is a natural science whose object is the meaning of natural language. As the semantic component of theoretical linguistics, it typically takes the following structure:

1. Takes some position on the question of what the meaning of natural language is, and defines a formal language for representing meanings.
2. Takes some position on the syntax of natural language.
3. Provides a mechanism for computing, for any given sentence or discourse of the language in question, a meaning representation according to the structure given by the syntax in 2., using the approach in 1.
4. Performs empirical verification by comparing, for individual sentences or discourses of the language, the meanings predicted by 3. with the linguistic intuitions of native speakers. Errors are traced back to 1., 2., or 3. (usually 3.) and corrections are made.

Research in formal semantics began with a series of papers by R. Montague in the early 1970s[39]. Generally known as Montague Grammar, its emergence was the product of various developments in computer science, theoretical linguistics, logic, and philosophy of language from the 1940s to the 1960s. First, the development of theoretical computer science by A. Turing, A. Church, H. Curry and others from the 1930s onward gave rise to typed lambda calculus. Second, N. Chomsky's generative grammar, beginning in the 1950s, put forward the concept of universal grammar and the paradigm of "theoretical linguistics as a natural science." Third, the development of formal language theory brought by Chomsky led J. Lambek and others to revive categorial grammar (devised by K. Ajdukiewicz in the 1930s) as a syntactic theory for natural language. Fourth, because S. Kripke provided Kripke semantics for the modal logic of C. I. Lewis, model-theoretic semantics for modal logic was established and became widely used in computer science and philosophy of language. Fifth, D. Davidson's truth-conditional semantics for natural language had emerged.

Montague Grammar adopted, for point 1., the position of D. Davidson's truth-conditional semantics, holding that "the meaning of a sentence is its truth conditions." This remains the standard position in formal semantics to this day. It also defined an original logical system called intensional logic—a fusion of higher-order modal logic and typed lambda calculus—and provided truth conditions for each logical formula by its model theory. For point 2. in syntax, it designed an original categorial grammar and covered a fragment of English (the reason Montague's theory was called Montague Grammar), while for point 3., a dictionary assigning intensional logic representations to each word in that fragment and semantic composition rules parallel to each rule of the categorial grammar were specified. By this means, for any sentence generated by the categorial grammar, a meaning representation in intensional logic can be computed. For point 4., the problems of quantifier scope ambiguity and de re/de dicto readings—classic problems in philosophy of language—were resolved in a unified manner.

Montague Grammar has two features not found in earlier philosophy of language, which have shaped subsequent formal semantics research. The first is that it made explicit the process of mapping from the structures given by syntax to meaning representations. In Montague's formulation, there is a strong correspondence between syntax and semantics, in the sense that semantic composition rules are applied in parallel with syntactic rules—this is the forerunner of the position called lexical grammar or lexicalism. Technically, what made lexicalization of intensional logic possible was its fusion with typed lambda calculus. However, lexicalization is not a necessary requirement for formal semantics; it is only one method of "mapping from the structures given by syntax to meaning representations." It is the existence of such a mapping that distinguishes formal semantics from earlier philosophy of language.

In the philosophy of language before Montague, when analyzing the meaning of sentences using logical representations, no theory was provided for correlating logical representations with sentences. This means that such language-philosophical analyses do not yield predictions for unknown sentences. Montague Grammar, by contrast, can predict truth conditions for any sentence (within the fragment of English covered by the categorial grammar). As a result, this feature brings falsifiability to semantic research. Falsifiability, together with the reproducibility of empirical data, is what K. Popper identified as the criterion distinguishing natural science from pseudoscience[43]. Yet this naturalistic attitude found in formal semantics may also be seen as a culture brought by the generative grammar that developed contemporaneously.

The second feature of Montague Grammar is the adoption of non-classical logic. In logic, through the development of proof theory and model theory, the structures implicitly assumed by classical logic (bivalence, the law of double negation, structural rules, etc.) became apparent, and accordingly the properties of logical systems lacking some or all of those structures were carefully studied. J.-Y. Girard's linear logic and J. Lambek's Lambek calculus are examples. The significance of such logical systems was not well recognized until the first half of the twentieth century, but it became one of the major themes of logic in the second half, when computer science relativized logic. Classical logic is no longer "the only" logic; an awareness emerged that one may design new logical systems suited to the object of analysis. Moreover, as the concept of "computation" became a new object of logical analysis, the computational process of understanding natural language meaning also became an object of this relativized logical analysis. In this sense, an understanding of modern logic is essential to understanding formal semantics.

Alongside these new features, Montague Grammar more prominently inherited the characteristic of logic-based philosophy of language: "formalization of a theory promotes the discovery of new linguistic phenomena." The formal rigor and falsifiability of Montague Grammar promoted the discovery of linguistic phenomena that Montague Grammar itself could not handle. These include diverse phenomena such as generalized quantifiers, modality, presupposition, genericity, kinds, plurality, coordination, events, questions, focus, conditionals, and disjunction. As formal semantics developed, problems surrounding these phenomena were recognized, and problems arising from their interactions were also brought to light. For further details, see[44] and[30]. To address these problems, formal semantics has, following the spirit of non-classical logic, attempted resolutions by designing new logical systems.

One major development that emerged from this is Discourse Representation Theory (DRT) by H. Kamp, I. Heim, and others[27][24]. Montague Grammar covered only the meaning of single sentences, but when considering phenomena such as inter-sentential anaphora and tense, it became necessary to analyze the meaning of discourse composed of multiple sentences. Moreover, as P. Geach's work[20] made known, even intra-sentential anaphora in donkey sentences was shown to have a structure parallel to inter-sentential anaphora. Early DRT introduced a representational language called Discourse Representation Structures, which significantly modified the existential quantification structure of first-order predicate logic, attempting to capture the dynamic aspect of anaphora. In the 1990s, Dynamic Predicate Logic (DPL) by J. Groenendijk, M. Stokhof, and others[22] emerged. Dynamic semantics resolves the problem that the procedure for obtaining meaning representations in DRT is not compositional; it transposes dynamic logic—a modal logic for capturing side effects in programming—to semantics for natural language. Through subsequent revisions of DRT, however, the two converged into a single theory. In that development, a unified theory of presupposition and anaphora was proposed by R. van der Sandt and R. Geurts[54], and discourse theory was unified with DRT through N. Asher et al.'s Segmented DRT (SDRT[2]), so that formal semantic analysis made great strides from the 1990s to the early 2000s.

Another major development is the fusion with generative grammar by B. Partee, I. Heim, and others[26]. R. Montague's categorial grammar could cover only a fragment of English, and formal semantics research required a full syntactic component. Meanwhile, N. Chomsky's generative grammar, in the 1980s, took the option of excluding discussion of language meaning from its scope of explanation. Therefore, it was natural to demand fusing Montague Grammar (minus its syntactic component) with generative grammar. From this period, Montague Grammar came to be called Montague semantics.

The fusion with generative grammar provided an opportunity for linguists without a background in logic to enter the field of formal semantics. This gave rise to a position that uses logical representations as a tool for describing linguistic phenomena, creating a situation in which "semantics as a natural science," as described above, and "descriptive semantics using logical representations as a descriptive language," coexist. Present-day formal semantics is an interdisciplinary field into which diverse personnel from linguistics (other than formal semantics), logic, philosophy of language, and natural language processing move in and out, and various forms of research exist depending on which of points 1.–4. above is emphasized (or de-emphasized).

Furthermore, while the methods used in theory construction have expanded to cover all manner of logical systems, since the use of logic as a basis is not itself a necessary requirement for formal semantics, all manner of mathematical models—probabilistic models, category theory, functional programming, and others—have begun to be employed. The topics addressed also range beyond traditional semantic problems to include linguistic phenomena such as polysemy and metaphor, which cognitive semantics and lexical semantics have proposed as counter-proposals to formal semantics. In addition, there are interactions with computational semantics and semantic processing in natural language processing, and it is becoming increasingly difficult to define the extension of formal semantics.

There are also positions not touched upon in this article, such as Minimal Recursion Semantics (MRS[12]), which grew out of the semantic component of Head-driven Phrase Structure Grammar, but these are not discussed in detail here.

(Originally published: Bekki, Daisuke (2017) "Formal Semantics," Encyclopedia of Artificial Intelligence, Japanese Society for Artificial Intelligence.)

The Proof-Theoretic Turn in Semantics

Since Montague, the mainstream in natural language semantics has been model-theoretic semantics, in which the meaning of a sentence is held to be its truth conditions. Meanwhile, from the 1980s, phenomena such as E-type anaphora[16] and (semantic) presupposition[25]—known to be inexplicable within first-order predicate logic or Montague's intensional logic—became recognized, motivating the emergence of Discourse Representation Theory (DRT:[27]) and File Change Semantics (FCS:[24]). In the 1990s, Dynamic Predicate Logic (DPL:[22]) was proposed, and attempts began to reconceive the meaning of a sentence not as truth conditions but as a Context Change Potential (CCP). Moreover, a unified theory of E-type anaphora and (semantic) presupposition within DRT was presented by[54], and the dynamic conception of meaning—in the form of CCP—has been increasingly accepted, leading into the 2000s and beyond.

What is interesting about these developments arising from formal semantics as a descendant of philosophy of language is that the analysis of specific linguistic phenomena—such as anaphora and (semantic) presupposition (however universal those phenomena may be)—demands the rejection of a specific position in philosophy of language (truth-conditional semantics) concerning the question "what is the meaning of language." However, whether the acceptance of CCP as the alternative is the only conclusion required by linguistic phenomena such as anaphora and (semantic) presupposition must be examined more carefully.

In this regard, it deserves greater attention that there exists a current in natural language semantics different from truth-conditional semantics. This is the current of proof-theoretic semantics stemming from Sundholm, Ranta, Cooper, and Luo. Studies of the meaning of natural language based on dependent type theory include[49][47][11][32] and others. Proof-theoretic semantics for natural language based on systems other than dependent type theory include[18] and[19], and model-theoretic semantics for natural language using dependent type theory includes[23]; comparisons with these will be addressed on another occasion.

Whereas model-theoretic semantics is the position that the meaning of a sentence is its truth conditions, proof-theoretic semantics originates from the position that the meaning of a sentence is its verification conditions[14][15]. Truth-conditional semantics has its origin in Tarski's semantics for mathematics, while verification-conditional semantics traces back to the semantics for mathematics developed by Gentzen and Prawitz[21][46].

In particular, when Martin-Löf's dependent type theory[35] is employed as the theoretical apparatus, expressions representing "proofs" can be used within logical formulas. This makes it possible to give an entirely different explanation of the phenomena—such as E-type anaphora and (semantic) presupposition—whose analysis was the original motivation for introducing dynamic semantics into formal semantics.

Furthermore, in our recent research (see[5][8][7]), it has been shown that the proof-theoretic semantics of Ranta and others can be reconstructed as a compositional semantics, and it is also becoming clear that it has empirical and computational advantages over dynamic semantics. We call this recent development in semantics the "proof-theoretic turn."

The Proof-Theoretic Turn in Formal Semantics

Dependent type theory was devised by Martin-Löf as a logical system forming the foundation of constructive mathematics, and after several revisions, arrived at the current system in[40].

In[3], one of the standard textbooks on lambda calculus and type theory, the system λP—the fragment of dependent type theory with type constructors restricted to Π—is explained as one of the systems forming the so-called lambda cube. Dependent type theory is also the foundational theory of the proof assistant Coq[13].

The first application of dependent type theory to natural language semantics was in[49], where the possibility of providing appropriate meaning representations for the so-called donkey sentences[20] was demonstrated. Subsequently,[1] showed that it is possible to convert meaning representations in DRT (DRSs) into types in dependent type theory.

The full-fledged theory of natural language meaning using dependent types had to await Type-Theoretical Grammar (TTG) by[47]. Here, it was shown that various anaphoric phenomena—including donkey sentences—as well as parts of (semantic) presupposition and linguistic phenomena extending to tense and modality, can be appropriately represented using dependent types, and it is known as a landmark in dependent-type-based semantic theory.

Subsequently, Type Theory with Records (TTR) by[11], and the work on Coercion by[31][32], focused on the possibilities of expansion in dependent type theory beyond anaphora and (semantic) presupposition, broadening the scope of possibilities.

Dependent Type Semantics (DTS)

While TTG gave a dependent-type-theory-based analysis to a wider range of linguistic phenomena than previous work and demonstrated the possibilities of dependent-type-theory-based semantics for natural language, it did not meet the standard as a theory in formal semantics in that it did not satisfy the principle of compositionality. As an attempt to correct this,[42] proposed a fusion of Montague Grammar and TTG, but for problems with this approach, see[5].

Dependent Type Semantics (DTS:[5][8][7]) is a system that reconstructs natural language semantics based on dependent type theory—such as TTG—as a system satisfying the principle of compositionality, by adding a syntactic construction called "underspecified terms" to dependent type theory.

As an example of analysis in DTS, consider the E-type anaphora example: A man entered. He whistled. For the syntactic theory, Combinatory Categorial Grammar[48] is assumed here in order to make the syntactic computation process explicit, but DTS as a semantic component is not dependent on CCG as a syntactic component, and any lexicalized grammar may be assumed.

The syntactic structure and semantic composition process for the first and second sentences are as follows. DTS uses some original notation for dependent types in order to make the meaning representations of natural language easier to read. For details, see[7]. At the bottom, the meaning representations of each sentence appear; these are connected using Σ-types (as conjunctions), yielding the meaning representation of the discourse comprising both sentences.

Here, the @ symbol is used to construct underspecified terms @_iA (where i∈{N} is an index distinguishing different underspecified terms, and A is a type). The rule for underspecified terms is called the @-rule, and gives the meaning: "when A is a type and there exists some proof term of type A, @_iA can be used as a term of type A." Intuitively, this is used as "a term that is A."

To resolve the antecedent of the anaphoric pronoun contained in this meaning representation, type checking is performed. Dependent type theory has a fragment with a decidable type-checking algorithm, and the meaning representations of natural language can be described using that fragment. For details, see[9].

As mentioned at the outset, there are several existing analyses of natural language meaning using dependent type theory, but the distinguishing feature of DTS is that it satisfies the principle of compositionality. By virtue of this feature, DTS can analyze a wide range of linguistic phenomena that have been discussed in formal semantics, in the same way as Montague semantics.

[54] pointed out that anaphora and (semantic) presupposition are phenomena of the same nature and proposed a unified theory based on DRT, and[7] showed that it is possible to develop an analysis that can be called the proof-theoretic counterpart of this. In addition,[6] proposes, for conventional implicature (CI:[45]), an analysis that represents it in the same dimension rather than from the position that distinguishes different dimensions of representation.

Furthermore, the scope of phenomena that DTS can capture extends to linguistic phenomena said to go beyond first-order predicate logic. For example,[51] provides an analysis of generalized quantifiers (GQ:[4]), and[52] provides an analysis of factive presupposition. For the former, an analysis using dependent type theory was proposed in[50], but it notes that problems remain in deriving the strong/weak readings of donkey sentences and discusses a revised proposal. The latter is known to be difficult to analyze within DRT.

Furthermore,[53] discusses the treatment of plurality, specifically the case where a generalized quantifier is the antecedent of a plural anaphor.[28] takes the position of viewing selectional restrictions on predicates as a type of (semantic) presupposition and provides an analysis using DTS.

The Proof-Theoretic Turn in Language Processing

One requirement common to both natural language semantics and semantic processing in natural language processing is to express the meaning conveyed by arbitrary sentences without excess or deficiency, and to accurately extract entailment relations among them. For this, it is necessary to have semantic representations that can accurately express semantic relations such as modality—which specifies relations between propositions or between propositions and the actual world—as well as presupposition, entailment, and tense.

The fact that "a considerable portion of information related to natural language meaning cannot be expressed within the descriptive power of first-order predicate logic" has been argued repeatedly since it was pointed out in early research in Montague semantics. Subsequent formal semantics has developed in a form that extends Montague's intensional logic (IL)—a higher-order logic—and it has become almost standard practice to use higher-order logic.

On the other hand, while Montague's own semantics was presented together with the proof theory of intensional logic (Montague, 1970), in subsequent formal semantics only the model theory was inherited and became dominant. This has tended to make opaque how semantic analyses using formal semantics behave in terms of the aspect of "computation."

At the same time, meaning representations in higher-order logic have hitherto been believed to be "disadvantageous compared to meaning representations in first-order predicate logic" in terms of computation. However, our recent research is revealing that there is room to reconsider this point.

In Mineshima et al. (2015)[36] and Martinez-Gomez et al. (2016)[34], by connecting a robust syntactic analysis based on combinatory categorial grammar (the C&C parser (Clark and Curran 2007)[10]) with a semantics in higher-order logic that provides inference and proof procedures for various semantic phenomena, an entailment recognition system, ccg2lambda, was developed that robustly and efficiently computes semantic analysis for large-scale real-world text. ccg2lambda is publicly available on GitHub: https://github.com/mynlp/ccg2lambda

In ccg2lambda, after obtaining the syntactic parse tree of a natural language sentence, semantic composition in higher-order logic is computed based on lambda calculus, and automated reasoning is performed using the theorem prover Coq. Verification was performed using the FraCaS test suite (Cooper et al. 1994)[17], achieving an accuracy of 69% against Nutcracker—the highest-performing system based on first-order predicate logic at the time in 2015—at 50%. Moreover, while reasoning with higher-order logic had previously been considered inefficient in terms of speed, Mineshima et al. (2015)[36] achieved a speed of 3.72 seconds/question compared to Nutcracker's 11.23 seconds/question, using 80 lexical items for function words, 57 lexical templates for content words, and a set of higher-order axioms (including those for generalized quantifiers and intensionality).

In Mineshima et al. (2016)[38], a system for higher-order-logic-based semantic composition and entailment recognition was similarly constructed for the Japanese CCG parser included with Jigg (Noji and Miyao 2016)[41], and an evaluation of Japanese entailment recognition was performed using the JSeM test suite (Kawazoe et al. 2015)[29]. An accuracy of 75% was achieved at a speed of 3.58 seconds/question for 523 inference tasks involving complex linguistic phenomena such as generalized quantifiers. The performance of ccg2lambda—both for English and Japanese—thus matches the state-of-the-art in entailment recognition.

Furthermore, in Martinez-Gomez et al. (2017)[37], a technique was proposed for dynamically generating axioms using WordNet and word2vec when lexical knowledge is needed during ccg2lambda's reasoning. An evaluation experiment for the entailment recognition task was conducted using the SICK dataset (Marelli et al. 2014)[33], constructed for evaluating the compositional semantics of distributed representations, and an accuracy of 83%—exceeding the performance of conventional systems based on first-order predicate logic or natural logic—was achieved.

These studies show that higher-order logic can be advantageous not only in terms of description but also in terms of speed in the computation of entailment recognition for natural language, casting new light on the question of what form of representation is appropriate for semantic processing. For example, they suggest that meaning representations in higher-order logic provide a well-behaved "compression" of the information in natural language meaning that requires descriptive power beyond first-order predicate logic (typically involving generalized quantifiers and modality). That is, by assigning short computational processes to the inference processes that this information frequently requires, efficient computation is possible compared to meaning representations written out in first-order predicate logic, which are verbose and require more powerful computational resources.

(Originally published: Bekki, Mineshima, Kaneko, Tanaka, Tanaka [Hitomi], Kinoshita, Ito, Yanagi (2017) "The Proof-Theoretic Turn in Semantics," Proceedings of the 31st Annual Conference of the Japanese Society for Artificial Intelligence, 2B3-OS-07a-4.)

1. Ahn, René and Kolb, Hans-Peter (1990). Discourse Representation meets Constructive Mathematics. Papers from the Second Symposium on Logic and Language.
2. Asher, Nicholas and Lascarides, Alex (2003). Logics of Conversation. Cambridge University Press.
3. Barendregt, Henk P. (1992). Lambda Calculi with Types. Handbook of Logic in Computer Science.
4. Barwise, Jon and Cooper, Robin (1981). Generalized Quantifiers and Natural Language. Linguistics and Philosophy.
5. Bekki, Daisuke (2014). Representing Anaphora with Dependent Types. Logical Aspects of Computational Linguistics (LACL 2014), LNCS 8535.
6. Bekki, Daisuke and McCready, Eric (2015). CI via DTS. New Frontiers in Artificial Intelligence (JSAI-isAI 2014 Workshops).
7. Bekki, Daisuke and Mineshima, Koji (2017). Context-Passing and Underspecification in Dependent Type Semantics. Modern Perspectives in Type-Theoretical Semantics.
8. Bekki, Daisuke and Mineshima, Koji (2016). Dependent Type Semantics: An Introduction. ESSLLI 2016 Lecture Notes.
9. Bekki, Daisuke and Sato, Miho (2015). Calculating Projections via Type Checking. TYpe Theory and LExical Semantics (TYTLES), ESSLLI 2015 Workshop.
10. Clark, Stephen and Curran, James R. (2007). Wide-coverage efficient statistical parsing with CCG and log-linear models. Computational Linguistics.
11. Cooper, Robin (2005). Records and Record Types in Semantic Theory. Journal of Logic and Computation.
12. Copestake, Ann and Flickinger, Dan and Pollard, Carl J. and Sag, Ivan A. (2006). Minimal Recursion Semantics: An Introduction. Research on Language and Computation.
13. Coquand, Thierry and Huet, Gérard (1988). The Calculus of Constructions. Information and Computation.
14. Dummett, Michael (1975). What is a Theory of Meaning?. Mind and Language.
15. Dummett, Michael (1976). What is a Theory of Meaning? (II). Truth and Meaning.
16. Evans, Gareth (1980). Pronouns. Linguistic Inquiry.
17. Cooper, R. et al. (1994). FraCaS: A Framework for Computational Semantics. FraCaS Technical Report.
18. Francez, Nissim and Dyckhoff, Roy (2010). Proof-theoretic semantics for a natural language fragment. Linguistics and Philosophy.
19. Francez, Nissim (2015). Proof-Theoretic Semantics. College Publications.
20. Geach, Peter (1962). Reference and Generality. Cornell University Press.
21. Gentzen, Gerhard (1935). Untersuchungen über das logische Schliessen I, II. Mathematische Zeitschrift.
22. Groenendijk, Jeroen and Stokhof, Martin (1991). Dynamic Predicate Logic. Linguistics and Philosophy.
23. Grudzińska, Justyna and Zawadowski, Marek (2014). System with Generalized Quantifiers on Dependent Types for Anaphora. EACL 2014 Workshop on Type Theory and Natural Language Semantics (TTNLS).
24. Heim, Irene (1983). File Change Semantics and the Familiarity Theory of Definiteness. Meaning, Use and the Interpretation of Language.
25. Heim, Irene (1983). On the Projection Problem for Presuppositions. West Coast Conference on Formal Linguistics II.
26. Heim, Irene and Kratzer, Angelika (1998). Semantics in Generative Grammar. Blackwell Publishers.
27. Kamp, Hans (1981). A Theory of Truth and Semantic Representation. Formal Methods in the Study of Language.
28. Kinoshita, Eriko and Mineshima, Koji and Bekki, Daisuke (2017). An Analysis of Selectional Restrictions with Dependent Type Semantics. New Frontiers in Artificial Intelligence. JSAI-isAI 2016, LNCS vol. 10247.
29. Kawazoe, Ai and Tanaka, Ribeka and Mineshima, Koji and Bekki, Daisuke (2015). An Inference Problem Set for Evaluating Semantic Theories and Semantic Processing Systems for Japanese. LENLS 12.
30. Lappin, Shalom (ed.) (1996). The Handbook of Contemporary Semantic Theory. Blackwell.
31. Luo, Zhaohui (2010). Type-theoretical semantics with coercive subtyping. Semantics and Linguistic Theory 20 (SALT 20).
32. Luo, Zhaohui (2012). Formal Semantics in Modern Type Theories with Coercive Subtyping. Linguistics and Philosophy.
33. Marelli, M. and Menini, S. and Baroni, M. and Bentivogli, L. and Bernardi, R. and Zamparelli, R. (2014). A SICK Cure for the Evaluation of Compositional Distributional Semantic Models. LREC 2014.
34. Martínez Gómez, Pascual and Mineshima, Koji and Miyao, Yusuke and Bekki, Daisuke (2016). ccg2lambda: A Computational Semantics System. ACL 2016 System Demonstrations.
35. Martin-Löf, Per (1984). Intuitionistic Type Theory. Bibliopolis.
36. Mineshima, Koji and Martínez Gómez, Pascual and Miyao, Yusuke and Bekki, Daisuke (2015). Higher-order logical inference with compositional semantics. EMNLP 2015.
37. Martinez-Gomez, Pascual and Mineshima, Koji and Miyao, Yusuke and Bekki, Daisuke (2017). Injection of Lexical Knowledge for Recognising Textual Entailment. EACL 2017.
38. Mineshima, Koji and Tanaka, Ribeka and Martinez-Gomez, Pascual and Miyao, Yusuke and Bekki, Daisuke (2016). Building compositional semantics and higher-order inference system for a wide-coverage Japanese CCG parser. EMNLP 2016.
39. Montague, Richard (1974). Formal Philosophy. Yale University Press.
40. Nordström, Bengt and Petersson, Kent and Smith, Jan (1990). Programming in Martin-Löf's Type Theory. Oxford University Press.
41. Noji, Hiroshi and Miyao, Yusuke (2016). Jigg: A Framework for an Easy Natural Language Processing Pipeline. ACL 2016 System Demonstrations.
42. Dávila-Pérez, Rogelio (1995). Semantics and Parsing in Intuitionistic Categorial Grammar. PhD thesis, University of Essex.
43. Popper, Karl Raimund (1934). The Logic of Scientific Discovery. Routledge.
44. Portner, Paul and Partee, Barbara H. (eds.) (2002). Formal Semantics: The Essential Readings. Blackwell.
45. Potts, Christopher (2005). The Logic of Conventional Implicatures. Oxford University Press.
46. Prawitz, Dag (1965). Natural Deduction: A Proof-Theoretic Study. Dover Publications.
47. Ranta, Aarne (1994). Type-Theoretical Grammar. Oxford University Press.
48. Steedman, Mark (1996). Surface Structure and Interpretation. The MIT Press.
49. Sundholm, Göran (1986). Proof Theory and Meaning. Handbook of Philosophical Logic.
50. Sundholm, Göran (1989). Constructive Generalized Quantifiers. Synthese.
51. Tanaka, Ribeka (2014). A Proof-Theoretic Approach to Generalized Quantifiers in Dependent Type Semantics. ESSLLI 2014 Student Session.
52. Tanaka, Ribeka and Mineshima, Koji and Bekki, Daisuke (2015). Factivity and Presupposition in Dependent Type Semantics. TYpe Theory and LExical Semantics (TYTLES), ESSLLI 2015 Workshop.
53. Tanaka, Ribeka and Mineshima, Koji and Bekki, Daisuke (2017). On the Interpretation of Dependent Plural Anaphora in a Dependently-Typed Setting. New Frontiers in Artificial Intelligence. JSAI-isAI 2016, LNCS vol. 10247.
54. van der Sandt, Rob (1992). Presupposition Projection as Anaphora Resolution. Journal of Semantics.