PostProcessor

Novelty: Removing Redundant Theorems

• Subsumption
• Easy proof
  • Test if Ax ∪ {T_i} |= T_k if leaf ancestors of T_k are a subset of those of T_i