Dissemination of Logic in 1999

Our efforts to promote a florishing logic education remain closely linked to the pursuit of research goals which are carried by a national research community. Using active research in logic as a permanent source of inspiration we aim to disseminate the living essence of the subject.

Logic and Language Analysis

Important themes in the analysis of natural language analysis are concerned with the dynamics of interpretation and of inference processes. Rule systems that pay due attention to these themes may involve considerable departures from standard rule systems, since they, for instance, may lack the property of monotonicity. If one adds a premise to a given premises list, one runs the risk of destroying argumentative patterns, and may no longer be able to derive conclusions that were derivable before. Developing sound and complete calculi for dynamic anaphora logics, a calculus for `variable free' incremental semantics emerged which proved to be a suitable basis for a new version of Montague grammar. The findings were incorporated in a course on Computational Semantics that bridges the gap between natural language and programming language semantics, thus demonstrating the continuum of imperative and functional programming and natural language understanding.

Logic and Programming

In dynamic variations on predicate logic formulas are interpreted as actions with a suggestion of execution processes. However, formulas of `dynamic' predicate logic are not suited for execution on a computer as they stand, for particular actions (existential quantification) tend to lead to infinities of possibilities that would embarrass even the most powerful computer.

By an ingenious computational reinterpretation, dynamic predicate logic may figure as the basis of a programming language after all. A language Dynamo has been developed that implements an executable process interpretation of dynamic predicate logic, with constructs for bounded iteration and bounded choice. Dynamo owes its inspiration and computational thrust to Alma, a language developed by Krzysztof Apt and his co-workers, and it forges a link between the Amsterdam research traditions in dynamic and computational logic. Further work includes an improved execution mechanism, where tests that cannot be performed immediately are stored to be resolved at a later stage. Heguiabehere is implementing the resulting system with constraint handling. Further information can be found at http://www.cwi.nl/~jve/dynamo.

Logic and programming are also brought together in courseware developed in the area of reasoning and imperative programming. The undergraduate course material prepared by Van Benthem, Van Eijck, Jaspars and Kaldewaij forms the starting point for the preparation of a series of booklets with internet software for use in secondary schools. Amsterdam University Press and CWI are involved in the plans.

Logic and Games

Marc Pauly established further connections between game logic, a generalization of propositional dynamic logic, and modal logic. As propositional dynamic logic was first invented to reason about indeterministic imperative programs, the study of game logic constitutes a link between programming semantics and game analysis. Tools are developed for the graphical display of evaluation games for dynamic logic formulas in Kripke models. Furthermore, progress has been made with axiomatization, decidability and expressiveness and we are presently working on an implementation of Parikh's games and on a logic for coalition games.

A joint initiative with the Logic in Communication group was the formation of a reading group on Game Theory and the organization of a two day workshop Logic and Games. The workshop provided a platform for the presentation of recent work in this area and attracted researchers from various countries and from a wide variety of disciplines (mathematics, linguistics, economics, philosophy, social sciences).

Structuring Information Flow in Electronic Handbooks

A concrete application of theoretical ideas on information structuring is the analysis and prototyping of an electronic environment for scientific handbook information, with Van Benthem and Ter Meulen (eds.), Handbook of Logic and Language, Elsevier 1997, as the concrete focus. This joint project with Elsevier Science BV aims at designing formats for electronic dissemination of knowledge as traditionally found in scientific handbooks. Jon Ragetli has started working on this LoLaLi project as a Ph.D. student in September 1999.

Implementation of Tools and Animation Programs

Innovation in logic education is pursued by means of implementations illustrating abstract definitions. Theoretical points with a boring flavour get a vivid appeal when they are illustrated by appropriate animations. Abstract definitions of reduction strategies in lambda calculus are conveniently demonstrated by means of procedures that actually perform these reductions and by means of working implementations of language fragments semantic programming come to life. For purposes of course rejuvenation, the toy imperative programming languages from the semantics textbooks have been implemented in Haskell (a state-of-the-art functional programming language eminently suited for fast prototyping): WHILE (imperative programs without procedures) and PROC (imperative programs with procedures, with static and dynamic procedure calling mechanisms, and static and dynamic binding of local variable declarations).

Visualization is a key method in communicating logic in an electronic environment, as can be seen from the success of Tarski's World and Turing's World, developed by Barwise and Etchemendy and their team from Stanford University. In a similar vein, the Logic in Action group developed calculators and animations for use in several elementary logic courses, freely distributed over the internet. A sample of such web-applications can be found at http://www.wins.uva.nl/~jaspars/animations/.