Automated Reasoning

Veel problemen, onder meer logistieke planning, optimalisatie van productieprocessen, verificatie van computersystemen en vele puzzels, laten zich beschrijven als een grote formule waarvan bewezen moet worden dat deze vervulbaar is. In dit vak willen we ingaan op de diverse methoden waarmee dergelijke problemen aangepakt kunnen worden en behandelen we de werking van relevante algoritmes. Hierbij staan we niet alleen stil bij een aantal theoretische aspecten van deze methodes, zoals de correctheid, volledigheid en efficiëntie, maar ook bij hun praktische toepassing. Aan de orde zullen komen:

• Resolutie als bewijsregel om proposities te bewijzen, en diverse algoritmen die op resolutie gebaseerd zijn.
• Uitbreiding naar Satisfaction Modulo Theories (SMT).
• Unificatie; resolutie op predicaten.
• Binary Decision Diagrams (BDDs) als efficiente representatie van Boolse functies.
• Toepassing hiervan op CTL-based symbolic model checking.

Na het volgen van dit vak ben je in staat om verschillende geautomatiseerde technieken voor het redeneren over logische formules toe te passen om realistische problemen op te lossen. In het bijzonder ben je aan het eind van dit vak in staat om:

• Resolutie, unificatie en gerelateerde algoritmes toe te passen om (on)vervulbaarheid van propositie- en predicaatformules te bewijzen.
• Uit te leggen hoe SMT-solvers generieke theorieën ondertsteuten en het simplex algoritme toe te passen om te redeneren over lineaire ongelijkheden.
• De gereduceerde, geordende binaire beslisboom (BDD) van een propositieformule the construeren.
• BDD’s te gebruiken om symbolisch model checking uit te voeren.
• Tools die de bovenstaande technieken implementeren te gebruiken om planning problemen op te lossen, software te verifiëren en deadlocks in hardware te detecteren.

Basic programming skills.

• Slides available on course web page
• Mathematical Logic for Computer Science by Mordechai Ben-Ari (https://doi.org/10.1007/978-1-4471-4129-7)