[metis-users] TPTP equalish predicate

[Joe Hurd]

Hi James,

I was just using == as a convenient infix notation for equalish, to
make things more readable when I was developing Metis. You could go
ahead and remove the ==/equalish binding from

Tptp.defaultRelationMapping

and use == for your own purposes. However, you should be aware that
Metis treats the symbol = specially, and if you use another symbol to
represent equality you might miss out on some equality processing
(such as scanning for irreflexivities to remove when factoring).

Cheers,

Joe

On Mon, Nov 21, 2011 at 2:12 AM, James Bridge <jpb65 at cam.ac.uk> wrote:
> Hi Joe,
>
> At present in Metis the symbol '==' is translated into the TPTP predicate
> 'equalish' (equality without axioms such as transitivity being automatically
> assumed).
>
> Geoff Sutcliffe seemed slightly puzzled when, in an e-mail asking about the
> use of '==' and 'equalish' in TPTP, we equated the '==' with 'equalish'
> having assumed that this was standard TPTP notation.
>
> Is the use of '==' for 'equalish' something that was only introduced in
> Metis or is it used by other provers as well?
>
> The reason for the question is that it would be very handy for us to use
> '==' in place of '=' to indicate demodulation should be used rather than
> paramodulation but we want to know what the side effects of doing so would
> be.
>
> James
>
>