BK 1R - Simplified Temporal Resolution for Propositional Linear Time Logic

Propositional linear time logic (PLTL) allows one to express how propositions change their truth value in time. In particular, this logic can be used to express and verify dynamic properties of hardware and software systems, which makes the development of reasoning methods for this logic practically interesting. A. Degtyarev, M. Fisher, and B. Konev suggested a resolution-style calculus for PLTL This method, termed simplified temporal resolution, was, however, never implemented. The aim of this project is to implement the simplified calculus using efficient solvers for the Boolean satisfiability problem (SAT solvers), which currently became available. This project involves reading and understanding a research paper, developing the code which communicates with an external program written by somebody else, and performance measuring the resulting program against existing provers for this logic.

BK 2R - Protege Plugin for Ontology Module Extraction

In computer science, ontologies are used to provide a common vocabulary for a domain of interest together with descriptions of the meaning of terms built from the vocabulary and relationships between them. Ontologies in this sense are increasingly used in knowledge management systems, medical and bio-informatics, and are set to play a key role in the semantic web and grid. In order to be computer-accessible, modern ontologies are formulated in a logic-based ontology language such as OWL. The ontology engineering and maintenance is supported by ontology editors such as Protege. Healthcare and life science ontologies often tend to be large and complex. In many practical cases, however, only a part of the ontology relevant to an application in hand would suffice. Konev, Lutz, Walter and Wolter developed an algorithm for extracting semantic modules from ontologies formulated in the lightweight fragment of OWL, OWL-EL. A prototype implementation of the algorithm is available.
The purpose of this project is to research into, design, and develop a Protege plugin communicating with the prototype implementation, and presenting the extracted modules to the user. Protege is written in Java, the prototype implementation is written in OCaml.

BK 3P - Writing a Handheld Computer Application

Programming for handheld devices (such as mobile phones, PDAs, smartphones etc) is very challenging due to their limited computing resources (low memory, slow CPU, poor graphics), yet it becoming more and more demanded. The aim of this project is to develop an application of your choice for a handheld computer such as a computer game or a useful utility.
I would expect an interested person to come and see me to discuss a possible application. I am happy to supervise a student-specified project based on this description. (However, if you do not have a good idea in mind, I can suggest implementing an analog of the Tetris game).

DISCLAIMER: the department will NOT provide you with a handheld device or any other equipment you may need to work on your project. Please make sure you have all necessary hardware before you decide to take this project. You must also make sure that there is a development kit available for the particular device you have (and that you have such a kit)!
Note also that our technical support staff may not have knowledge to help you out if something goes wrong.
I would expect this project to be taken ONLY by a truly interested person. If you are not interested, please do not select this project even as your last choice since you may still get it. This one is not an easy ride.

BK 4P - Landscape Modelling

There exist a number of programs capable to show "realistic" landscapes (in particular, computer games and landscape generators); however, they cannot usually depict a real place. The project consists of developing a tool generating a landscape view given a description of a particular landscape (that is, given a map with geodesic information supplied with a description of the surface and some details on it such as trees etc, for example, in the USGS Digital elevation Models format) and capable to depict movement through this landscape in real time. The program could also be extended with "extra" features such as fog and other weather conditions.

BK 5P - Visual program construction tool for Logo

Logo is a programming language specifically designed to teach novice users including small children to write simple programs. A typical program controls a little robot turtle, which executes commands and draws a picture. The language features modularity, extensibility, interactivity, and flexibility. More information on Logo and sample programs can be found here. The development of Logo started in mid 1960s and the language was released to the general public in mid 1980s. At the time, visual programming tools were not available and a user must type the program, which does not go easy with small - the target user group for this language. This project involves first researching into how to represent language constructs in an accessible way and how to synthesise programs using a graphical tool without the need to type code. Further, the obtained specification needs to be implemented so that Logo code is generated (and showed to the user for teaching purposes) and executed by the Logo system.

BK 7D - Maintaining a Collection of Multiple Choice Questions

Multiple-choice questions became quite popular in this and other departments. Lecturers have big collections of such questions; while preparing the exam one selects a subset from the collection. After the examination, a lecturer is given feedback on what percentage of students answered correctly to a particular question. The aim of this project is to implement a database and a front-end application to assist preparing MC exams. A user should be able to insert questions into the database in a particular format (I personally use LaTeX to write my questions), annotate the questions with the feedback and other attributes, select questions for an exam, reshuffle questions in a random order, and see the resulting exam paper. The questions should not be made accessible to anybody, so the web technology cannot be used to implement this project unless tight security measures are taken

BK 8D - Photograph on the Web and Access Rights Management

Maintaining a collection of digital photographs becomes harder when the collection grows. Quite often people make their pictures available on the Web; however, it is not always desirable to let just anybody to see all the pictures, especially, private pictures. The aim of this project is to develop a web application capable of storing large collection of pictures. A collection owner should be able to brows, add, and delete pictures. Pictures may be annotated with some textual description and have attributes (such as venue, date, quality etc). In addition, the owner should be able to select some pictures from the collection and make the selected pictures available to users (e.g. in form of a link and/or username/password). A user can only brows the available pictures. The owner and users should authenticate themselves and it should not be allowed to a user to browse pictures outside of the selection made available to her/him. ~ ~