TPTP Syntax for Assumptions

Assumptions

• Unproved proposition introduced (assumed to be true) locally in proof
  (supposition in Jaskowski's terminology)
• Coupled with a discharge (elimination) rule, making the reasoning result unconditionally true
• Common example is proof by contradiction:
  assume negation, deduce contradiction, conclude theorem

TPTP Syntax

• formula role assumption
• assumptions([...]) list for recording assumptions
• discharge list of discharged assumptions

Example

fof(e1,assumption, subset(c1,c2), introduced(assumption)). 

fof(i3,plain, c2 = set_union2(c1,set_diff(c2,c1)), 
  inference(conclusion,[status(thm),assumptions([dt_c1,e1])],[e3,i4])). 

fof(i2,plain, (subset(c1,c2) => c2 = set_union2(c1,set_diff(c2,c1)), 
  inference(discharge_asm,[status(thm),assumptions([dt_c1]), 
    discharge_asm(discharge,[e1])], [e1,i3])).