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

Application domain/field

• Theorem generation
• Deductive inference
• Theory exploration
• Theory synthesis
• Lemma discovery

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