Matryoshka: Extending Superposition Provers and SMT Solvers to Higher-Order Logic

by Jasmin Christian Blanchette

Abstract
The Matryoshka project [*] aims at reducing the gap between the logics of automatic and interactive theorem provers. Our approach is to enrich the two leading approaches for first-order reasoning, namely superposition and SMT, with higher-order reasoning in a careful manner, to preserve their performance and any completeness guarantees. We initially focused on supporting currying (applied variables and partial application) and have now started investigating lambdas and higher-order unification, with promising results. Our techniques are implemented in the superposition-based provers Zipperposition and E and the SMT solvers veriT and CVC4.

Bio
Jasmin Christian Blanchette is an assistant professor in the Theoretical Computer Science section of the Vrije Universiteit Amsterdam, in the Netherlands. He is also a guest researcher in the VeriDis group at Loria in Nancy, France, and in the Automation of Logic group at the Max-Planck-Institut für Informatik in Saarbrücken, Germany. He was a postdoc at the Chair for Logic and Verification at the Technische Universität München, Germany, which he joined in 2008 as a PhD student. From 2000 to 2008, he worked as software engineer and documentation manager for Trolltech (now The Qt Company) in Oslo, Norway.
His research focuses on the use of first-order automatic theorem provers and model finders to find proofs and counterexamples in higher-order logic (Sledgehammer, Nitpick, Nunchaku, and Matryoshka). Another aspect of his work is the development of foundational definitional mechanisms for (co)datatypes and (co)recursive functions. He is also interested in formalizing classic results and modern research in automated reasoning (IsaFoL) and number theory (Lean Forward).

More information