2020-07-14 19:41:41 (GMT)
Petar and I started playing with Zip on a handful of hand-crafted Isabelle problems, and things look very promising. It's very exciting. But this also revealed that Zip's proof output needs more work: outputting HO terms in FO syntax isn't something Isabelle can parse right now...
2020-07-14 19:43:10 (GMT)
May I boldly suggest to use some sort of S-expressions based format? :)
It'd be much easier to parse. I believe the wonderful land of SMT and veriT proofs could benefit too :)
2020-07-14 20:53:50 (GMT)
If you can convince the authors of 15+ ATPs to move from TSTP to S-expressions overnight, I'm in. Otherwise, my view is and remains that Zipperposition should output legal TSTP.
2020-07-14 20:57:48 (GMT)
You're right, of course. TSTP is pretty entrenched.
2020-07-14 21:20:28 (GMT)
If I may ask, is this to integrate Zipperposition into Sledghammer or to do an independent checker for Zipperposition (TSTP?) proofs?
2020-07-14 22:12:0 (GMT)
I think it's for integrating Zipperposition into Sledgehammer. Having an independent proof checker is not as high on @Jasmin Blanchette 's priority list :)
2020-07-14 22:17:40 (GMT)
It's very high on my list: Isabelle is an independent checker. ;)
2020-07-14 22:18:26 (GMT)
Anyway, I'd rather have a slightly unsound prover find proofs for hundreds of Isabelle users than a perfectly sound prover that's used by nobody.
2020-07-14 22:25:24 (GMT)
I think the distinction here is between a "full" checker (i.e. it succeeds iff the proof is valid), and a proof reconstruction tool like Isabelle (which might fail to reconstruct a proof even if it's valid).
I don't mean to criticize SH, of course. It's super nice that Zipperposition is going to be used! But I personally also want a (lightweight?) proof checker for development or just for running Zipperposition standalone. The two are not exclusive :slight_smile:
2020-07-14 22:26:45 (GMT)
Of course. I appreciate the distinction between an ad hoc checker and a full checker, between one that comes with 500 GB of stuff and one that doesn't, etc.
2020-07-15 22:13:57 (GMT)
On the new isabelle friendly branch, running:
./zipperposition.exe examples/pelletier_problems/pb34.p -o tstp
gives an invalid TSTP trace, btw. (zf_stmt_2 for example has free variables in a tff block).
The same command on master properly re-quantifies the formulas…
2020-07-15 22:19:1 (GMT)
That branch was only a very temporary thing. I think it's raison d'etre is over. Right, Petar?
2020-07-15 22:21:17 (GMT)
It could also be the case on combinators and more recent branches :)
2020-07-19 15:31:40 (GMT)
I will take a look into this