$distinct and $universe

[Geoff Sutcliffe]

Hi all,

For a long time TPTP language has had $distinct, and at least 2 ATP systems have implemented it. For those who have not used it, it's the Unique Names Assumption, e.g....

    $distinct(agatha,butler,charles)

... is equivalent to ...

    (agatha != butler & agatha != charles & butler != charles)

$distinct is very useful in applications.

The flip side of the coin is a Closed World Assumption, and I'm considering adding that to the TPTP language, something like ...

    $universe(agatha,butler,charles)

... will be equivalent to ...

    ! [X] : ( X = agatha | X = butler | X = charles )

$universe would be very useful in applications.

Your opinions please!

Cheers,

Geoff

[Nikolaj Bjorner]

IMOO:

Distinct is more succinct than spelling out all disequalities. It has a clear use. If you can handle distinct efficiently, which was looked at for CP solvers you don't have to expand into binary disequalities.

OTOH, universe doesn't save anything. 

A theorem prover can equivalently pattern match for finite domain axioms like these and

There is no guarantee that users/systems adding arbitrary formulas will remember to use this new feature.

You would also then have the option to reverse engineer $universe against all of TPTP benchmarks if you add such a change, and then you would render legacy provers to fend.

So I would call feature creep.

Cheers,

Nikolaj

---

From: tptp-...@googlegroups.com <tptp-...@googlegroups.com> on behalf of Geoff Sutcliffe <geoffgeo...@gmail.com>
Sent: Monday, March 3, 2025 11:11 AM
To: TPTP World <tptp-...@googlegroups.com>
Subject: [EXTERNAL] [TPTP World] $distinct and $universe

 

--
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/92c4194a-0227-4bce-88e4-d4f86cd7f4d7n%40googlegroups.com.

[Martin Suda]

Hi Geoff,

I am kind of on board with your sentiments (the beauty of two symmetrical notions, underpinning well-known assumptions from knowledge representation, ...), but Nikolaj is right that this just adds another (small) hurdle to writing a TPTP-compliant theorem prover and has no immediate practical benefit.

Personally, I never liked the idea that we (as prover developers) should just go "fishing for axioms" of various shapes (Nikolaj's pattern match here) if we want to treat them specially.

How about an optional field in the formula line ("special info"?) that the user could use to mark their intent ("universe", "commutative", "extensionality", ..., even "question", but that's a "role", maybe it shouldn't be) and perhaps trigger specific treatment of their favourite ATP, while the formula-content would be the only thing that ultimately matters (so that an average ATP need not bother and would still be sound and complete)?

Cheers,

Martin

To view this discussion visit https://groups.google.com/d/msgid/tptp-world/LV8PR21MB4239C24E411A152028D3E0F1C3C92%40LV8PR21MB4239.namprd21.prod.outlook.com.

[Stephan Schulz]

Hi all,

I tend to go with Nikloaj. I liked the idea at first, but after it became

obvious (to me) that it also needs typing, and type-checking, I think

it’s to much work for little gain.

Bye,

       Stephan

To view this discussion visit https://groups.google.com/d/msgid/tptp-world/CAHVDYO2RnkL5mEk%2Bw-b%3DO9p5z4kUcCh42K9Z91Tr8r-BtSRJcQ%40mail.gmail.com.

--

------------------------------ It can be done! ---------------------------------

          Please email me as sch...@eprover.org (Stephan Schulz)

--------------------------------------------------------------------------------

[Geoff Sutcliffe]

Hi everyone,

Thanks for the feedback. Given that there is not an overwhelming positive response, and worse it does not not meet the needs of people like Adam who really has closed worlds of objects, I'll leave it alone for now. I'm happy to reopen the discussion if anyone wants to say more.

Cheers,

Geoff