<div dir="ltr">Hi Norbert, and all<div><br></div><div>If you would count my opinion, I would not advise having that as a permanent solution. These statements, once generated, would be hard to maintain in practice. Plus you can have more than one DisjointUnions in a single document, and such kind of boilerplate usually affects reader flow.</div><div><br></div><div>Obviously you should take my opinion with a grain of salt, since I'm yet to write any significant document in ACE.  </div><div><br></div><div>Best regards,</div><div>Andrey</div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Apr 23, 2021 at 10:14 PM Norbert E. Fuchs <<a href="mailto:fuchs@ifi.uzh.ch" target="_blank">fuchs@ifi.uzh.ch</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><br>
<br>
> On 22 Apr 2021, at 20:38 , Kaarel Kaljurand <<a href="mailto:kaljurand@gmail.com" target="_blank">kaljurand@gmail.com</a>> wrote:<br>
> <br>
> Hi,<br>
> <br>
> what you are describing is what OWL calls DisjoinUnion. ACE does not<br>
> have a short single-sentence expression for this. I wrote about it in<br>
> my thesis, see<br>
> <br>
> 5.7.4 DisjointUnion and other short-hand constructs<br>
> <a href="http://attempto.ifi.uzh.ch/site/pubs/papers/phd_kaljurand.pdf" rel="noreferrer" target="_blank">http://attempto.ifi.uzh.ch/site/pubs/papers/phd_kaljurand.pdf</a><br>
> <br>
> Best,<br>
> Kaarel<br>
> <br>
>> ---------- Forwarded message ----------<br>
>> From: Andrii Kurdiumov <<a href="mailto:kant2002@googlemail.com" target="_blank">kant2002@googlemail.com</a>><br>
>> To: "Norbert E. Fuchs" <<a href="mailto:fuchs@ifi.uzh.ch" target="_blank">fuchs@ifi.uzh.ch</a>>, attempto ML <<a href="mailto:attempto@lists.ifi.uzh.ch" target="_blank">attempto@lists.ifi.uzh.ch</a>><br>
>> Cc:<br>
> <br>
>>> Now back to the original issue.<br>
>>> "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?<br>
<br>
Andrii, Kaarel and all<br>
<br>
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.<br>
<br>
There is, however, a solution offered by the Attempto reasoner RACE. <br>
<br>
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.<br>
<br>
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.<br>
<br>
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?<br>
<br>
Best regards.<br>
<br>
   --- nef<br>
<br>
</blockquote></div>