2020-03-17 19:7:42 (GMT)
I have just read the paper about lazy clausification (https://www.sciencedirect.com/science/article/pii/S0890540105000258?via%3Dihub) and it is really really nice (like anything else from Ganzinger)
2020-03-17 19:8:38 (GMT)
I was always complaining how we need something like that in HO setting and I will implement this rule during the rest of the week, and if there are any interesting conclusions let you know
2020-03-17 19:9:11 (GMT)
@Alex Bentkamp this might be also interesting for you, because before you start working on HO superpositon, you might have a picture of what works and what does not work
2020-03-17 19:10:41 (GMT)
@Alexander Bentkamp . In their paper, they use the order that makes de Bruin indices the largest symbols in the precedence
2020-03-17 19:12:13 (GMT)
Will this work with your calculus?
2020-03-17 19:58:15 (GMT)
This is definitely one of the tougher questions that we have to solve. Of course we can make the De Bruin indices the largest symbols, but I don't know if that will be enough. The problem is that in HOL, we can instantiate a for-all quantifier with something that contains even more De Bruin indices, which will make it larger than a single De Bruin index...
2020-03-17 20:3:39 (GMT)
OK, I see. Well, I will implement the approach since I am very curious how it will work and let you know what my experiences are :)
2020-03-17 20:4:5 (GMT)
One huuuge difference that is going to be in my implementation is that few days ago I reverted back to != T presentation of literals
2020-03-17 20:4:48 (GMT)
this means that unlike in Ganziger's paper negative ocurrences of equalities and equivalences will be represented with a negative sign
2020-03-17 20:41:0 (GMT)
If you can do renaming/sharing of skolems with this paper I think the results might be very good. Long ago in Zipperposition there was a more naive version of that that wasn't very good on some problems because the CNF was sometimes exponential in size.
2020-03-17 20:47:15 (GMT)
Yeah, I will include renaming with sharing of definitions
2020-03-17 21:37:5 (GMT)
Why did you revert to != T ?
I found it very interesting that Ganzinger & Stuber do not have disequations at all. They represent s != t as (s = t) = false.
2020-03-18 9:9:17 (GMT)
We got better performace when we reverted back to != t
2020-03-18 11:23:40 (GMT)
Is this change isolated in a single commit? We should remember what to change if we want to change it again :-)
2020-03-18 12:4:23 (GMT)
Oh no :(
2020-03-18 12:4:39 (GMT)
Next time we change it (it is going to happen sooner or later, I will do it in a modular fashion)