Skeptik: RecycleUnits, Subsumption and Intermediate RP-RPI Algorithms

		Description
There are a few proof compression algorithms that are not yet implemented in Skeptik, even though they have already been described in the literature and implemented elsewhere. We would like these algorithms to implemented, generalized and improved.
One of them is "RecycleUnits" which implements an efficient restricted kind of subsumption in which the subsuming clause is unit. Besides implementing the original "RecycleUnits", we would like to generalize it to larger non-unit subsuming clauses.
Another algorithm is (unrestricted) "Subsumption". While a naive implementation would most probably be too inefficient, the use of some clever data structures to compare many clauses simultaneously might give it the needed efficiency.

Finally, while "RecyclePivots" and "RecyclePivotsWithIntersection" have been already implemented in Skeptik, there are a few easy variants that remain to be implemented.

This idea comprises and addresses issues #14 and #16 in our issue tracker (https://github.com/Paradoxika/Skeptik/issues?state=open).  

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
If all mentioned algorithms are implemented, Skeptik will contain practically all known propositional resolution proof compression algorithms known to this date.
Requirements
Basic knowledge of (propositional) logic is required. Basic 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 desirable.
Mentors
Bruno Woltzenlogel Paleo, Joseph Boudou
Contact
Mentors are regularly around in our GSoC IRC channel #TU-CSE-SoC at irc.freenode.net. You can also reach us via the mailinglist – send an email to This email address is being protected from spambots. You need JavaScript enabled to view it. using the prefix [SKEPTIK] (a subscription is required).
More Information
http://www.iue.tuwien.ac.at/cse/wiki/doku.php?id=recycleunits_subsumption_and_intermediate_rp-rpi_algorithms
Instructions on how to improve your chances of getting accepted are listed on Skeptik's wiki (https://github.com/Paradoxika/Skeptik/wiki/GSoC-Instructions). In our issue tracker you can also find other ideas.