Description

The Splitting algorithm (proposed in the 2010 paper "Two Techniques for Minimizing Resolution Proofs" by Scott Cotton in the SAT conference) and the ReduceAndReconstruct algorithm (proposed in the 2010 paper "An Efficient and Flexible Approach to Resolution Proof Reduction" by Simone, Brutomesso and Sarygina in the Haifa Verification Conference) are two alternative algorithms for propositional resolution proof compression. Splitting consists of dividing a refutation into a proof of "a" and a proof of "not a", for some predicate "a", and then recombining these two proofs into a new refutation. ReduceAndReconstruct consists of applying local rewrite rules that are known to reduce the size of proofs. These two algorithms need to be implemented in the ResK framework.

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

The implementation of these two algorithms will enable a proper comparison of all algorithms and will allow us to combine their strengths.

Requirements

Moderate skills in Scala or experience with object-oriented programming (e.g. Java, C++,...) or functional programming (e.g. Haskell, OCaml,...) and willingness to learn Scala (don't worry! It is easy!). Experience with data structures for proofs or directed acyclic graphs is a plus, but not necessary.

Mentors

Bruno Woltzenlogel Paleo, Josef Weinbub

Contact

Send an email to This email address is being protected from spambots. You need JavaScript enabled to view it. (first subscribe here) using the prefix [ResK].

More Information

Instructions on how to improve your chances of getting accepted are listed on the ResK-wiki.