4

我正在学习 COQ，但我被困在书中的一个练习中。这本书没有给我一个解决方案，所以我不知道该怎么做。虽然我已经完成了第一个。我必须将这些语句转换为谓词逻辑：

   h0 : Everybody knows somebody
   h1 : Nobody doesn't know anybody. 
   h2 : Everybody knows somebody 
   h3 : A footballer is known by everybody.
   h4 : Footballers only know footballers. 
   h5 : There is somebody who only knows one person.

代码：

Section Stadium.

Variable Fans : Set.
Variable Knows : Fans -> Fans -> Prop.
Variable Footballer : Fans -> Prop.

Hypothesis h0 : forall x: Fans, exists y: Fans, Knows x y.


End Stadium

.

你能帮忙吗？非常感谢！

4

1 回答 1

3

我假设这些定义已提供给您，因此“每个人”都由Fans.

你被什么困住了？

例如，h1 表示“没有人不认识任何人”。这归结为一个事实，即“并非某人不认识任何人”。现在您有两种方法可以继续：

  1. 您手动编码“某人不认识任何人”，然后否定它。

  2. （或）你重用 h0，注意到它的否定是“某人不认识任何人”。

要谈论足球运动员，您只需验证一个变量x : Fans满足Footballer x ->。例如，h3 的开头如下：

forall x, Footballer x -> (* here, you encode "everybody knows x" *)

也许h5有点难。编码“只有一个人”的一种方法是说他认识一个人 p0，如果他认识另一个人 p1，那么 p1 = p0。

如果没有关于您发现困难的更多细节，很难为您提供一个不是解决方案的有用答案。

于 2012-10-21T02:56:58.557 回答