[metis-users] TPTP equalish predicate

[James Bridge]

Hi Joe,

Are you sure that it should be the way around that you have in your e-mail 
below?

I've found that I get much better results with using TermNet.match with 
deduceParamodulationInto and TermNet.matched with deduceParamodulationWith. 
In fact using matched with Paramod..Into caused the prover to give up on 
the sample problems I was trying whilst using match with the Paramod..With 
still worked but was much slower than using matched with Paramod..With.

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
>