I'm still not able to express certain mutual exclusiveness with Attempo.<br><br>I want to say: <br> ∀x. IsInserted(x) ⇒ ¬∃y. IsInserted(y) ∧ x ≠y<br><br>My expected translation of that would be:<br>If there exists an x that is inserted then there does not exist a y different from x that is inserted.<br>
OR (inclusive!):<br>For every x that is inserted there is no y different from x that is inserted.<br>Tersely: Only one object could be inserted.<br><br>How could this exclusiveness be expressed?<br><br><div class="gmail_quote">
2010/7/11 Norbert E. Fuchs <span dir="ltr"><<a href="mailto:fuchs@ifi.uzh.ch">fuchs@ifi.uzh.ch</a>></span><br><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<div class="im"><br>
On 11 Jul 2010, at 10:45, Gabriele Kahlout wrote:<br>
<br>
> I found no documentation on expressing mutual exclusiveness.<br>
<br>
</div>See "2.2.5 How to Express Exclusive Disjunction?" in the document "ACE Troubleshooting Guide" (<a href="http://attempto.ifi.uzh.ch/site/docs/ace_troubleshooting.html" target="_blank">http://attempto.ifi.uzh.ch/site/docs/ace_troubleshooting.html</a>).<br>
<font color="#888888"><br>
--- nef<br>
<br>
</font></blockquote></div><br><br clear="all"><br>-- <br>Regards, <br>K. Gabriele<br><br>--- unchanged since 25/1/10 ---<br>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.<br>
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).<br><br>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.<br>
∀x. In(x, MyInbox) ⇒ In(senderAddress(x), MySafeSenderList) ∨ (∃y. In(y, subject(this) ) ∧ In(y,x) ∧ isCodeLike(y, -LICHT01X) ).<br><br>