Bücher der Reihe Nato ASI Subseries F:

Recent developments in computer science clearly show the need for a better theoretical foundation for some central issues. Methods and results from mathematical logic, in particular proof theory and model theory, are of great help here and will be used much more in future than previously. This book provides an excellent introduction to the interplay of mathematical logic and computer science. It contains extensively reworked versions of the lectures given at the 1997 Marktoberdorf Summer School by leading researchers in the field.Topics covered include: proof theory and specification of computation (J.-Y. Girard, D. Miller), complexity of proofs and programs (S. R. Buss, S. S. Wainer), computational content of proofs (H. Schwichtenberg), constructive type theory (P. Aczel, H. Barendregt, R. L. Constable), computational mathematics, (U. Martin), rewriting logic (J. Meseguer), and game semantics (S. Abramski).

Soft computing is a consortium of computing methodologies that provide a foundation for the conception, design, and deployment of intelligent systems and aims to formalize the human ability to make rational decisions in an environment of uncertainty and imprecision. This book is based on a NATO Advanced Study Institute held in 1996 on soft computing and its applications. The distinguished contributors consider the principal constituents of soft computing, namely fuzzy logic, neurocomputing, genetic computing, and probabilistic reasoning, the relations between them, and their fusion in industrial applications. Two areas emphasized in the book are how to achieve a synergistic combination of the main constituents of soft computing and how the combination can be used to achieve a high Machine Intelligence Quotient.

For some years, specification of software and hardwaresystems has been influenced not only by algebraic methodsbut also by new developments in logic. These newdevelopments in logic are partly based on the use ofalgorithmic techniques in deduction and proving methods, butare alsodue to new theoretical advances, to a great extentstimulated by computer science, which have led to new typesof logic and new logical calculi. The new techniques,methods and tools from logic, combined with algebra-basedones, offer very powerful and useful tools for the computerscientist, which may soon become practical for commercialuse, where, in particular, more powerful specification toolsare needed for concurrent and distributed systems. This volume contains papers based on lectures by leadingresearchers which were originally given at an internationalsummer school held in Marktoberdorf in 1991. The papers aimto give a foundation for combining logic and algebra for thepurposes of specification under the aspects of automateddeduction, proving techniques, concurrency and logic,abstract data types and operational semantics, andconstructive methods.

The understanding of parallel processing and of the mechanisms underlying neural networks in the brain is certainly one of the most challenging problems of contemporary science. During the last decades significant progress has been made by the combination of different techniques, which have elucidated properties at a cellular and molecular level. However, in order to make significant progress in this field, it is necessary to gather more direct experimental data on the parallel processing occurring in the nervous system. Indeed the nervous system overcomes the limitations of its elementary components by employing a massive degree of parallelism, through the extremely rich set of synaptic interconnections between neurons. This book gathers a selection of the contributions presented during the NATO ASI School "e;Neuronal Circuits and Networks"e; held at the Ettore Majorana Center in Erice, Sicily, from June 15 to 27, 1997. The purpose of the School was to present an overview of recent results on single cell properties, the dynamics of neuronal networks and modelling of the nervous system. The School and the present book propose an interdisciplinary approach of experimental and theoretical aspects of brain functions combining different techniques and methodologies.

The idea for this workshop originated when I came across and read Martin Zelkowitz's book on Requirements for Software Engineering Environments (the proceedings of a small workshop held at the University of Maryland in 1986). Although stimulated by the book I was also disappointed in that it didn't adequately address two important questions - "e;Whose requirements are these?"e; and "e;Will the environment which meets all these requirements be usable by software engineers?"e;. And thus was the decision made to organise this workshop which would explicitly address these two questions. As time went by setting things up, it became clear that our workshop would happen more than five years after the Maryland workshop and thus, at the same time as addressing the two questions above, this workshop would attempt to update the Zelkowitz approach. Hence the workshop acquired two halves, one dominated by discussion of what we already know about usability problems in software engineering and the other by discussion of existing solutions (technical and otherwise) to these problems. This scheme also provided a good format for bringing together those in the HeI community concerned with the human factors of software engineering and those building tools to solve acknowledged, but rarely understood problems.

This book is the result of a NATO sponsored workshop entitled "e;Student Modelling: The Key to Individualized Knowledge-Based Instruction"e; which was held May 4-8, 1991 at Ste. Adele, Quebec, Canada. The workshop was co-directed by Gordon McCalla and Jim Greer of the ARIES Laboratory at the University of Saskatchewan. The workshop focused on the problem of student modelling in intelligent tutoring systems. An intelligent tutoring system (ITS) is a computer program that is aimed at providing knowledgeable, individualized instruction in a one-on-one interaction with a learner. In order to individualize this interaction, the ITS must keep track of many aspects of the leamer: how much and what he or she has leamed to date; what leaming styles seem to be successful for the student and what seem to be less successful; what deeper mental models the student may have; motivational and affective dimensions impacting the leamer; and so ono Student modelling is the problem of keeping track of alI of these aspects of a leamer's leaming.

The chapters of this book summarize the lectures delivered du ring the NATO Advanced Study Institute (ASI) on Computational Methods in Mechanisms, that took place in the Sts. Constantin and Elena Resort, near Varna, on the Bulgarian Coast of the Black Sea, June 16-28, 1997. The purpose of the ASI was to bring together leading researchers in the area of mechanical systems at large, with special emphasis in the computational issues around their analysis, synthesis, and optimization, during two weeks of lectures and discussion. A total of 89 participants from 23 count ries played an active role during the lectures and sessions of contributed papers. Many of the latter are being currently reviewed for publication in specialized journals. The subject of the book is mechanical systems, Le. , systems composed of rigid and flexible bodies, coupled by mechanical means so as to constrain their various bodies in a goal-oriented manner, usually driven under computer con- trol. Applications of the discipline are thus of the most varied nature, ranging from transportation systems to biomedical devices. U nder normal operation conditions, the constitutive bodies of a mechanical system can be consid- ered to be rigid, the rigidity property then easing dramatically the analysis of the kinematics and dynamics of the system at hand. Examples of these systems are the suspension of a terrestrial vehicle negotiating a curve at speeds within the allowed or recommended limits and the links of multiaxis industrial robots performing conventional pick-and-place operations.

This book is one outcome of the NATO Advanced Studies Institute (ASI) Workshop, "e;Speechreading by Man and Machine,"e; held at the Chateau de Bonas, Castera-Verduzan (near Auch, France) from August 28 to Septem- ber 8, 1995 - the first interdisciplinary meeting devoted the subject of speechreading ("e;lipreading"e;). The forty-five attendees from twelve countries covered the gamut of speechreading research, from brain scans of humans processing bi-modal stimuli, to psychophysical experiments and illusions, to statistics of comprehension by the normal and deaf communities, to models of human perception, to computer vision and learning algorithms and hardware for automated speechreading machines. The first week focussed on speechreading by humans, the second week by machines, a general organization that is preserved in this volume. After the in- evitable difficulties in clarifying language and terminology across disciplines as diverse as human neurophysiology, audiology, psychology, electrical en- gineering, mathematics, and computer science, the participants engaged in lively discussion and debate. We think it is fair to say that there was an atmosphere of excitement and optimism for a field that is both fascinating and potentially lucrative. Of the many general results that can be taken from the workshop, two of the key ones are these: * The ways in which humans employ visual image for speech recogni- tion are manifold and complex, and depend upon the talker-perceiver pair, severity and age of onset of any hearing loss, whether the topic of conversation is known or unknown, the level of noise, and so forth.

Despite its increasing importance, the verification andvalidation of the human-machine interface is perhaps themost overlooked aspect of system development. Although muchhas been written about the design and developmentprocess,very little organized information is available on how toverifyand validate highly complex and highly coupleddynamic systems. Inability toevaluate such systemsadequately may become the limiting factor in our ability toemploy systems that our technology and knowledge allow us todesign.This volume, based on a NATO Advanced Science Institute heldin 1992, is designed to provide guidance for theverification and validation of all highly complex andcoupled systems. Air traffic control isused an an exampleto ensure that the theory is described in terms that willallow its implementation, but the results can be applied toall complex and coupled systems.The volume presents the knowledge and theory ina formatthat will allow readers from a wide variety of backgroundsto apply it to the systems for which they are responsible.The emphasis is on domains where significant advances havebeen made in the methods of identifying potential problemsand in new testing methods and tools. Also emphasized aretechniques to identify the assumptions on which a system isbuilt and to spot their weaknesses.

The Marktoberdorf Summer School 1995 'Logic of Computation' was the 16th in a series of Advanced Study Institutes under the sponsorship of the NATO Scientific Affairs Division held in Marktoberdorf. Its scientific goal was to survey recent progress on the impact of logical methods in software development. The courses dealt with many different aspects of this interplay, where major progress has been made. Of particular importance were the following. ¿ The proofs-as-programs paradigm, which makes it possible to extract verified programs directly from proofs. Here a higher order logic or type theoretic setup of the underlying language has developed into a standard. ¿ Extensions of logic programming, e.g. by allowing more general formulas and/or higher order languages. ¿ Proof theoretic methods, which provide tools to deal with questions of feasibility of computations and also to develop a general mathematical understanding of complexity questions. ¿ Rewrite systems and unification, again in a higher order context. Closely related is the now well-established Grabner basis theory, which recently has found interesting applications. ¿ Category theoretic and more generally algebraic methods and techniques to analyze the semantics of programming languages. All these issues were covered by a team of leading researchers. Their courses were grouped under the following headings.