ABSTRACT. The main stream in machine translation is to build systems that are able to translate everything, but without any guarantees of quality. An alternative to this is systems that aim at precision but have limited coverage. Combining wide coverage with high precision is considered unrealistic. Most wide-coverage systems are based on statistics, whereas precision-oriented domain-specific systems are typically based on grammars, which guarantee translation equality by some kind of formal semantics.

This talk introduces a technique that combines wide coverage with high precision, by embedding a high-precision semantic grammar inside a wide-coverage syntactic grammar, which in turn is backed up by a chunking grammar. The system can thus reach good quality whenever the input matches the semantics; but if it doesn't, the user will still get a rough translation. The levels of confidence can be indicated by using colours, whence the title of the talk.

The talk will explain the main ideas in this technique, based on GF (Grammatical Framework) and also inspired by statistical methods (probabilistic grammars) and the Apertium system (chunk-based translation), boosted by freely available dictionaries (WordNet, Wiktionary), and built by a community of over 50 active developers. The current system covers 11 languages and is available both as a web service and as an Android application.

Demo system: http://www.grammaticalframework.org/demos/translation.html

ABSTRACT. Transfer semantics uses a rewriting (or transfer) system to map syntactic parses onto semantic representations [4, 5]. This form of semantic mapping was used to build broad coverage semantic text indexes at Powerset, and has been used in various other settings such as question answering for intelligence analysts and medical QA. It has been used for English, German [14] and Japanese [13]. However, in all these cases the transfer semantics has been applied to the output of just one kind of parser: LFG functional structures created by the XLE parser [6]. This paper describes the adaptation of transfer semantics to apply to the output of the Clear dependency parser [2].

ABSTRACT. In this contribution, we start form a concrete problem: the identification of argument compounds and show how their structure can be modelled on a linguistic and logical basis. This investigation is, in a first stage, restricted to arguments found in technical texts. Then, we propose a type-based syntactic analysis and the premises of a conceptual model that accounts for the logical properties of such compounds. An implementation in Dislog is presented with an indicative evaluation of the results. Dislog runs on TextCoop which is a logic-based platform we developed for discourse analysis.

ABSTRACT. We show how one can formalise quantifiers in the categorical compositional distributional model of meaning. Our model is based on the generalised quantifier theory of Barwise and Cooper. We develop an abstract compact closed semantics and instantiate it in vector spaces and in relations. The former is an example for the distributional corpus-based models of language and the latter for the truth-theoretic ones.

ABSTRACT. This work is part of a project which goal is to understand natural language by taking dialogue as a primitive notion. For this aim, the core of our theoretical framework is a logical theory of interaction, namely Ludics. Ludics is a logical theory developed by J.Y. Girard as an achievement of both proof theoretical and computational theoretical considerations. Above all it is a theory of interaction in the sense that interaction is ontologically the primitive element of Ludics. Ludics being a logical theory, our framework is relevant for grasping logical dimensions of language, especially for studying argumentation but also divergences in dialogue as we show in this paper. In particular complementary aspects of argumentation and divergence in dialogues are modelled in a uniform way: from logics and pragmatics to semantics and syntax. Furthermore we account for several features of dialogues directly at the formal level. Therefore, we may expect a fine-grained representation of various dialogical phenomenas. More precisely we illustrate this last point by describing how different divergences in dialogue may be distinguished in our modelling.

ABSTRACT. The specialized language of mathematics has a number of linguistically and logically interesting features. One of them, which to our knowledge has not been systematically studied before, is the implicit dynamic introduction of function symbols, exemplified by constructs of the form "for every x there is an f(x) such that ...". We present an extension of Groenendijk and Stokhof's Dynamic Predicate Logic -- Typed Higher-Order Dynamic Predicate Logic -- which formally models this feature of the language of mathematics. Furthermore, we illustrate how the implicit dynamic introduction of function symbols is treated in the proof checking algorithm of the Naproche system.

ABSTRACT. This paper outlines a proof-theoretic approach to developing correct and terminating monadic parsers. Using a modified realisability interpretation, we extract provably correct and terminating programs from formal proofs. If the proof system is proven to be correct, then any extracted program is guaranteed to be so. By extracting parsers, we can ensure that they are correct, complete and terminating for any input. The work is ongoing, and is being carried out in the interactive proof system M\textsc{inlog}.

ABSTRACT. We modify Buszkowski's translation of context-free grammars to Lambek categorial grammars in order to deal with Montague-style semantics properly.