Parsers implementation and extension of proof compression algorithms from propositional to first-order logic

Skeptik [1] is a collection of data structures and algorithms focused especially on the compression of formal proofs.

Resolution proofs, in particular, are used by various sat-solvers, smt-solvers and automated theorem provers, as certificates of correctness for the answers they provide. These automated deduction tools have a wide range of application areas, from mathematics to software and hardware verification.

By providing smaller resolution proofs that are easier and faster to check, Skeptik aims at improving the reliability of these automated deduction tools and at facilitating the exchange of information between them.

This project aims to implement full TPTP-TSTP parsers [2] and a random generator of first order logic proofs to test a diverse variety of algorithms.

Regarding proof compression, this project aims to lift the ideas behind splitting proof compression algorithm [3] (developed for propositional logic) to first order logic and to explore improvements for similar algorithms already implemented in Skeptik.

References
[1] github.com/Paradoxika/Skeptik
[2] www.cs.miami.edu/~tptp/
[3] en.wikipedia.org/wiki/Resolution_proof_compression_by_splitting