2020-04-20 12:55:44 (GMT)
We will have an "official" discussion about AVATAR then, as the previous seminar already had like 15min of it :)
2020-04-20 13:52:44 (GMT)
Jasmin Blanchette said:
It's past noon (Paris time)
this is discriminatory to the ones among us who lives west! :stuck_out_tongue:
2020-04-20 13:55:40 (GMT)
we're the minority and should accept the domination of our oppressors
2020-04-21 16:48:43 (GMT)
Regarding recognition of Church numeral problems: Satallax does specially treat Church numerals, but AFAIK only for printing terms. :)
2020-04-21 16:49:56 (GMT)
Jasmin Blanchette said:
I am very skeptical here. Consider that Satallax uses a superposition prover, E, as a backend, that it was recently still beaten by Isabelle/Sledgehammer at the competition (except that Isabelle didn't produce proofs, a requirement) [1], that it performs rather poorly (and worse than Zipperposition) on Sledgehammer-generated benchmarks, and that it was highly optimized for the TPTP (including recognition of Church numeral problems, from what I'm told -- instead of relying on HO unification). Satallax's days are counted, I promise you. ;) It's still surprisingly good, though.
Regarding recognition of Church numeral problems: Satallax does specially treat Church numerals, but AFAIK only for printing terms. :)
2020-04-21 16:55:32 (GMT)
Petar Vukmirovic said:
Michael Färber might also be interested in enlightening us on Satallax :)
If you are interested in why Satallax performs well in CASC, then my personal guess is that it is the immense number of flags and of modes that combine these flags in order to obtain good performance on CASC. Furthermore, Satallax profits from development of the tools it uses; for example, when a wizard like Petar implements lambda-free higher-order logic in E, then Satallax can profit from this almost immediately. :) This also clearly shows in the CASC results.
2020-04-30 11:23:18 (GMT)
Here is a Zoom invitation for this afternoon's bookclub:
Topic: bookclub on AVATAR
Time: Apr 30, 2020 03:00 PM Amsterdam, Berlin, Rome, Stockholm, Vienna
Join Zoom Meeting
https://zoom.us/j/95363307001?pwd=V1hwaEpXWWh4SnpzbEhRUEFtTjArUT09
Meeting ID: 953 6330 7001
Password: 850969
One tap mobile
+496971049922,,95363307001# Germany
+493056795800,,95363307001# Germany
Dial by your location
+49 69 7104 9922 Germany
+49 30 5679 5800 Germany
+49 695 050 2596 Germany
+1 669 900 9128 US (San Jose)
+1 253 215 8782 US (Tacoma)
+1 301 715 8592 US (Germantown)
+1 312 626 6799 US (Chicago)
+1 346 248 7799 US (Houston)
+1 646 558 8656 US (New York)
Meeting ID: 953 6330 7001
Find your local number: https://zoom.us/u/aeF1Ynf9Le
2020-04-30 12:58:3 (GMT)
I might be a minute or two too late, my neighbor has no electricity and we are trobuleshooting :slight_smile:
2020-04-30 13:0:11 (GMT)
oh, it's earlier today, had forgotten