Efficient Propositional Proof Compression

Research areas

Description

Outline

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. 

Requirements/Prerequisites

Some background in logic. Good implementation skills in object-oriented and functional programming.

Student Gain

Become acquainted with proof theory; gain experience in programming in Scala; practice writing efficient code; publish papers about Skeptik's improvements.

Background Literature

Our papers are available at: https://github.com/Paradoxika/Papers

Links

 

Updated:  1 November 2018/Responsible Officer:  Head of School/Page Contact:  CECS Marketing