Description
Until 2013 Skeptik has focused on the compression of propositional proofs generated by sat- and SMT-solvers. In 2014, Jan Gorzny, GSoC student in 2014, has started to generalise two of the proof compression algorithms (RecyclePivotsWithIntersection and LowerUnits) to first-order proofs generated by resolution-based first-order automated theorem provers (ATPs). Nevertheless, there are still many other proof compression algorithms that deserve to be generalised to the first-order case, and Jan's algorithms could still be improved in order to handle more proofs.
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 parser for proofs generated by the automated theorem prover SPASS is already available, but it handles only simple proofs that do not use the SPASS's most sophisticated inference rules. Having a fully general parser for unrestricted SPASS proofs would be useful. a combinator parser for first-order proofs in the TPTP TSTP format [1] would be very nice to have as well, since it would allow us to import proofs generated by many other theorem provers (e.g. Schultz's E prover).
The generalisation of the compression algorithms to the first-order case will involve some scientific creativity and, therefore, this is not an easy project. A solid knowledge of logic, automated deduction and basic proof theory is required.
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 downloaded from http://www.logic.at/people/bruno . Look for the IJCAR 2014 paper describing Skeptik. It provides a good starting point to learn more about Skeptik.
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 further extended from propositional to first-order logic.
Requirements
Solid knowledge of logic, automated deduction and basic proof theory is required. 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 highly desirable.
Mentors
Bruno Woltzenlogel Paleo, Jan Gorzny
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).