Time 
Nick 
Message 
01:48 

ilbot3 joined #isabelle 
01:48 

Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html  Now with logging: http://irclog.perlgeek.de/isabelle/ 
06:07 
ThreeOfEight 
andromedagalaxy: What do you mean by that? 
06:07 
ThreeOfEight 
"proofs to add manually"? 
10:39 

silver joined #isabelle 
14:34 

dmiles joined #isabelle 
17:01 
andromedagalaxy 
ThreeOfEight: Sledgehammer will spit out proof terms that I have to manually copy into the source 
17:01 
andromedagalaxy 
at proofwriting time, instead of at proofchecking time (when SMT does) 
18:13 
ThreeOfEight 
Yes. 
18:14 
ThreeOfEight 
Sledgehammer works in a totally different way than Isabelle's proof methods. 
18:15 
ThreeOfEight 
In particular, it sends the proof obligation to web servers over the internet and calls local solvers that may take a long time to find a proof 
18:15 
ThreeOfEight 
(or take a long time and then just give up) 
18:15 
ThreeOfEight 
you could, in theory, do something like this in an Isabelle proof method (you can run arbitrary code there), but it is discouraged to say the least 
18:15 
ThreeOfEight 
you want proof methods to be predictable in their actions 
18:16 
ThreeOfEight 
"smt" itself pretty much only does the translation and calls Z3 and then translates that into a proof that is passed to the Isabelle kernel 
18:17 
ThreeOfEight 
In particular, smt does not have any repertoire of facts to use; you have to explicitly give it all the facts that it should use 
18:17 
ThreeOfEight 
(by the way, these are not "proof terms"; proof terms are much more lowlevel and huge) 
18:17 
ThreeOfEight 
(it's more like a "proof script", or "method invocation") 
18:20 
ThreeOfEight 
cf. also http://isabelle.in.tum.de/dist/doc/sledgehammer.pdf 
18:21 
ThreeOfEight 
also a number of Sledghammerrelated papers 
18:28 
andromedagalaxy 
ThreeOfEight: okay, that makes sense. Thanks for the explanation! 
19:35 
ThreeOfEight 
andromedagalaxy: for the sake of completeness, there is a proof method called "sos" 
19:36 
ThreeOfEight 
it proves inequalities on polynomials by decomposing them into a sum of squares 
19:36 
ThreeOfEight 
(if you have an equation of the form p(x,y,z) >= 0 and you can decompose p into a sum of squares of polynomials, that's a proof) 
19:36 
ThreeOfEight 
*an inequality 
19:36 
ThreeOfEight 
(for univariate polynomial, this procedure is, in theory, even complete) 
19:37 
ThreeOfEight 
Finding those sumofsquare witnesses is, however, very difficult, so it sends the proof obligation to an online service to do it (and possibly a local solver) 
19:37 
ThreeOfEight 
finding the witness can take minutes or even hours 
19:37 
ThreeOfEight 
and once it has found one, it will complete the proof 
19:38 
ThreeOfEight 
however, it will also output a line saying something like "you can replace this invocation with 'apply (sos_cert …)', where "…" is the witness that it has found 
19:39 
ThreeOfEight 
sledgehammer is kind of a similar idea, but instead of giving you the option of inserting the proof that it found directly and avoiding having to do the work again, it /forces/ you to do that 
19:39 
ThreeOfEight 
That's a design choice; one reason for it may be that sledgehammer may find several proofs and it is not clear which of them you want 
19:39 
ThreeOfEight 
(or it may find proofs that are so slow/convoluted that you deem all of them inacceptable) 
20:46 
inte 
https://www.isaafp.org/updating.shtml is not quite clear about how one should update one's own AFP entry. Does one need to ask for write access to the repo, or are there other ways? 
21:08 
ThreeOfEight 
inte: you can just submit a patch to anyone with push rights 
21:08 
ThreeOfEight 
(like me) 
21:08 
ThreeOfEight 
but you can also ask Gerwin Klein for push access, I suppose 
21:09 
ThreeOfEight 
actually, if you do send a patch somewhere and your entry is not thematically closely related to some person with push access, sending it to Gerwin Klein is probably the best idea 
21:09 
ThreeOfEight 
or you can ask on the mailing list 
21:19 
inte 
thanks 
22:25 
chuchuco1ny 
ThreeOfEight: wait, I can update my afp entry (in stable, not in devel) by just flooding gerwin with patches? 