Descirption
Skeptik has so far focused on the compression of propositional proofs generated by sat- and SMT-solvers. Now we would like to extend some of its algorithms to first-order proofs generated by resolution-based first-order automated theorem provers (ATPs). Skeptik’s data structures are already general enough to handle first- and even higher-order formulas. There are general abstract data structures for proofs, but they will have to be specialised (via inheritance) to deal with specific inference rules used by various ATPs. Furthermore, a combinator parser for first-order proofs in the TPTP TSTP format [1] needs to be implemented. The generalisation of the compression algorithms to the first-order case will involve some scientific creativity and will probably require some familiarity with the notion of unification, although a draft implementation of a unification algorithm is already available in Skeptik. We recommend the generalisation of the RecyclePivotsWithIntersection and LowerUnits algorithms [2], but you are welcome to study other algorithms as well and think about the viability of extending them to the first-order case.
In the previous two years, Skeptik’s GSoC students have achieved great academic success and were able to publish and present their results in high-level conferences. We are committed to provide similar opportunities to this year’s GSoC students, and we are looking for students that are enthusiastic about these opportunities! If you are interested in this project idea, please contact us as soon as possible.
[1] TSTP is the proof format used by the TPTP library of automated deduction problems maintained by Geoff Sutcliffe at the University of Miami. Google it to know more!
[2] Papers about these algorithms can be download from http://www.logic.at/people/bruno . Look for the CADE 2011 paper about regularisation and the TABLEAUX 2013 paper about lowering subproofs.
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
Skeptik’s application scope will be extended from propositional to first-order logic.
Requirements
Basic knowledge of 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
Instructions on how to improve your chances of getting accepted are listed on Skeptik's wiki (https://github.com/Paradoxika/Skeptik/wiki/GSoC-Instructions).
http://www.iue.tuwien.ac.at/cse/wiki2014/doku.php?id=extension_of_proof_compression_algorithms_from_propositional_to_first-order_logic