TPTP arithmetic adds $abs

[Geoff Sutcliffe]

Hi everyone,

I have quietly, but with approval of the Vampires who are the only real players in TFA, added $abs to the list of TPTP arithmetic functions ...

    https://tptp.org/UserDocs/TPTPLanguage/TPTPLanguage.shtml#ArithmeticSystem

Here's a little problem I added to the ARI domain of the problem library ...

tff(prove_abs,conjecture,
    ( ( $abs(-3) = 3 )
    & ! [I: $int] : ( $abs($abs(I)) = $abs(I) ) ) ).

Cheers,

Geoff

[Stephan Schulz]

Hi Geoff,

I like it. It looks like a useful small addition that also is
good as a first test for an implementation design.

Bye,

Stephan

> --
> You received this message because you are subscribed to the Google Groups "TPTP World" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tptp-world+...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/tptp-world/5a1302c9-6c8f-44f1-a77f-565e5043bf1bn%40googlegroups.com.

--
------------------------------ It can be done! ---------------------------------
Please email me as sch...@eprover.org (Stephan Schulz)
--------------------------------------------------------------------------------