DTAI

Begeleiding

Onderzoeksgroep

Declaratieve Talen en Artificiële Intelligentie, KennisRepresentatie en Redeneren (KRR)

Context

Deze webpagina heeft als doel een overzicht van verschillende potentiele thema's en onderwerpen over logica, logische inferentie en/of toepassingen in de KRR-groep te geven. Sommige onderwerpen zijn nieuw, andere vind je al op de webpagina met thesisonderwerpen of zijn varianten ervan. Wie interesse heeft of meer wil weten of zelf een onderwerp wil aanbrengen kan contact opnemen met Prof. Marc Denecker.

Logica is de wetenschap van kennis, informatie, en het gebruik ervan voor het oplossen van taken en problemen door middel van inferentie. Het zijn onderwerpen van centraal belang in de informatica. Daarmee heeft logica en logische inferentie een fundamentele rol in computerwetenschappen, wat op dit ogenblik nog maar weinigen zich realiseren. De vraag is niet zozeer of logica en logische inferentiesystemen een rol zullen spelen in de informatica van de toekomst, wel wanneer ze dat zullen doen.

Hoe het ook zij, de evolutie in logica-gebaseerde verificatie, specificatie, problem solving en AI-tools gaat tegenwoordig enorm snel. In de komende 10, 15 jaar zal logica ongetwijfeld een steeds prominenter rol gaan spelen in software engineering.

De KRR groep werkt rond rijke uitbreidingen van klassieke logica (FO(.) genoemd) en rond inferentie-tools en nieuwsoortige toepassingen ervan. We bouwen er inferentie-tools voor (zoals het IDP-systeem) en onderzoeken nieuwsoortige toepassingen (zoals bv. het interactief configuratie-systeem voor het kiezen van een studieprogramma). Dit zijn uiteraard ambitieuze, toekomst- en onderzoeksgerichte doelstellingen. Gemotiveerde thesisstudenten kunnen hieraan een waardevolle bijdrage doen.

Thema's

IDP en zijn opvolgers

• T214: Een Debugger voor het IDP-systeem

  Debuggen van invoer voor modelgeneratoren en constraint solvers is vaak moeilijk wanneer een bug de invoer inconsistent maakt. Het doel van deze thesis is daar verbetering in te brengen door een debugger te ontwerpen voor de modelgenerator IDP.

• T232 Een IDE voor kennisgebaseerde software engineering

  Ontwerpen en implementeren van een Eclipse-plugin voor het kennisbanksysteem gebaseerd op FO(.). De IDE zal de gebruikers ondersteunen in het voorstellen van kennis in de taal FO(.), het uitvoeren van allerlei problem solving taken met het systeem en het debuggen van dergelijke programma's.

• T222 Appels met peren vergelijken

  Uitbreiden van de op klassieke logica gebaseerde taal FO(.) met natuurkundige eenheden.

• T244 Verbeteren van heuristieken voor zoekproblemen

  Versnellen van modelexpansie van FO(.) door het uitbuiten van de structuur van een probleem. Enerzijds door nieuwe heuristieken te onderzoeken en te implementeren, anderzijds door toe te laten om heuristieken op een declaratieve manier te specifiëren.

• Symmetriebreking in FO(.) (nieuw onderwerp)

  Veel zoekproblemen bevatten symmetrie. Bv. in het n-konninginnenprobleem zal elke permutatie van de koninginnen en elke spiegeling rond 1 van de assen een oplossing omzetten in een symmetrische oplossing. Het doel van symmetrie-breking is per groep van equivalente symmetrische oplossingen slechts 1 te berekenen om zo de efficientie te verbeteren. In sommige gevallen krijg je een exponentiele reductie van de zoekruimte.

Nieuwe toepassingen van logica in software engineering

• T248 GUI-generatie van de toekomst

  Automatisch genereren van grafische gebruikersomgevingen voor kennisgebaseerde configuratietoepassingen. Thesis in samenwerking met Agfa Healthcare (mogelijkheid tot stage).

• T220 Formele modellering en kennisrepresentatie in robotica

  In deze thesis is het de bedoeling om een modellering te bouwen van de diverse kennisbankcomponenten van een autonome robot die zich op een verkeerspark voortbeweegt. Thesis in samenwerking met co-promotor Prof. Herman Bruyninckx van de robotics onderzoeksgroep van Werktuigkunde.

  Een relevante paper: Combining High-Level Causal Reasoning with Low-Level Geometric Reasoning and Motion Planning for Robotic Manipulation

• T221 Kijken naar bordspellen: ontwikkeling van een kennisgebaseerd computervisie-systeem

  In deze thesis wordt een systeem ontwikkeld dat in staat is om een bordspel te volgen aan de hand van camerabeelden.

• T249 Klinische beslissingsondersteunende systemen

  Ontwerpen van een informatiesysteem om klinisch personeel te ondersteunen bij het nemen van beslissingen. Thesis in samenwerking met Agfa Healthcare (mogelijkheid tot stage).

• Building a logic-based expert system for Tracomilus dosage control in the Intensive Care Unit (Nieuw onderwerp)

  Building an expert system in collaboration with Intensive care of UZLeuven.

• Modelleren van uurroosters

  In deze thesis is het de bedoeling om een modellering op te stellen voor het plannen van lessen en uuroosters binnen een faculteit of departement. Uitdagen zijn hier zowel het voorstellen van alle gewenste beperkingen als de schaalbaarheid van de modellering naar meerdere groepen studenten en een langere tijdsperiode.

Verificatie van dynamische systemen

• T216 Event-B and de integratie van NuSMV en IDP

  Event-B is a formal language used by, e.g., Siemens to build executable specifications for large projects (e.g., Paris Metro Line 14). Pro-B is the verification system used by Siemens. In this thesis we want to study the Event-B language and its relation to the Linear Time Calculus in FO(.). We also want to develop a suitable representation of Event-B specifications in FO(.), and build tools that offer some of the most important functionality that the ProB system offers.

• T210: A study of lightweight software verification methods.

  The goal of the thesis is to make a comparative study of several lightweight software verification systems and methodologies. In collaboration with Prof. Dave Clark

• Vergelijkende studie van Alloy en IDP.

  Het doel van deze thesis is om een formeel model op te stellen van nieuwe functionaliteit van het moderne web, specifiek met als doel om na te gaan of deze veilig is en of er onbekende aanvalsvectoren bestaan. Verschillend met thesisonderwerp T117 over deze toepassing is het de bedoeling om deze modellering te gebruiken voor een vergelijkende studie van twee gerelateerde systemen: ALLOY en IDP, in het bijzonder om te onderzoeken wat het nut is van de grotere expressiviteit van IDP en een vergelijking te maken qua methodologie en efficientie.

Profiel

Interesse in logica.
1 student per onderwerp, veel onderwerpen.
Deze masterproef kan gekozen worden door

• alle studenten van de Master Toegepaste Informatica
• alle studenten van de Master Informatica
• alle studenten van de Master in de Ingenieurswetenschappen: Computerwetenschappen

Clusters waarin deze onderwerpen voorkomen

• Voorstelling van en redeneren met kennis
• Software engineering
• Computationele informatica
• Theoretische informatica