Umfang

Dieses Thema kann als Bachelorarbeit bearbeitet werden.

Empfohlene Vorkenntnisse

  • logische Programmierung
  • Aussagenlogik

Problemstellung

ProB ist ein animator und model checker für B und Event-B. Die Grundlage hierfür ist ein Constraint Solver für die B Sprache welcher Techniken des Constraint Logic Programming verwendet. Neben dem eigenen Constraint Solver hat ProB eine eigene SMT Solver implementierung in Prolog, welche auf dem sogenannten DPLL(T) Algorithmus basiert. Hierbei wird SAT Solving mit Theory-spezifischen Constraint Solvern kombiniert. Für den SAT Solver müssen aussagenlogische Terme in konjunktive Normalform (KNF) überführt werden. Dies ist im Allgemeinen einfach, jedoch kann die Anzahl der Klauseln exponentiell steigen und somit die Überführung in KNF sehr langsam werden. Die ist z.B. der Fall wenn das Distributivgesetz auf zwei große Konjunktionen angewendet wird: (A & B & C) or (D & E & F) Tseitin hat dieses Problem durch die Einführung künstlicher Variablen verbessert, so dass kein exponentielles Wachstum mehr vorliegt. Bei obigem Beispiel kann z.B. eine Variable P eingeführt werden, um die Anwendung des Distributivgesetzes zu vereinfachen: ((A & B & C) or P) & (P <=> (D & E & F)) Es wurde jedoch festgestellt, dass nicht in jedem Fall eine künstliche Variable eingeführt werden muss (siehe An Optimality Result for Clause Form Translation und On Generating Small Clause Normal Forms). Dies kann anhand der vorhanden Polaritäten der Variablen in den verschachtelten Termen entschieden werden. Diese effiziente Umwandlung aussagenlogischer Formeln in KNF mit möglichst wenigen künstlichen Variablen soll in dieser Arbeit in Prolog implementiert und im Rahmen des SMT Solving mit ProB ausgewertet werden. Des weiteren sollen Regeln für eine effiziente Umschreibung von Äquivalenzen mittels Konjunktionen und Disjunktionen implementiert werden.

Minimalanforderungen

  • effiziente Umwandlung in KNF mit möglichst wenigen künstlichen Variablen
  • effiziente Umschreibung von Äquivalenzen
  • Auswertung im Bereich des SMT Solving

Kontakt

Joshua Schmidt
Raum 25.12.02.52 · joshua.schmidt@hhu.de