[Attempto] Auto-discard notification

[Norbert E. Fuchs]

> On 22 Apr 2021, at 20:38 , Kaarel Kaljurand <kaljurand at gmail.com> wrote:
> 
> Hi,
> 
> what you are describing is what OWL calls DisjoinUnion. ACE does not
> have a short single-sentence expression for this. I wrote about it in
> my thesis, see
> 
> 5.7.4 DisjointUnion and other short-hand constructs
> http://attempto.ifi.uzh.ch/site/pubs/papers/phd_kaljurand.pdf
> 
> Best,
> Kaarel
> 
>> ---------- Forwarded message ----------
>> From: Andrii Kurdiumov <kant2002 at googlemail.com>
>> To: "Norbert E. Fuchs" <fuchs at ifi.uzh.ch>, attempto ML <attempto at lists.ifi.uzh.ch>
>> Cc:
> 
>>> Now back to the original issue.
>>> "No dog is a cat" is fine if the set has only 2 non-intersecting subsets. What about 3 non-intersecting subsets. Let's say I want to expand to animal = { cat, dog, rabbit }. What are the options?

Andrii, Kaarel and all

Kaarel is right, ACE does not offer a compact way to express that N items are disjoint. To do so requires N/2*(N-1) statements of the form "No A is a B.", which is OK for Andriis's example (cat, dog, rabbit), but gets out of hand for larger numbers.

There is, however, a solution offered by the Attempto reasoner RACE. 

I recently extended RACE by an interface to Prolog in the form ["functor", Argument1, ... , ArgumentN] that calls the user-defined or built-in Prolog predicate functor(Argument1, ..., ArgumentN). Please note that this interface has not yet been published, but is available in RACE's web-interface for built-in Prolog predicates.

If there is sufficient interest I could implement the predicate ["distinct, List of N distinct items] that would automatically generate the N/2*(N-1) statements of "distinctness". Note that since these statements are RACE internal, they would not appear in the original list of axioms or in the list of axioms needed for the proof. This could cause confusion or misunderstandings.

Before I decide to implement this I would like to get your feedback. How often do we need to express that, say 10 items, are distinct?

Best regards.

   --- nef