Decision procedures for equality logic with uninterpreted functions

In dit proefschrift presenteren we een aantal technieken om vervulbaarheid (satisfiability) vast te stellen binnen beslisbare delen van de eerste orde logica met gelijkheid. Het doel van dit proefschrift is voornamelijk het ontwikkelen van nieuwe technieken in plaats van het ontwikkelen van een effici¨ente implementatie om vervulbaarheid vast te stellen. Als algemeen logisch raamwerk gebruiken we de eerste orde predikaten logica zonder kwantoren. We beschrijven enkele basisprocedures om vervulbaarheid van propositionele formules vast te stellen: de DP procedure, de DPLL procedure, en een techniek gebaseerd op BDDs. Deze technieken zijn eigenlijk families van algoritmen in plaats van losse algoritmen. Hun gedrag wordt bepaald door een aantal keuzen die ze maken gedurende de uitvoering. We geven een formele beschrijving van resolutie, en we analyseren gedetailleerd de relatie tussen resolutie en DPLL. Het is bekend dat een DPLL bewijs van onvervulbaarheid (refutation) rechtstreeks kan worden getransformeerd naar een resolutie bewijs van onvervulbaarheid met een vergelijkbare lengte. In dit proefschrift wordt een transformatie ge¨introduceerd van zo’n DPLL bewijs naar een resolutie bewijs dat de kortst mogelijke lengte heeft. We presenteren GDPLL, een generalisatie van de DPLL procedure. Deze is bruikbaar voor het vervulbaarheidsprobleem voor beslisbare delen van de eerste orde logica zonder kwantoren. Voldoende eigenschappen worden ge¨identificeerd om de correctheid, de be¨eindiging en de volledigheid van GDPLL te bewijzen. We beschrijven manieren om vervulbaarheid vast te stellen binnen de logica met gelijkheid en niet-ge¨interpreteerde functies (EUF). Dit soort logica is voorgesteld om abstracte hardware ontwerpen te verifi¨eren. Het snel kunnen vaststellen van vervulbaarheid binnen deze logica is belangrijk om dergelijke verificaties te laten slagen. In de afgelopen jaren zijn er verschillende procedures voorgesteld om de vervulbaarheid van dergelijke formules vast te stellen. Wij beschrijven een nieuwe aanpak om vervulbaarheid vast te stellen van formules uit de logica met gelijkheid die in de conjunctieve normaal vorm zijn gegeven. Centraal in deze aanpak staat ´e´en enkele bewijsregel genaamd gelijkheidsresolutie. Voor deze ene regel bewijzen wij correctheid en volledigheid. Op grond van deze regel stellen we een volledige procedure voor om vervulbaarheid van dit soort formules vast te stellen, en we bewijzen de correctheid ervan. Daarnaast presenteren we nog een nieuwe procedure om vervulbaarheid vast te stellen van EUF-formules, gebaseerd op de GDPLL methode. Tot slot breiden we BDDs voor propositionele logica uit naar logica met gelijkheid. We bewijzen dat alle paden in deze uitgebreide BDDs vervulbaar zijn. In een constante hoeveelheid tijd kan vastgesteld worden of de formule een tautologie is, een tegenspraak is, of slechts vervulbaar is.