The Ajdukiewicz Calculus, Polish Notation and Hilbert-Style Proofs

Abstract

Current research programs in the logic of language and computational linguistics employ certain methods characteristic of logical proof theory, a branch of logic devoted to fine structures of proofs. For instance, formal semantics of natural language applies the Curry-Howard correspondence between natural deduction proofs and typed lambda-terms to describe the process of computing semantic representations of expressions. Cut-free systems in the Gentzen form are used in standard axiomatizations of logical calculi of categorial grammar, closely related to substructural logics. Cut elimination and interpolation theorems play a significant part in some proofs of equivalence theorems for different kinds of formal grammar and in some proofs of completeness theorems for substructural logics. Proofs by resolution and unification, known from logic programming, are also a basic technique of unification systems in computational linguistics, as e.g. Definite Clause Grammars and Categorial Unification Grammars. Unification can also be used in learning algorithms for categorial grammars; see (1990), (1994), (1994) and (1997). A thorough account of interrelations between mathematical linguistics and proof theory can be found in (1997) (also see van Benthem, 1991).