Imperfect Filtering about vampire HOT 8 OPEN

I am very much in favour of this. Both imperfect indexing and unification (or maybe some unification-like thing - UWA?) can be implemented very efficiently and concisely, but perfect indexing is much trickier. I'm also not convinced that perfect indexing pays off.

It would be interesting to try replacing these with fewer indices that contain more terms each. Inferences then share indices and carry out post-procesing to filter out unwanted terms.

Could you expand on this a little? Maybe an example? I think there's two separate things to try here:

1. imperfect indexing techniques like discrimination trees
2. coalescing multiple indices into one and filtering out unwanted items

I think both are worth exploring, to be clear.

from vampire.

Do we know of some papers evaluating indexing techniques in the past? Let's avoid common pitfalls and not try to reinvent the wheel ;)

from vampire.

I am not suggesting abandoning substitution trees. The suggestion is to combine similar indices (your #2). For example, instead of having a substitution tree that indexes only left-hand sides for demodulation, and another that indexes only left-hand sides for superposition, we have a tree that contains both sets of terms.

When performing a query on the index from demodulation, we may receive extra left-hand sides (those suitable for superposition, not demodulation) which will then need filtering out.

Looking into discrimination trees and other techniques is also interesting, but an even more radical departure from the current code base.

from vampire.

The suggestion, is to combine similar indices (your #2). For example, instead of having a substitution tree that indexes only left-hand sides for demodulation, and another that indexes only left-hand sides for superposition, we have a tree that contains both sets of terms.

I see. This seems like a good idea. My only concern is that the performance win from combining indices (mostly spatial locality and reduced index maintenance, right?) will be lost by increased query time resulting a larger index. But it's worth a try!

from vampire.

Do we know of some papers evaluating indexing techniques in the past? Let's avoid common pitfalls and not try to reinvent the wheel ;)

Here are a couple:

https://www.sciencedirect.com/science/articl/pii/B978044450813350028X?via%3Dihub
https://link.springer.com/content/pdf/10.1007/3-540-45744-5_18.pdf

from vampire.

And of course:
https://people.mpi-inf.mpg.de/~hillen/compit/evaluation.pdf

from vampire.

from vampire.

from vampire.