2020-05-08 8:37:14 (GMT)
No answer from Michael. Let's meet next week.
2020-05-14 12:15:18 (GMT)
So, the last time I created a zoom meeting for the bookclub, but since @Michael Färber mentioned it is banned in some places, should I create a jitsi?
2020-05-14 12:17:15 (GMT)
People commented that we could try jitsi for today.
2020-05-14 12:20:59 (GMT)
Here it is: https://jitsi.mpi-klsb.mpg.de/bookclub4_brown_reducing_ho_to_sat .
See you soon!
2020-05-14 14:7:57 (GMT)
Is the HO unification algorithm in Satallax Huet's preunification? If so, what do they do with the Flex-flex pairs that remain? Maybe they also have full unification like we have in Zipperposition?
2020-05-14 15:32:5 (GMT)
Alexander Bentkamp said:
Is the HO unification algorithm in Satallax Huet's preunification? If so, what do they do with the Flex-flex pairs that remain? Maybe they also have full unification like we have in Zipperposition?
I read somewhere it is huet
2020-05-14 15:55:38 (GMT)
Maybe they keep the flex-flex pairs around as "constraints" -- like Isabelle does. If instantiation leads them to become non flex-flex, then they can be Huetted further.
2020-05-18 9:57:59 (GMT)
Hello there, sorry I could not join last Thursday. I had a teleconference the same day, and my internet connection was so amazingly bad that I even had to abort the conference. :(