苏格拉底会死答案

【问题标题】：Socrates is mortal苏格拉底会死
【发布时间】：2018-02-22 22:42:16
【问题描述】：

All men are mortals.
Socrates is a man.
Therefore, Socrates is a mortal.

在合金模型下方表达推理规则。这是表达推理规则的好方法吗？你能提供更好的表达方式吗？

abstract sig man {}

// Socrates is a man
one sig Socrates extends man{}
one sig Plato extends man{}
one sig Aristotle extends man{}

one sig Earthly {
    mortals: set man
}

// All men are mortal
fact All_men_are_mortal {
    all m: man | m in Earthly.mortals
}

// Therefore, Socrates is mortal
assert Socrates_is_mortal {
    Socrates in Earthly.mortals   
}
check Socrates_is_mortal

【问题讨论】：

我投票决定将此问题作为离题结束，因为它要求进行代码审查（因此这太宽泛/基于意见）。它可能会被调整为the code review stackexchange 的主题。

标签： alloy

【解决方案1】：

为了更接近自然语言的表述，你可以这样写：

assert Syllogism {
  all Socrates: univ, Man, Mortal: set univ |
      -- every man is mortal
      Man in Mortal
      -- Socrates is a man
      and (Socrates in Man)
      -- implies Socrates is mortal
      implies Socrates in Mortal
  }

check Syllogism

【讨论】：

哇！惊人的！谢谢@Daniel Jackson

【解决方案2】：

有趣。几周前我这样做了。

在你的定义中，你已经把苏格拉底是一个男人的标志。这基本上使三段论变得多余，因为您已经说过苏格拉底是男人。

因此，我认为您需要一个模型，其中苏格拉底不是男性的定义。

简而言之，我对三段论的正确使用版本

sig Men{}
one sig Socrates {}

check Correct {

    all mortal, men : some Men + Socrates {

        men in mortal
        and  
        Socrates in men 
        => Socrates in mortal

    }
} for 5 Men

如果你检查这个，那么没有反例，所以我们似乎没问题。

但是，三段论很容易搞砸：

所有人都会死。
苏格拉底是凡人。
因此苏格拉底是人。

这可以在合金中完成如下

check Wrong {

    all mortal, men : some Men + Socrates {

        men in mortal
        and  
        Socrates in mortal 
        => Socrates in men

    }
} for 5 Men

当我们检查这一点时，我们会得到一个版本，其中苏格拉底是道德的，但不是人的。

您可以找到一个 html 版本 here 和这个 here 的源代码。这些使用新提议的 Alloy 5 降价格式。

【讨论】：

【解决方案3】：

另一种选择：

sig Mortal {}
sig Man extends Mortal {}
one sig Socrates extends Man {}

check {Socrates in Mortal}

【讨论】：

谢谢@wmeyer