Description

RecyclePivotsWithIntersection (RPI) and LowerUnits (LU) (described by the mentor in detail in a 2011 paper in CADE, the Conference on Automated Deduction) are currently among the most powerful algorithms for the compression of propositional resolution proofs. We have already empirically determined that it is beneficial to combine RPI and LU sequentially, but the optimal order for the sequential combination is unknown. Therefore, we would like to implement a tighter non-sequential combination of RPI and LU, and to show that it is always better than both sequential combinations in terms of compression rate and speed.

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

We expect the non-sequential combination to be about twice faster than any of the sequential combinations, because the number of required proof traversals would be cut to half.

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, Karl Rupp

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.