Laura Kovács is a full professor of computer science at the TU Wien, leading the automated program reasoning (APRe) group of the Formal Methods in Systems Engineering division. Her research focuses on the design and development of new theories, technologies, and tools for program analysis, with a particular focus on automated assertion generation, symbolic summation, computer algebra, and automated theorem proving. She is the co-developer of the Vampire theorem prover and a Wallenberg Academy Fellow of Sweden. Her research has also been awarded with four ERC grants and two Amazon Research Awards. Recently, she received financial support from LEA Frauenfonds to disseminate unplugged computer science to elementary schools, while organising computer science workshops with school children at the TU Wien. Starting with May 2025, she is the president and steering committee chair of the ETAPS association, running the ETAPS conferences.
Title: SAT in Saturation: A Satisfied Match
Abstract: Saturation is the leading concept behind the proof-search algorithms of state-of-the-art first-order theorem provers. The key idea behind saturation-based proof search is to reduce the problem of proving validity of a first-order formula to the problem of establishing unsatisfiability of the respective formula, by using a sound inference system, such as superposition. Central to efficient saturation-based proof search is the implementation of redundancy in the form of simplification rules: such rules do not add new formulas to search space, but instead simplify/delete (redundant) formulas from the search space, while not loosing refutational completeness of superposition.
Subsumption is one of the most important simplification rules in automated reasoners, ranging from SAT solvers to first-order theorem provers and beyond. It is common that millions of subsumption checks are performed during a single solver run, necessitating efficient implementations. However, in contrast to propositional subsumption as used by SAT solvers and implemented using sophisticated polynomial algorithms, first-order subsumption in first-order theorem proving involves NP-complete search queries, turning the efficient use of first-order subsumption into a huge practical burden.
This talks shows a tailored integration of SAT solving for solving variants of subsumption in superposition. Key to our approach is retrieving clauses from the search space and checking whether subsumption with retrieved clauses can be applied, using multi-literal-matching. Our experimental results using the Vampire prover demonstrate the practical benefits of using SAT solving for variants of first-order subsumption.