PV2 TheSy: Theory Synthesis, pronounced Tessydiscovers lemmas based on data types and recursive definitions

Application domain/field

Type of tool

Meta-tool? Synthesis tool?

Expected input

Base set of inductive data types and recursive definitions


Own format (.th files) or SMT-LIB v2.6, based on uninterpreted function theory, limited to universal quantifications

Expected output

Library of lemmas


TheSy focuses on discovering lemmas. Lemmas are often used in verification tools such as Dafny, Coq and Isabelle/HOL to state background knowledge. It's technique is based on syntax-guided enumerative synthesis.


License: GPL v3.0


Repository: https://github.com/eytans/TheSy

Related papers

Theory Exploration Powered by Deductive Synthesis (CAV '21)

Last publication date

15 July 2021

Related tools

ProVerB specific

Markdown description: view/edit

ProVerB is a part of SLEBoK. Last updated: February 2023.