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

Format:

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

Expected output

Library of lemmas

Internals

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.

Comments

License: GPL v3.0
Synthesis

Links

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.