Skeptik: Heuristics and Improvements for Split and Reduce&Reconstruct

		Description
"Split" is an algorithm that compresses a given propositional resolution proof by first selecting a literal "L", then splitting the refutation into a proof of "L" and proof of "(not L)", and finally constructing a new refutation by resolving these two proofs. This process can be repeated until no further compression occurs. We have reasons to believe that the current heuristic for selecting the literal "L" is far from optimal. Furthermore, it seems to be possible to improve compression by using recursion instead of mere repetition of the process. 
"Reduce&Reconstruct" searches for locally redundant configurations of subproofs and reduces them to smaller subproofs. We believe it might be possible and beneficial to combine the non-expensive reduction rules of "Reduce&Reconstruct" in the proof fixing phase of other algorithms such as "RecyclePivotsWithIntersection" and "LowerUnivalents". "Reduce&Reconstruct" also performs expensive reshuffling of subproofs (by changing the order of resolution steps, using the proof rewriting rule A2), in order to form new reducible redundant configurations. Currently, this reshuffling is done in a rather ad-hoc way. It might be possible to develop heuristics to perform the reshuffling more efficiently.

This idea comprises and addresses issues #35, #41, #36, #37 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
"Split" and "Reduce&Reconstruct" are among the most compressing algorithms available, but they are far from being the most efficient. If the ideas discussed above are successfully implemented, Skeptik will be able to provide more efficient algorithms to the research community.
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=heuristics_and_improvements_for_split_and_reduce_reconstruct
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.