Geavanceerde technieken voor grounden en solven in het IDP kennisbanksysteem

Het gebied van Kennisrepresentatie en Redeneren, een onderdeel van het veld Artificiële Intelligentie, bestudeert hoe kennis kan worden voorgesteld en hoe die kan gebruikt worden voor automatische redeneertaken.
Verschillende declaratieve programmeerparadigmas implementeren dit door middel van een formele taal om kennis voor te stellen en een bijbehorende vorm van inferentie om het beoogde resultaat te behalen.
Recentelijk werd het Kennisbank Systeem (KBS) paradigma voorgesteld.
Dit is gebaseerd op het idee dat kennis niet inherent geassocieerd is met een specifieke redeneertaak.
Dit paradigma stelt voor om de kennis op een werkelijk declaratieve manier voor te stellen, in tegenstelling to eerdere aanpakken.
Als een toegevoegd voordeel wordt de mogelijkheid voorzien om kennis te hergebruiken voor verschillende redeneertaken die elk een oplossing bieden voor een bepaald probleem.
De initiële implementatie van het KBS paradigma, ook gekend als het IDP3 systeem, heeft gediend als een geschikt laboratorium om nieuwe technieken in software engineering te onderzoeken.

De huidige generatie aan declaratieve programmeersystemen, zoals IDP3, clasp, WASP, lp2sat, gebruiken een ground-en-solve aanpak.
Bij deze aanpak wordt de specificatie met rijke taalconstructen eerst omgezet in een voorstelling die op een lager niveau werkt en geen van de rijkere taalconstructen gebruikt.
Dit proces wordt "grounding" genoemd.
Een tweede stap bestaat uit het verwerken van deze voorstelling met behulp van een algemene, laag-niveau solver die gewoonlijk gebaseerd is op technieken uit het SAT (satisfiability) veld.
Deze thesis bevat een grondige studie over de impact van verschillende "grounding" aanpakken op het gedrag van de onderliggende solver.

De taal die ondersteund wordt door het IDP3 systeem bevat constraints en definities.
In de context van deze thesis worden deze definities opgedeeld in twee categoriën: de "input*" en de "zoek" definities.
Input* definities zijn definities die afhangen van concepten die reeds gekend zijn, wat wil zeggen dat deze definities op voorhand uitrekenbaar zijn zonder dat er een zoekstap aan te pas komt.
Dit soort definities wordt ook wel "intentional" of "stratified" genoemd, oftwel "domain atoms" in de literatuur.
Een van de bijdragen van dit werk is de evaluatie van deze input* definities met behulp van het XSB Prolog systeem.
Om deze aanpak te kunnen volgen, moeten deze definities omgezet worden naar een formaat dat bruikbaar is door het Prolog systeem.
De grootste uitdaging bij deze omzetting ligt in het correct transformeren van de types en andere rijkere taalconstructen, zowel als in het rekening houden met het uitvoeringsmechanisme van Prolog dat van links naar rechts werkt.
De "zoek" definities kunnen niet op voorhand uitgerekend worden en hangen nog af van ongekende data.
Deze tekst verduidelijkt hoe de bovenstaande omzetting kan veralgemeend worden om dit soort "zoek" definities gedeeltelijk uit te rekenen, waarbij er zoveel mogelijk informatie al wordt afgeleid.

We ontwikkelen een methode om de solver ge begeleiden gedurende het zoekproces en voorrang te geven aan delen van de zoekruimte die relevant zijn.
Enkel het deel van de zoekruimte dat is verbonden met de huidige zoektak van het probleem moet hierbij in acht genomen worden.
Het doel van deze techniek is het voorkomen van beslissingen waarvan kan bewezen worden dat ze geen bijdrage hebben tot het bekomen van een oplossing in de huidige zoektak.
Hierbovenop geniet het zoekproces van een nieuw en verbeterd stopcriterium, omdat de eindstatus van de solver niet meer een hoeft te zijn wanneer de waarde van alle variabelen gekend is.
We presenteren ook een implementatie die gebruik maakt van een incrementele aanpak, waarbij gegevensstructeren worden aangepast op basis van de veranderingen in de status van de solver.

Met dit werk verhogen we de gebruikbaarheid van het IDP3 systeem en bekomen we een meer robuster vorm van deze alternatieve aanpak tot softwareontwikkeling.