[Attempto] Auto-discard notification

[Andrii Kurdiumov]

Hi Norbert, and all

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.

Obviously you should take my opinion with a grain of salt, since I'm yet to
write any significant document in ACE.

Best regards,
Andrey


On Fri, Apr 23, 2021 at 10:14 PM Norbert E. Fuchs <fuchs at ifi.uzh.ch> wrote:

>
>
> > 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.ifi.uzh.ch/pipermail/attempto/attachments/20210425/076e68cc/attachment.html>