3 ms·
One area I've been playing with is "theory exploration", which takes a set of definitions and produces lemmas that are 'interesting' (i.e. irreducible, via some
by chriswarbo 5y ago
One area I've been playing with is "theory exploration", which takes a set of definitions and produces lemmas that are 'interesting' (i.e. irreducible, via some scheme like Knuth-Bendix rewriting).
(Thanks to Curry-Howard, we can also view this as generating test suites/specifications for software libraries!)
Notable tools include Hipster, IsaScheme, IsaCoSy, QuickSpec and Speculate.