The quest for simpler proofs goes back at least to Hilbert's recently rediscovered 24th Problem, but it has become more relevant nowadays, as proofs generated by automated reasoning tools can be long and redundant. Fulfilling the practical need for algorithms that compress and improve proofs is the goal of the Skeptik tool (https://github.com/Paradoxika/Skeptik), which is implemented in Scala.
Although Skeptik's algorithms are theoretically very efficient, running in only linear time w.r.t. the length of the proofs, several inefficiencies in their current implementation cause Skeptik to fail on extremely large proofs, such as proof related to Erdos conjecture (http://www.newscientist.com/article/dn25068-wikipe...). We need several implementation improvements (faster parsing, more clever proof replaying, parallelization, caching, indexing, hashing...) in order to cope with huge proofs.
Goals of this project
The goal of this project is to implement various techniques to increase the efficiency of Skeptik on propositional proof compression.
Some background in logic. Good implementation skills in object-oriented and functional programming.
Become acquainted with proof theory; gain experience in programming in Scala; practice writing efficient code; publish papers about Skeptik's improvements.
Our papers are available at: https://github.com/Paradoxika/Papers