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

[Gabriele Kahlout]

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?

2010/7/11 Norbert E. Fuchs <fuchs at ifi.uzh.ch>

>
> On 11 Jul 2010, at 10:45, Gabriele Kahlout wrote:
>
> > I found no documentation on expressing mutual exclusiveness.
>
> See "2.2.5 How to Express Exclusive Disjunction?" in the document "ACE
> Troubleshooting Guide" (
> http://attempto.ifi.uzh.ch/site/docs/ace_troubleshooting.html).
>
>   --- nef
>
>


-- 
Regards,
K. Gabriele

--- unchanged since 25/1/10 ---
P.S. Unless a notification (LON), please reply either with an answer OR with
" ACK" appended to this subject within 48 hours. Otherwise, I might resend.
In(LON, this) ∨ In(48h, TimeNow) ∨ ∃x. In(x, MyInbox) ∧ IsAnswerTo(x, this)
∨ (In(subject(this), subject(x)) ∧ In(ACK, subject(x)) ∧
¬IsAnswerTo(x,this)) ⇒ ¬IResend(this).

Also note that correspondence may be received only from specified a priori
senders, or if the subject of this email ends with a code, eg. -LICHT01X,
then also from senders whose reply contains it.
∀x. In(x, MyInbox) ⇒ In(senderAddress(x), MySafeSenderList) ∨ (∃y. In(y,
subject(this) ) ∧ In(y,x) ∧ isCodeLike(y, -LICHT01X) ).
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.ifi.uzh.ch/pipermail/attempto/attachments/20100711/4022bf89/attachment.htm>