AGInT

• A system for automatic generation of interesting theorems
• ATP generates LCs according to the SoS strategy
• Rating components select interesting LCs
• Loops to reseed the SoS

• Rating component used to analyse completed derivations

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 Rater

• Measures from the Runtime Filter are normalized
• Usefulness measures proportion of interesting children
• All measures are combined and renormalized