Abstract: It's not accidental that the editors of two of the foundational international standards for the World Wide Web are a philologist with an interest in formal language theory and a computational linguist. In this talk I'll present a linguist's introduction to XML, and explore some areas where the XML standards depend on fundamental insights from formal language theory, grammatical theory and formal logic.

The complete talk is available here.

Abstract: Formal compositional semantics is generally thought to depend on deep syntactic processing and on a detailed lexicon that includes information about subcategorization. This has led to semantics being ignored in much recent computational linguistic work that concentrates on robust, broad-coverage techniques. I will argue that even very shallow processing can be treated as manipulating logical forms, if a representation language is used which allows extreme underspecification. Thinking of shallow processing in this way allows for the development of a general framework for integrating shallow and deep language processing.

E.W. Beth dissertation award: 2003 winner

The selection for the E.W. Beth Dissertation Prize for the year 2003 has been concluded. The quality of submissions was very high and the competition intense. After careful deliberation the committee has reached the following decision:

The E.W. Beth Dissertation Prize 2003 has been awarded to JASON BALDRIDGE (University of Edinburgh) for the dissertation ``Lexically Specified Derivational Control in Combinatory Categorial Grammar''.

The abstract can be found at: http://www.cs.nott.ac.uk/~nza/beth02

FoLLI would like to congratulate the winner for his excellent thesis, and to thank all applicants who responded to the call for submissions and the members of the E.W. Beth Dissertation Prize Committee (Anne Abeille, Natasha Alechina (chair), Patrick Blackburn, Nissim Francez, Valentin Goranko, Larry Moss, Francesco Orilia, Gerald Penn, Manfred Pinkal, Christian Retore, Rob van der Sandt and Henriette de Swart) for doing a great job.

An award ceremony will take place during ESSLLI 03 in Vienna, on Monday, August 25 at 20:00 hrs.

Finally, our thanks go to the E.W. Beth Foundation which kindly sponsors the prize.

On behalf of FoLLI, Raffaella Bernardi

Abstract: If we want computers to cope with semantic content, we need computational tools which build sensible representations, infer new information from old, detect inconsistencies, and so on. How realistic is this goal?

Closer than it was even five years ago. Nowadays a wide range of automated reasoning tools (such as theorem provers and model builders) are available over the internet, and this opens up the possibility of combining semantic construction with efficient reasoning.

In this talk I'm going to discuss the goals of computational semantics, and explain why recent advances in automated reasoning are important to its development.

This talk is based on joint work with Johan Bos. For further information (and in particular, to find out about the CURT programs, which I will be discussing) see www.comsem.org.

Abstract: We will speak about three traditions in Logic:

• Classical, usually associated with Frege, Hilbert, Gödel, Tarski, and others;
• Intuitionistic, founded by Brouwer, Heyting, Kolmogorov, Gödel, Kleene, and others;
• Explicit, which we trace back to Skolem, Curry, Gödel, Church, and others.

The classical tradition in logic based on quantifiers $\forall$ and $\exists$ essentially reflected the 19th century mathematician's way of representing dependencies between entities. A sentence $\forall x\exists y A(x,y)$, though specifying a certain relation between $x$ and $y$, did not mean that the latter is a function of the former, let alone a computable one.

The Intuitionistic approach provided a principal shift toward the effective functional reading of the mathematician's quantifiers. A new, nonTarskian semantics had been suggested by Kleene: realizability that revealed a computational content of logical derivations. In a decent intuitionstic system, a proof of $\forall x\exists y A(x,y)$ yields a program $f$ that computes $y=f(x)$. \par

Explicit tradition makes the ultimate step by using representative systems of functions instead of quantifiers from the very beginning. Since the work of Skolem, 1920, it has been known that the classical logic can be adequately recast in this way. Church in 1936 showed that even the very basic system of function definition and function application is capable of emulating any computable procedure. However, despite this impressive start, the explicit tradition remained a Cinderella of the mathematical logic for decades. Now things have changed: due to its very explicitness, this third tradition became the one most closely connected with Computer Science.

In this talk we will show how switching from quantifiers to explicit functional language helps problem solving in both theoretical logic and its applications. A discovery of a natural system of self-referential proof terms, {\em proof polynomials}, was essential in the solution to an open problem of G\"odel concerning formalization of provability. Proof polynomials considerably extend the Curry-Howard isomorphism and lead to a joint calculus of propositions and proofs which unifies several previously unrelated areas. It changes our conception of the appropriate syntax and semantics for reasoning about knowledge, functional programming languages, formalized deduction and verification.

Abstract: Renyi and Ulam asked what is the minimum number q of yes-no questions needed to find an unknown number x in a search space S of cardinality 2^m, if up to E of the answers may be wrong/false. This is an important problem in Berlekamp's theory of noisy communication with noiseless feedback. If all questions are asked at the outset, before knowing any answer, then strategies with q questions correspond to optimal E error correcting codes. This is the nonadaptive version of the Renyi-Ulam game of Twenty Questions with lies. The sphere packing bound fixes an insurmountable lower bound q* for q, and the question is whether a clever searching strategy can find the unknown x with exactly q* questions. Negative results are pervasive in the literature, already for E=2. Remarkably enough, positive results are obtained if one allows a minimum amount of adaptiveness, in the following sense: the unknown x can be infallibly discovered by first asking a nonadaptive batch of m questions, precisely as in the game without lies, and then, only depending on these answers, a second batch of q*-m nonadaptive questions. We shall present the necessary tools for this result, along with the logical aspects of the game: it turns out that (E+2)-valued logic naturally expresses our states of knowledge (as given by the conjunction of the answers) and their natural order.