Description

SMT-proofs are composed of a propositional resolution proof in the bottom and "theory proofs" in the top. The simplest theory supported by SMT-solvers is the theory of equality with uninterpreted functions. Statements in the language of this theory can be decided modulo this theory using congruence closure algorithms. In 2014, Andreas Fellner (who was GSoC student in 2012) implemented the first algorithm aiming at compressing such congruence closure proofs. His algorithm was based on a variant of Dijkstra's shortest path algorithm applied to congruence graphs. However, due to the NP-completeness of this problem, this algorithm is not able to find the shortest congruence explanation.

This project idea aims at extending Andreas' algorithm in order to guarantee that minimally short explanations are found. To achieve this, we propose a brute-force approach, in which literals in the explanation to be shortened are incrementally removed while the explanation remains invalid. The choice of which literal to remove may be done heuristically and may influence the size of the minimally short explanation.

[1] To learn more, have a look at Andreas' MSc thesis: https://github.com/AFellner/Thesis/blob/master/latex/thesis.pdf .

Benefit for the Student

The student will acquire practical experience and be in touch with cutting-edge research in the fields of automated deduction and applied proof theory. He will be mentioned as a co-author of any paper that might benefit from his implementation. He will have the pleasure of programming in the awesome language Scala.

Benefit for the Project

Skeptik capability of compressing congruence closure proofs will be improved.

Requirements

Solid knowledge of logic, automated deduction and basic proof theory is required. Knowledge of Scala or experience with other object-oriented (e.g. Java, C++,...) and functional (e.g. Haskell, OCaml,...) programming languages and willingness to learn Scala is required. Experience with data structures for proofs or directed acyclic graphs is highly desirable.

Mentors

Bruno Woltzenlogel Paleo, Andreas Fellner

More information

Instructions on how to improve your chances of getting accepted are listed on Skeptik's wiki (https://github.com/Paradoxika/Skeptik/wiki/GSoC-Instructions).