Description

RecyclePivotsWithIntersection (RPI) and LowerUnits (LU) have been developed for propositional resolution proofs only. This means that, so far they can only compress proofs generated by sat-solvers and smt-solvers, but not by first-order automated theorem provers. We would like to generalize our proof data-structures and these algorithms to the first-order case, and to evaluate them on the benchmarks provided by the TSTP library.

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

Invaluable. :-)

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 the first-order resolution calculus and unification is 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.