DTAI

  • Increase font size
  • Default font size
  • Decrease font size
DTAI KRR Research Thesisonderwerpen
Masterproefonderwerpen: Logica: revolutie in de computerwetenschappen

Masterproefonderwerpen

Begeleiding

Informatie: Marc Denecker
Promotor: Marc Denecker
Begeleiders: Broes De Cat, Hanne Vlaeminck, Stef De Pooter

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

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
Last Updated on Thursday, 03 November 2011 14:52