Skeptik:Extension of Proof Compression Algorithms from Propositional to FOL

by Jan Gorzny for Computational Science and Engineering at TU Wien

Skeptik is a proof-compression tool that currently excels at compressing propositional logic proofs. First-order logic proofs, a more difficult class of proofs, is currently under-supported in the tool due partly to a lack of appropriate algorithms. The proposed project would use existing algorithms for propositional logic proofs to guide the development and implementation of new first-order logic proof compression algorithms in order to allow Skeptik to support a wider range of proofs.