Title: CKM_1 Extracting logical information from requirements expressed in restricted natural language [ME,CS] Requirements specifications for engineering systems are often written using natural language descriptions. Company codes of practice and government regulations require that vast quantities of such information be generated, particularly in safety-critical applications. There is often too much information for people to be able, for example, to fully understand the interactions between system components (the "write-only documentation" syndrome). This leads to problems when changes must be made to system components. One approach to dealing with this problem is to attempt to express the information contained in requirements specs using logical sentences, which can then be used for automated reasoning. One of the problems of this approach is that of extracting the required information from the natural language descriptions. This is an example of the general problem of task-driven text interpretation: producing clearly prescribed structures (in this case logical sentences) from input text. The aim of this project is to investigate methods for automatic text interpretation and attempt to apply one or more of these to the generation of logical descriptions from requirements described using a restricted subset of natural language. The programming involved will probably use Prolog and/or C. References: P.S. Jacobs and L.F. Rau, Innovations in text interpretation, Artificial Intelligence, 63, pp143-191, 1993. N.E. Fuchs, Specifications are (preferably) executable, Software Engineering Journal, September, 1992. Title: CKM_2 Tools for describing requirements [IP,CS] Traditional requirements specification techniques such as Data Flow Diagrams, State Transition Diagrams and State Charts have proved to be useful tools for capturing requirements but are restricted in the analysis that they support. Logical descriptions, on the other hand, provide a sound basis for automated analysis of requirements, but are resisted by many engineers who find them unfamiliar or less intuitive. The aim of this project is to help bridge this gap by generating traditional representations, such as state descriptions, from logical descriptions and vice versa. The project will involve reviewing a number of traditional representations, developing programs to perform the functions described above (probably using Prolog), and comparing the expressiveness of the representations. It may also involve some user evaluation. References: Davis, A., Software Requirements and System Specifications. Prentice hall, 1990. Title: CKM_3 A Goedel Theorem Prover for the Temporal Logic BTK [ME,CS] The logic BTK is similar to a standard (or 'classical') logic, but gives time a special status by treating time points differently from other objects. Formally it is called a 'two-sorted' logic, the time points forming the second sort (or 'type'). This allows a user of the logic to implement, in a fairly straight-forward way, reasoning strategies which make use of this temporal information. Usually, however, this requires the availability of a general-purpose theorem prover for BTK. The main aim of this project is to develop a theorem prover for BTK by modifying a classical theorem prover to deal with two-sorted logic. The logic programming language Goedel is a new language which avoids many of Prolog's non-logical features, and adopts some of the features typically found in functional languages such as ML. In particular it has a strong type system which makes it a good candidate for the two-sorted theorem prover. The secondary aim of this project is to assess the utility of Goedel for this task, compared with traditional languages such as Prolog. References: F. Bacchus, J. Tenenberg and J.A. Koomen, A non-reified temporal logic, Proc. 1st International Conference on Principles of Knowledge Representation and Reasoning, pp 2-10, 1989. Extended version in Artificial Intelligence, 1991. M. Fitting, First-order Logic and Mechanical Theorem Proving, Springer-Verlag, 1990. J. Lloyd et al, The Goedel Programming Language, in print (available in Technical Report form). Title: CKM_4 Collision Avoidance Using Automated Reasoning [CS,ME] The need to avoiding collisions between mobile agents (robots, airplanes, trains, etc) is a common problem and one which we would like to be able to deal with automatically. This entails describing the situations, predicting collisions, and employing strategies for avoiding them. Logic-based approaches to this problem have a number of possible advantages. First, the situations involved are often safety-critical and we need to be sure that the reasoning employed is correct. Secondly, we would like the reasoning process to be independent of the domain of application, so that it can be ported to any domain which permits a suitable logical description. The aim of this project is to compare two or more temporal logics as candidates for this task, develop suitable collision avoidance strategies, and demonstrate the use of the resulting system for avoiding collisions between simulated agents in a microprocessor controlled grid (Turner, 93). The project will involve the use of Prolog (for implementing automated reasoning) and probably some use of C (the language used by the grid). References: M. Ben-Ari, Mathematical Logic for Computer Science, Prentice Hall, 1993. W. Turner, Interfacing Prolog to a Microprocessor Controlled Grid, University of York, 3rd Year Project, 1992/93. Title: CKM_5 A Quantity Knowledge Base [CS] In many practical reasoning problems the solutions are constrained by relationships between real-valued quantities such as times, distances, temperatures, pressures and so on. A quantity knowledge base is a reasoning subsystem which is devoted to maintaining these mathematical relationships. Generally this consists of a network of nodes, corresponding to quantitative parameters, connected by constraints, and some strategy for propagating constraints around the network. 'Label inference' (Davis, 87) in which nodes are labelled with sets of possible values and successively refined, is one strategy for constraint propagation which has attractive properties both in terms of control and correctness. The aim of this project is to implement the algorithm for label inference proposed by Davis and link this with a reasoning system (such as a temporal or spatial reasoning system) with quantitative constraints. It is likely that the project will involve programming in C and interfacing to Prolog, and may involve comparison with alternative systems such as Goedel and/or publicly available constraint logic programming systems. References: E. Davis, Constraint propagation with interval labels, Artificial Intelligence, 32, pp 281-331, 1987. Title: CKM_6 A Slightly Intelligent Keyboard [IP,CS] Entering textual information into computers has formed a growing part of the daily activities of many people at work, and with the spread of electronic mail and information systems is gradually entering the home as well. In a text entering device there is a trade-off between the "cost" in terms of physical effort (eg number or range of keystrokes required) and the complexity of generating the approriate strings. The traditional keyboard is at one end of this spectrum, requiring great dexterity from the user, with a simple algorithm for mapping keys to characters. While this is (arguably) quite efficient for many users, for users with physical disabilities the cost of physical effort is often greater, and computational aids have an important role to play. Computational aids for text entry typically include encoding and prediction algorithms, both aimed at producing more text from fewer keystrokes. This project involves surveying existing encoding and prediction schemes, and attempting to express one or more schemes within a formal, implementation independent, setting (for example, logic or grammar rules). The rules would then be manipulated by a general purpose inference system, probably written in Prolog. (As a CS project this may also involve looking at some "machine learning" techniques.) References: J. J. Darragh and I. H. Witten, The Reactive Keyboard, Cambridge Series in Human-Computer Interaction, Cambridge University Press, 1992. A. D. N. Edwards (ed), Extra-Ordinary Human-Computer Interaction: Interfaces for Users with Disabilities, Cambridge University Press, 1994.