AGInT Architecture

Macro Process

• Generate logical consequences from axioms and interesting theorems
• Double filtering to remove uninteresting consequences
• Rank the interesting theorems
• Postprocess with stored interesting theorems
• Store the surviving interesting theorems

Set-of-Support

• All formulae descend from SoS
• Axioms in first SoS
  Nothing else
• New interesting theorems in subsequent SoS's
  Axioms + old interesting theorems in non-SoS
• Produces focussed search deeper into search space