2020-04-13 12:34:42 (GMT)
Dear all,
I have been working with Ahmed on various heuristics that try to take the best out of combinator/lambda calculi and I was wondering if anyone is aware of any work that uses non-syntactic criteria to select clauses (@Stephan Schulz I am hoping you are aware of something like this).
My idea is to introduce a counter in clause object that is going to count how many times that clause subsumed/simplified other clauses.
One possible clause weight function that can use this information is the one that would sum those values for proof parents of clauses and
select the one that has the maximal value. Intuition is that a clause that obsoletes other ones is somehow more useful
2020-04-13 14:8:33 (GMT)
So far, in E there are priority functions that use the derivation depth. Using subsumption or simplification counts is not useful (for a single run) in the context of the DISCOUNT loop, since by definition (for most settings) only clauses there have already been picked are used for simplification.
DISCOUNT itself used such heuristics (simplification counts) to determine which clauses to pass on into the global proof state in the team meetings if it ran in its distributed mode.
Also, something similar can be used with learning heuristics and watchlists. I may have experimented with these in the distant and forgotten past, but not to very exciting results.
2020-04-13 14:12:47 (GMT)
So far, in E there are priority functions that use the derivation depth. Using subsumption or simplification counts is not useful (for a single run) in the context of the DISCOUNT loop, since by definition (for most settings) only clauses there have already been picked are used for simplification.
Thank you for your answer. But if in the passive set, we have clauses whose parents were used to simplify a lot of clauses, maybe we want to prefer them?
2020-04-13 14:30:42 (GMT)
That is certainly an option. For simplicity's sake, its probably best to determine this at the time the clause was created (so that we don't need to reweight clauses all the time).
2020-04-13 14:36:32 (GMT)
that is what I thought
Thanks
2020-04-13 14:37:7 (GMT)
I am reading Jan and yours' CICM 2016 paper
to get some inspiration (i.e. shamefull copy) on what to implement in Zip
2020-04-13 14:37:53 (GMT)
I have a CICM 2016 paper? Those Prague guys are too busy ;-)
2020-04-13 14:38:47 (GMT)
We do have a 2018 ITP paper (that we could not submit to IJCAR because I was a program chair).
2020-04-13 14:39:48 (GMT)
is it also about heuristics?
2020-04-13 14:44:32 (GMT)
About watch lists, yes.
2020-04-13 14:45:21 (GMT)
ProofWatch: Watchlist guidance for large theories in E
Z Goertzel, J Jakubův, S Schulz, J Urban
International Conference on Interactive Theorem Proving, 270-288
2020-04-13 14:46:33 (GMT)
Ok. Thanks
2020-04-13 14:48:7 (GMT)
Did you mean "Extending E prover with similarity based clause selection strategies"?
That is CICM 2016, but I'm not on it (that I know of ;-)
2020-04-13 14:50:3 (GMT)
Yes, that is what I meant.
Now I checked again and I mistaken Joseph Urban for Stephan Schulz (I have no idea how :slight_smile:
2020-04-13 14:51:37 (GMT)
We are nearly the same body shape!
2020-04-13 14:55:46 (GMT)
Or it is that all this wine I have been drinking since the corona outbreak is taking its toll :slight_smile:
2020-04-13 15:16:39 (GMT)
Aaaahh.. now I see how I mixed it up
In the source code it says:
Author: Stephan Schulz, yan
2020-04-15 9:8:59 (GMT)
Yes, I possibly helped with the code. Or Jan borrowed something. I'm too helpful ;-)