AGInT - Automatic Generation of Interesting Theorems
LC Generation
- Input a satisfiable set of axioms
- Axioms, then theorems, used in SoS
- E generates LCs according to the SoS strategy
- PreProcessor cleans them up
Runtime Filter
- Obviousness measures derivation size
- Weight measures number of symbols
- Complexity measures number of different symbols
- Surprisingness measures unexpected co-occurences of symbols
- Intensity measures information summary
- Adaptivity measures variable constraints
- Focus measures polarity of atoms
- Adaptive controllers use windows to determine suitable thresholds
Static Ranker
- Values from the Runtime Filter are normalized and propagated, and
- Usefulness measures proportion of interesting children
PostProcessor
- Removes subsumed and redundant theorems
Results