[Attempto] or is interpreted as inclusive or , or xor?

[Norbert E. Fuchs]

On 11 Jul 2010, at 15:21, Gabriele Kahlout wrote:

> I'm still not able to express certain mutual exclusiveness with Attempo.
> 
> I want to say: 
>  ∀x. IsInserted(x) ⇒ ¬∃y. IsInserted(y) ∧ x ≠y
> 
> My expected translation of that would be:
> If there exists an x that is inserted then there does not exist a y different from x that is inserted.
> OR (inclusive!):
> For every x that is inserted there is no y different from x that is inserted.
> Tersely: Only one object could be inserted.
> 
> How could this exclusiveness be expressed?

As in your FOL formula just express that x is not y, i.e. use "is not" in ACE.

See section "2.3.3 Negating Verb Phrases" in the document "ACE Construction Rules" (http://attempto.ifi.uzh.ch/site/docs/ace_constructionrules.html).

We are certainly happy to answer your questions, but may I suggest again that you have a look at the documentation?

   --- nef