This paper describes our work on improving interaction between humans and mobile robots on navigation tasks. To represent and reason about humans' route instructions, a user-centered qualitative spatial model -- the Conceptual Route Graph -- is introduced. Three reasoning strategies based on this conceptual model are discussed, which enable a mobile robot to generate different clarification responses if spatial mismatches are detected in route instructions. Moreover, results of an empirical study to evaluate and compare their effects on people's navigation activities are presented.

In order to allow severely disabled people who cannot move their arms and legs to steer an automated wheelchair, this work proposes the combination of a non-invasive EEG-based human-robot interface and an autonomous navigation system that safely executes the issued commands. The robust classification of steady-state visual evoked potentials in brain activity allows for the seamless projection of qualitative directional navigation commands onto a frequently updated route graph representation of the environment. The deduced metrical target locations are navigated to by the application of an extended version of the well-established nearness diagram navigation method. The applicability of the system proposed is demonstrated by a real-world pilot study in which eight out of nine untrained subjects successfully navigated an automated wheelchair, requiring only some ten minutes of preparation.

Transformations are functions over programs that adhere to some program refinement relation. The power of transformations stems, in the first instance, from the flexibility available within the transformation system for representing design decisions, which requires that transformations be parameterized with the knowledge of problem domain; and second, on the ability to reuse developments in an effective manner, after some modifications have been made to the problem definition. In this paper, knowledge-based transformational programming in the PROSPECTRA system is presented. The strength of this approach arises from the smooth combination of knowledge bases and transformations in the development and re-development of programs. In particular, emphasis is placed on the separation of concerns achieved by the effective partitioning of problem domain knowledge and problem specification.>

Two approaches to the development of efficient and correct iterative programs are contrasted: the construction of an iterative program and a proof of its correctness using invariant assertions of loops, and the construction and proof of a recursive program with a subsequent transformation into an iterative version by schematically applying suitable recursion removal rules. The connection between the approaches is demonstrated by augmenting such transformation rules by inductive assertions. It is argued that the latter approach to program development is superior since the correctness proof of a recursive program is easier in most cases. Considerable verification overhead can be avoided this way, in particular, some difficulties with the interaction of successive loops and their associated invariants.