08 October 2014
Master Thesis Defense by Mr Andreas Fellner
Mr Andreas Fellner defended his master thesis on 'Space & Congruence Compression of Proofs '
Mr Andreas Fellner defended his master thesis on 'Space & Congruence Compression of Proofs ' at TUW on 23 September 2014.
Abstract:
We propose two novel methods to compress SAT and SMT proofs in space and length. The space compression method builds on the analogy of the space measure and a specific pebbling game. Two algorithms to construct strategies in this game are proposed and evaluated. The length compression method searches for short explanations in the congruence reasoning part SMT proofs. We show that the problem of finding the shortest explanation is NP-complete and propose algorithms to find short, but not necessary the shortest explanation.