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 soc2012@iue.tuwien.ac.at (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.