苏格拉底终有一死

Question

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

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

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

Answer 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

Answer 2

另一种选择：

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

check {Socrates in Mortal}

Answer 3

有意思。几周前我做了这个。

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

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

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

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

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

然而，使用三段论很容易搞砸：

人终有一死。
苏格拉底终有一死。
所以苏格拉底是人。

这可以在 Alloy 中完成，如下所示

check Wrong {

    all mortal, men : some Men + Socrates {

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

    }
} for 5 Men

当我们检查这个时，我们得到一个版本，其中苏格拉底在道德方面而不是在人方面。

您可以找到 html 版本 here and the source for this here。这些使用新提议的 Alloy 5 markdown 格式。

苏格拉底终有一死

Socrates is mortal

alloy