RedAx

Principle

• Approaches to proving hard theorems
• There are often unnecessary axioms in problems in rich theories

Architecture

• Repeatedly
  • Remove some axioms to form an axiom reduced problem
  • Submit the result to ATP
• Brute force and ignorance - Combinatorial removal

Performance

• Results from TPTP FOF problems, 3600s limit, 60s per axiom reduced problem

  	60 SPASS unsolved problems			73 problems rated 1.00
  	SPASS 2.0	RedAx		Vampire 5.0	RedAx
  Solved	7	14		0	4