Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-08-19

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

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 andromeda-galaxy: 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 andromeda-galaxy ThreeOfEight: Sledgehammer will spit out proof terms that I have to manually copy into the source
17:01 andromeda-galaxy at proof-writing time, instead of at proof-checking 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 low-level 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 Sledghammer-related papers
18:28 andromeda-galaxy ThreeOfEight: okay, that makes sense.  Thanks for the explanation!
19:35 ThreeOfEight andromeda-galaxy: 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 sum-of-square 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 int-e https://www.isa-afp.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 int-e: 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 int-e thanks
22:25 chuchuco1ny ThreeOfEight: wait, I can update my afp entry (in stable, not in devel) by just flooding gerwin with patches?

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary