2020-01-14 16:22:59 (GMT)
Question for Zip experts: Does Zipperposition support orphan deletion (cf. Brainiac paper, "orphan-criterion")?
2020-01-14 16:23:10 (GMT)
And I presume the main loop is a DISCOUNT loop, like E?
2020-01-14 16:23:24 (GMT)
It used to, but I removed it a while ago, it was buggy.
The main loop is indeed DISCOUNT.
2020-01-14 16:23:36 (GMT)
It's not fast enough to afford an Otter loop :joy:
2020-01-14 16:29:2 (GMT)
To elaborate on the orphan rule: there used to be that based on the proof objects (parents would be "a clause reachable from the current clause throught exactly one inference"). It was sometimes a bit slow and I must have got something wrong cause it barely ever pruned anything.
2020-01-14 16:30:37 (GMT)
OK. I'll still capture orphan deletions then in my abstract loop (but phrase thing so as not to imply that Zip implements orphan del).
2020-01-15 9:2:16 (GMT)
I can reinvestigate the orphans since from what I know from Stephan it works quite nice
in E.
2020-01-26 22:58:25 (GMT)
BTW see our "Zipperposition loop" description (including orphans) in
http://matryoshka.gforge.inria.fr/pubs/satur_paper.pdf http://matryoshka.gforge.inria.fr/pubs/satur_report.pdf
2020-01-27 2:4:55 (GMT)
This could go into the IsaFoL stream :)
2020-01-27 2:6:10 (GMT)
Does this paper mean that, once you get to extract a verified superposition prover, it could be able to imitate Zipperposition?
2020-01-27 8:32:49 (GMT)
This could also go in the "Saturation framework" substream of "Matryoshka". ;)
2020-01-27 8:35:27 (GMT)
The Zip loop isn't formalized yet, but in principle it means given a refutation calculus that has rules with countably infinitely many conclusions (e.g. superposition with HO unif), you can derive (on paper) an abstract Zipperposition prover as a transition system and some conditions on the strategy to achieve fairness. Then an extra step of refinement (like Schlichtkrull et al. CPP 2019 did for the resolution prover RP) gives you a functional program.