The computer science and engineering group of the Vienna University of Technology has been accepted as a mentoring organization for the 3rd consecutive year in Google's Summer of Code program (http://www.google-melange.com/gsoc/org/googl…2013/cse_tuwien), and *Skeptik* (https://github.com/Paradoxika/Skeptik/wiki/GSoC-Instructions) is one of its projects.
Skeptik is a tool for checking, compressing and improving formal proofs generated by automated deduction tools, currently focusing on propositional resolution proofs generated by Sat- and SMT-solvers. It implements various recent proof compression algorithms, such as RecyclePivots, RecyclePivotsWithIntersection, Split, Reduce&Reconstruct, LowerUnits, LowerUnivalents, as well as combinations and variants of these algorithms.
Students interested in applying for a Google Summer of Code grant (US$ 5000) to work from 17th of June to 23rd of September on the development of new proof compression algorithms within Skeptik should follow the instructions in this wiki-page: https://github.com/Paradoxika/Skeptik/wiki/GSoC-Instructions
The *DEADLINE* for student applications is 3rd of May 2013.
Before preparing their applications, students are encouraged to contact us (preferably by sending a message to our mailinglist (http://jwein2.iue.tuwien.ac.at:8080/mailman/listinfo/soc2013/) with "[Skeptik]" in the subject).
Best regards,
Bruno Woltzenlogel Paleo
--
Theory and Logic Group
Vienna University of Technology
http://www.logic.at/people/bruno/