Structural proof theory is a branch of logic that studies the general structure and properties of logical and mathematical proofs. This book is both a concise introduction to the central results and methods of structural proof theory, and a work of research that will be of interest to specialists. The book is designed to be used by students of philosophy, mathematics and computer science. The book contains a wealth of results on proof-theoretical systems, including extensions of such systems from logic (...) to mathematics, and on the connection between the two main forms of structural proof theory - natural deduction and sequent calculus. The authors emphasize the computational content of logical results. A special feature of the volume is a computerized system for developing proofs interactively, downloadable from the web and regularly updated. (shrink)

It is the aim of INDICES to document recent explorations in the various fields of philosophical logic and formal linguistics and their applications in other disciplines. The main emphasis of this series is on self-contained monographs covering particular areas of recent research and surveys of methods, problems, and results in all fields of inquiry where recourse to logical analysis and logical methods has been fruitful. INDICES will contain monographs dealing with the central areas of philosophical logic (extensional and intensional systems, (...) indexical logics, non-classical logics, philosophy of logic, etc.) as well as studies in which these systems are applied to specific issues in philosophy, in the formal semantics of natural languages, the foundations of linguistic theory, in computational linguistics, and in theoretical computer science. Constructive type theory was first presented in 1970, by the Swedish logician Per Martin-Lof. It has become one of the main approaches used in the foundations of mathematics and computer science. But it has remained relatively unknown among linguists and philosophers, although it provides a considerable extension of the concepts and techniques of logic. The book first gives an introduction to type theory from the point of view of linguistics and the philosophy of language. Type theory is then applied in the areas of quantification, anaphora, temporal reference, and the structure of text and discourse. By virtue of the type-theoretical concepts of proof object and context, various phenomena of dependence and progression in language can be discussed in precise terms, and several well-known problems can be solved. A categorial grammar is presented togenerate formally a fragment of English, together with an example of a computer implementation. (shrink)

Without violating the spirit of Game-Theoretical semantics, its results can be re-worked in Martin-Löf''s Constructive Type Theory by interpreting games as types of Myself''s winning strategies. The philosophical ideas behind Game-Theoretical Semantics in fact highly recommend restricting strategies to effective ones, which is the only controversial step in our interpretation. What is gained, then, is a direct connection between linguistic semantics and computer programming.

We propose a shift in perspective from the view of natural languages as formal languages to natural languages as a collection of resources for constructing local languages for use in particular situations. This is suggested by our experience constructing natural language grammars for particular applications using the Grammatical Framework. It points to a research programme investigating how such resources play a role in linguistic innovation by agents constructing situation-specific local languages and how they can be made dynamic, modified by the (...) linguistic agent’s exposure to innovative linguistic data. (shrink)

The paper takes a look at the history of the idea of universal grammar and compares it with multilingual grammars, as formalized in the Grammatical Framework, GF. The constructivist idea of formalizing math- ematics piece by piece, in a weak logical framework, rather than trying to reduce everything to one single strong theory, is the model that guides the development of grammars in GF.

The paper takes a look at the history of the idea of universal grammar and compares it with multilingual grammars, as formalized in the Grammatical Framework, GF. The constructivist idea of formalizing math­ematics piece by piece, in a weak logical framework, rather than trying to reduce everything to one single strong theory, is the model that guides the development of grammars in GF.

This paper shows how a dialogue system for information-seekingdialogues can be implemented in a type-theory-based syntax editor,originally developed for editing mathematical proofs.The implementation gives a simple logical metatheory tosuch dialogue systems and also suggests new functions forthem, e.g., a local undo operation. The method developed provides alogically based declarative way of implementing simple dialoguesystems that is easy to port to new domains.

The aim of this study is to look at the the syntactic calculus of Bar-Hillel and Lambek, including semantic interpretation, from the point of view of constructive type theory. The syntactic calculus is given a formalization that makes it possible to implement it in a type-theoretical proof editor. Such an implementation combines formal syntax and formal semantics, and makes the type-theoretical tools of automatic and interactive reasoning available in grammar.In the formalization, the use of the dependent types of constructive type (...) theory is essential. Dependent types are already needed in the semantics of ordinary Lambek calculus. But they also suggest some natural extensions of the calculus, which are applied to the treatment of morphosyntactic dependencies and to an analysis of selectional restrictions. Finally, directed dependent function types are introduced, corresponding to the types of constructive type theory. (shrink)

In this paper, we shall present a generalization of phrase structure grammar, in which all functional categories have type restrictions, that is, their argument types are specific domains. In ordinary phrase structure grammar, there is just one universal domain of individuals. The grammar does not make a distinction between verbs and adjectives in terms of domains of applicability. Consequently, it fails to distinguish between sentences like every line intersects every line, which is well typed, and every line intersects every point, (...) which is ill typed.Our generalization relates to ordinary phrase structure grammar in the same way as the higherlevel constructive type theory of Martin-Löf relates to the simple type theory of Church . Simple type theory has been used in linguistics and related with phrase structure grammar, especially in the tradition based on the work of Montague .Our definition of the grammar will be more formal than Montague's in the sense that we shall use a formal metalanguage, that of constructive type theory, for defining both the object language and its interpretation. The grammar, both syntax and semantics, is thus readily implementable in the type-theoretical proof system ALF . Inside type theory, a distinction can be made between the object language and the model, in other words, between syntactic and semantic types. It will turn out that the object language cannot be defined independently of the model, as in ordinary Tarski semantics. This is a direct consequence of introducing the typing restrictions.The grammar presented here can be seen as a formal linguistic elaboration of the work presented in Ranta 1991 and 1994. The organization of generative grammar as categorial grammar followed by sugaring should now look more familiar to the linguist, as the grammatical formalism on which sugaring operates is no longer full type theory but a set of phrase structure trees. (shrink)

Portable Grammar Format (PGF) is a core language for type-theoretical grammars. It is the target language to which grammars written in the high-level formalism Grammatical Framework (GF) are compiled. Low-level and simple, PGF is easy to reason about, so that its language-theoretic properties can be established. It is also easy to write interpreters that perform parsing and generation with PGF grammars, and compilers converting PGF to other formats. This paper gives a concise description of PGF, covering syntax, semantics, and parser (...) generation. It also discusses the technique of embedded grammars, where language processing tasks defined by PGF grammars are integrated in larger systems. (shrink)