Støtte til et Constraint Handling Rules-projekt

Foto: Colorbox.dk

Foto: Colorbox.dk

DHT-forskeren prof. Henning Christiansen (CBIT) har modtaget støtte på kr. 2.315.925 fra Det Frie Forskningsråd/Natur og Univers til projektet:

Automatic support for Proving Confluence Modulo Equivalence for Constraint Handling Rules

Constraint Handling Rules (CHR) er et programmeringssprog, som består af genskrivningsregler over mængder af logiske atomer, og CHR har bevist sin slagkraft i forhold til mange former for logisk ræsonnering. En ønskværdig egenskab ved et CHR-program er konfluens, dvs. det slutresultatet er uafhængigt af rækkefølgen, reglerne udføres i. Et konfluent program kan optimeres ved styring af rækkefølge eller ved parallelitet. Bevis for konfluens indgår ofte i beviset for korrekthed af et program. Dette projekt generaliserer kendte metoder for bevis af konfluens til konfluens modulo en ækvivalensrelation (KME). Givet en ækvivalensrelation E, så er et program KME, hvis alternative sluttilstande er ækvivalente modulo E. KME er interessant, fordi det omfatter en væsentligt større og praktisk interessant klasse af programmer, f.eks. dynamisk programmeringsalgoritmer og redundante datastrukturer (f.eks. mængder repræsenteret ved træer). Projektet er også en undersøgelse af KME, som er nyt i forhold til CHR.

Leave a Reply

Your email address will not be published. Required fields are marked *