AGInT - Automatic Generation of Interesting Theorems
Logical Consequence Generation
- Input a satisfiable set of axioms
- ATP generates LCs according to the SoS strategy
- Pre-processor cleans them up
Adaptive 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
Static Ranker and Post-processor
- Values from the Runtime Filter are normalized and propagated, and
- Usefulness measures proportion of interesting children
- Post-processor removes subsumed and redundant theorems
- Loop to reseed the SoS
Results