search

spechub / Hets

The Heterogeneous Tool Set
http://hets.eu
GNU General Public License v2.0
57 stars 19 forks source link

Support "axiom list minimization" workflow more smoothly #1110

Open sternk opened 10 years ago

sternk commented 10 years ago

Reported by clange and assigned to ldiaconu Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/1110

I found that some provers (at least darwin and eprover) frequently report that they have used all axioms in my theory to prove some goal, whereas much fewer axioms should actually be needed, and SPASS does report using fewer axioms. Now, being interested in what axioms were really used, I manually ran the following workflow:

  1. run a proof while "Prove→Axioms to include" is set to "all"
  2. in the list of "Used Axioms" reported by the prover, find out axioms that should not be necessary for proving the goal
  3. back in the "Prove" window, deselect these axioms from the list of axioms to include (BTW see #1099 for another bug related to this)
  4. run "Prove" again This workflow could be facilitated if the list of "Used Axioms" somehow directly interfaced with the list of "Axioms to include", so that deleting/unselecting/whatever an axiom from "Used Axioms" would remove it from "Axioms to include", and you could leave the prover-specific window open for immediately trying the next proof attempt with fewer axioms. (Finally, an automation of this whole minimization workflow would also be nice of course; I think Isabelle's Sledgehammer can do this at least in combination with E.)
sternk commented 10 years ago

Comment by till Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/1110#comment:2

I think this workflow could be automated also (and maybe easier) for the CMDL interface. Hets would read in a whole script, process it, and output a modified script where the axioms used in proofs have been turned into "set axioms" statements. (This could even be added on top of Hets, using some scripting language.)