Supervisor for bachelor and master students:
**Jørgen Villadsen, Associate Professor, PhD MSc**

General prerequesits:
**Good knowledge of a higher level programming language (for example Java), basic algorithms and data structures, and discrete mathematics (elementary logic)**

NB: The proposals are first and foremost meant as inspiration since the precise conditions must be negotiated in each case.

Classical logic predicts that everything (thus nothing useful at all) follows from inconsistency. A paraconsistent logic is a logic where an inconsistency does not lead to such an explosion. Since in practice consistency is difficult to achieve there are many potential applications of paraconsistent logics in knowledge-based systems, logical semantics of natural language, etc. A particular paraconsistent many-valued logic has been proposed and experiments have been carried out in an Erasmus student project. The goal is to develope a prototype of a paraconsistent knowledge-based system, either by model checking or theorem proving techniques. In particular a case study in the domain of medicine could be considered. A long term aim is the study of a paraconsistent higher order logic and its applications in computer science as well as its use as a classical foundation of mathematics.

In computer science an agent is anything from a few lines of code automatically executed on certain primitive conditions to complex AI systems like robots. A rational agent bases its actions on a model of the world including both declarative and procedural knowledge, also called know-that and know-how, respectively. The know-how must describe how actions of agents change the world, and for this purpose a programming language called NIL: Natural Imperative Language has been proposed. The language can be given a direct operational semantics in definite clauses, but a denotational semantics in a higher order logic is also possible. The goal is to develope a prototype of a program interpreter for the NIL language, and to use the system in a suitable case study. Planning and scheduling problems for multiagent systems could also be considered.

The growing criticality and complexity of computer applications is wellknown and for safety and/or security there is no substitute for formal proofs. A previous advanced student project described the use of the proof assistent Isabelle for verification of Quicksort. The goal is to investigate how to verify cryptographic protocols in automated reasoning systems.

Computational linguistics is a research area with many challenges. The goal is to study natural language processing using a categorial grammar and a higher order logic for semantics. A previous Erasmus student project can be used as a starting point for the work on lexical and logical combinators for semantics. The report was later published by Juan Fernández Ortiz as his graduation thesis (Technical University of Madrid).

PS: Colorless green ideas sleep furiously.

Autumn 2006

02125 Bachelor Project in Software Technology (Administration)

02153 Declarative Modelling (Logical Part)

Spring 2007

02125 Bachelor Project in Software Technology (Administration)

02348 Programming Techniques (Algorithms Exercises / Examination)

Autumn 2007

02125 Bachelor Project in Software Technology (Administration)

02153 Declarative Modelling (Logical Part)

02156 Formal Logical Systems (Examination)

Spring 2008

02125 Bachelor Project in Software Technology (Administration)

02348 Programming Techniques (Algorithms Exercises / Examination)

Autumn 2008

02101 Introductory Programming (Design)

02156 Formal Logical Systems

Spring 2009

02102 Introductory Programming (Partly)

02285 Artificial Intelligence and Multi-Agent Systems (Partly)

02326 Algorithms and Data Structures (Exercises / Examination)

02348 Programming Techniques (Algorithms Exercises / Examination)