2020-06-12 16:5:40 (GMT)
Back in March 2019, there were some very promising results with HO veriT. Then I went through my lost weekend, and one year later I realize that the code is still in a separate branch and that proof output does not work yet. I hope these are things on the radar for the next 12 months or so? On the Isabelle side, together with Martin D., I'd love to integrate HO veriT and deploy it, before the end of Matryoshka.
2020-06-12 16:56:59 (GMT)
@Hans-Jörg do you need new proof rules for HO proofs or is it basically the same, you just have to do an ugly merge?
2020-06-12 17:9:22 (GMT)
From what Hans-Jörg told me, he needs more than a merge.
2020-06-12 17:22:27 (GMT)
I believe the code that Daniel wrote is not proof producing
2020-06-12 17:22:40 (GMT)
the calculus is the same modulo currying
2020-06-12 17:23:26 (GMT)
Daniel did not implement extensionality as part of the ground procedure. It's handled via instantiation
2020-06-29 11:4:21 (GMT)
Sorry to come up later on this topic. Regarding the proof format, I think, it's necessary to implement what is described in the PxTP paper: Language and proofs for higher-order SMT (work in progress). That means, provide support for curried terms. Concerning UF I need to make the congruence closure proof-producing. For the other theories, I think it could be enough to make the output in curried form afterward (just need to modify the pretty-printer). Maybe other solutions could be considered since only UF is performing HO reasoning. For instance, we could introduce a special lemma bridging curried and non-curried terms. But it looks really tricky.
However, Sledgehammer doesn't need proof,, isn't it? I can make available a clean version of the "HO" veriT, but a simple merge is not really possible. I think we should use the HO branch as it is, and only merge update from devel, of preprocessing or arithmetic, independently.
2020-06-29 11:9:35 (GMT)
Right, I do handle extensionality by instantiation, which is not too bad for proofs. Nothing special is required.
2020-06-29 11:10:8 (GMT)
Sledgehammer does not, but it would be great to reconstruct HO proofs. The proof-reconstructed methods are also among the methods that Sledgehammer can suggest. So Sledgehammer would also profit.
2020-06-29 11:10:27 (GMT)
And Sledgehammer works better with proofs.
2020-06-29 11:18:0 (GMT)
I see, then we need to discuss how to integrate what you've done @Hans-Jörg , with the HO branch. It's going to take some time and organization....
2020-06-29 11:22:3 (GMT)
Yeah
2020-06-29 11:54:41 (GMT)
To clarify Mathias's claim, see the paper https://www.cs.vu.nl/~jbe248/isar.pdf .
2020-06-29 11:55:38 (GMT)
I think one issue with the HO branch was also that it is more prototypical, and would need some cleanup before Pascal is comfortable with having it in the main branch. Is that right?
2020-06-29 12:18:43 (GMT)
Yes, that was the first point, but now this branch is too far away from the main branch to be merged... We should defenitly discuss the futur of this branch at the next matryoshka meeting...