Ticket #222 (closed task: wontfix)

Opened 3 years ago

Last modified 2 weeks ago

use local links induced by %implies for subsumption proofs

Reported by: till Owned by: maeder
Priority: major Milestone: 0.95
Component: development-graph Version: 0.66
Keywords: Cc:

Description

In Proofs.Automatic, adjust the order of dg rule application: try to use local links induced by %implies for subsumption proofs (such that the %implied formulas need not be re-proved)

Change History

Changed 3 years ago by till

  • owner changed from till to ken
  • milestone changed from 0.7 to 0.75

Changed 21 months ago by till

  • owner changed from ken to maeder

Changed 2 weeks ago by maeder

  • status changed from new to closed
  • resolution set to wontfix

I don't see a need for this. Links induced by %implies go backwards. Re-open this ticket if you have an example.

Note: See TracTickets for help on using tickets.