【发布时间】：2021-12-03 23:28:32
【问题描述】：
我尝试在 Alloy 上实现一篇关于 mereology 的论文中描述的公理系统：“Bennett，有一个部分两次结束，2013 年”。
我实现了所有的公理，我认为如果我正确地实现了它们，我就可以断言和检查这些定理。
这就是我的编码方式：
/* (T9) Conditional Reflexivity */
assert conditional_reflexivity {
all x: Filler | some z: Slot | z in x.slots implies x in x.parts
}
（Ps(z, x) 表示 z 是 x 的一个槽，P(x, x) 表示 x 是 x 的一部分。我将槽和部分都编码为集合。）
但是，当我检查断言时，似乎有些东西不起作用。我得到了以下反例：
但我不明白这是一个暗示的反例。连前提都没有实现。唯一有意义的方法是它要求每个 x 都有一个 z。在这种情况下，这肯定是一个反例。在这种情况下，我如何检查这个定理？
（如果需要，我可以分享完整的代码。）
【问题讨论】：
-
看起来像一个优先问题，当你想要
A((Ep) impl q)时，你得到了AE(p impl q)。添加括号可以解决问题吗？ -
@Hovercouch 它有效。谢谢！我不明白“优先级问题”是什么意思。运营商优先级有问题吗？
-
是的，暗示比
some绑定得更紧密。 -
@Hovercouch 你想写一个答案吗？这样我可以验证你的答案。
标签： alloy