Description

Until 2013 Skeptik has focused on the compression of propositional proofs generated by sat- and SMT-solvers. In 2014, Jan Gorzny, GSoC student in 2014, has started to generalise two of the proof compression algorithms (RecyclePivotsWithIntersection and LowerUnits) to first-order proofs generated by resolution-based first-order automated theorem provers (ATPs). Nevertheless, there are still many other proof compression algorithms that deserve to be generalised to the first-order case, and Jan's algorithms could still be improved in order to handle more proofs.

Skeptik’s data structures are already general enough to handle first- and even higher-order formulas. There are general abstract data structures for proofs, but they will have to be specialised (via inheritance) to deal with specific inference rules used by various ATPs. Furthermore, a parser for proofs generated by the automated theorem prover SPASS is already available, but it handles only simple proofs that do not use the SPASS's most sophisticated inference rules. Having a fully general parser for unrestricted SPASS proofs would be useful. a combinator parser for first-order proofs in the TPTP TSTP format [1] would be very nice to have as well, since it would allow us to import proofs generated by many other theorem provers (e.g. Schultz's E prover).

The generalisation of the compression algorithms to the first-order case will involve some scientific creativity and, therefore, this is not an easy project. A solid knowledge of logic, automated deduction and basic proof theory is required.

In the previous two years, Skeptik’s GSoC students have achieved great academic success and were able to publish and present their results in high-level conferences. We are committed to provide similar opportunities to this year’s GSoC students, and we are looking for students that are enthusiastic about these opportunities! If you are interested in this project idea, please contact us as soon as possible.

[1] TSTP is the proof format used by the TPTP library of automated deduction problems maintained by Geoff Sutcliffe at the University of Miami. Google it to know more!

[2] Papers about these algorithms can be downloaded from http://www.logic.at/people/bruno . Look for the IJCAR 2014 paper describing Skeptik. It provides a good starting point to learn more about Skeptik.

Benefit for the Student

The student will acquire practical experience and be in touch with cutting-edge research in the fields of automated deduction and applied proof theory. He will be mentioned as a co-author of any paper that might benefit from his implementation. He will have the pleasure of programming in the awesome language Scala.

Benefit for the Project

Skeptik’s application scope will be further extended from propositional to first-order logic.

Requirements

Solid knowledge of logic, automated deduction and basic proof theory is required. Knowledge of Scala or experience with other object-oriented (e.g. Java, C++,...) and functional (e.g. Haskell, OCaml,...) programming languages and willingness to learn Scala is required. Experience with data structures for proofs or directed acyclic graphs is highly desirable.

Mentors

Bruno Woltzenlogel Paleo, Ekaterina Lebedeva

More information

Instructions on how to improve your chances of getting accepted are listed on Skeptik's wiki.

SMT-proofs are composed of a propositional resolution proof in the bottom and "theory proofs" in the top. The simplest theory supported by SMT-solvers is the theory of equality with uninterpreted functions. Statements in the language of this theory can be decided modulo this theory using congruence closure algorithms. In 2014, Andreas Fellner (who was GSoC student in 2012) implemented the first algorithm aiming at compressing such congruence closure proofs. His algorithm was based on a variant of Dijkstra's shortest path algorithm applied to congruence graphs. However, due to the NP-completeness of this problem, this algorithm is not able to find the shortest congruence explanation.

This project idea aims at extending Andreas's algorithm in order to guarantee that minimally short explanations are found. To achieve this, we propose a brute-force approach, in which literals in the explanation to be shortened are incrementally removed while the explanation remains invalid. The choice of which literal to remove may be done heuristically and may influence the size of the minimally short explanation.

[1] To learn more, have a look at Andreas's MSc thesis.

Benefit for the Student

The student will acquire practical experience and be in touch with cutting-edge research in the fields of automated deduction and applied proof theory. He will be mentioned as a co-author of any paper that might benefit from his implementation. He will have the pleasure of programming in the awesome language Scala.

Benefit for the Project

Skeptik capability of compressing congruence closure proofs will be improved.

Requirements

Solid knowledge of logic, automated deduction and basic proof theory is required. Knowledge of Scala or experience with other object-oriented (e.g. Java, C++,...) and functional (e.g. Haskell, OCaml,...) programming languages and willingness to learn Scala is required. Experience with data structures for proofs or directed acyclic graphs is highly desirable.

Mentors

Bruno Woltzenlogel Paleo, Ekaterina Lebedeva

More information

Instructions on how to improve your chances of getting accepted are listed on Skeptik's wiki.