合金中从谓词演算风格到关系演算风格

Question

我有两个合金事实：

fact A5 {
  all a, b : Filler, s, t : Slot |
    (b in s.slot_of and s in a.fills and a in t.slot_of) implies b in t.slot_of 
}
fact A6 {
  all a, b : Filler, s, t : Slot | ((b in s.slot_of  and s in a.fills) and
      (a in t.slot_of and t in b.fills)) implies a = b
}

当我注意到关系演算风格似乎比谓词演算风格更有效（生成的变量和子句更少）时，我想使用关系演算风格重写它们。

对于 A5，我有这个：

fact A5 { slot_of.fills.slot_of in slot_of }

如果我正确理解这些风格，效果很好，并且与微积分风格相关。

但是对于A6，我没有实现重写。现在，我得到了这个：

fact A6 {
  all a, b : Filler | (a->b in fills.slot_of and b->a in fills.slot_of) implies a = b
}

效率更高，但我认为它仍然是谓词演算风格。所以我有一些疑问：我现在的A6是谓词演算风格的吗？是否可以用关系演算风格重写它？如果是的话，怎么办？

Answer 1

它仍然是谓词演算风格，因为您使用的是

all

量词。为了保持关系，它不能使用任何量词。

我认为你想要的事实是“唯一的对称关系是自反关系”。所有自反关系的集合是

iden

，

r

中所有对称关系的集合是

r & ~r

。因此，如果您想让

A6

完全相关，您可以写

fills.slot_of & ~(fills.slot_of) in iden

。