2020-04-18 12:13:13 (GMT)
I have found one nasty performance bug in Zip concerning combining avatar and HO unif:
Both checking propositional satisfiability and generating HO unifiers is the same special kind of generating inference which is called when there are no passive clauses
2020-04-18 12:14:3 (GMT)
However, if getting clauses from HO unif is called before avatar then it might be possible we will never check propositional satisfiability
and loop while trying to get a unifier
2020-04-18 12:14:44 (GMT)
To fix this I have implemented:
2020-04-18 12:16:54 (GMT)
Which brings me to a following point: we might need to introduce such priorities to everything:
There are many places in the prover where it is important which inference is run first
2020-04-18 15:46:31 (GMT)
This sounds like satallax priority queues…
2020-04-18 16:9:14 (GMT)
Not qutie.
AFAIK, Satallax has, with each inference a priority attached and then it performs inferences with the lowest priority
What I am saying, is that we change nothing fundamental (such as given clause algo), but when you have say, two simplification rules applicable
to the clause you introduce a mechanism that is going to decide which is run first.