[metis-users] TPTP equalish predicate

[James Bridge]

Thanks. Also thank you for the warning re match and matched - an easy one 
to miss.

James

On Nov 21 2011, Joe Hurd wrote:

>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
>