[metis-users] TPTP equalish predicate

[Joe Hurd]

Hi James,

> By the way, thanks for your earlier suggested mod of changing Subt.unify to
> Subt.match which works well. I did notice that the calling routines
> Active.deduceParamodulationWith and Active.deduceParamodulationInto call
> TermNet.unify, presumably it would be a bit more efficient to change these
> to TermNet.match as well?

Yes indeed, although take care to use TermNet.match for
deduceParamodulationWith and TermNet.matched for
deduceParamodulationInto to respect the substitution ordering. The
purpose of these calls is to narrow down the possible paramodulations,
so nothing would go wrong by leaving it as unify, but match and
matched are both faster and result in a smaller set for paramodulate
to check.

Cheers,

Joe