Stream: Machine learning and automation

Topic: Learning new tactics and refactoring existing tactics

view this post on Zulip Patrick Nicodemus (Apr 02 2023 at 23:58):

In machine learning, there is a notion of "inductive bias" where the structure of the permitted or assumed form of the solution has a huge effect on how easy/hard the pattern is to recognize. You want your space of functions or hypotheses to be as small as possible, but not so small that you exclude the desired solution.
In theorem proving and proof search, I think this means trying to configure your arsenal of tactics in a way that's most equipped for the class of problems you want to solve.

How do we appropriately choose a basic set of tactics so they are most adequate for solving our problems?

Two more specific questions in this vein:

Last updated: Jun 18 2024 at 00:02 UTC