4

私は COQ を学んでいて、本の演習の 1 つに行き詰まっています。この本には解決策が書かれていないので、どうすればよいかわかりません。最初はやったけど。これらのステートメントを述語ロジックに変換する必要があります。

   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 は「誰も知らない人はいない」と言っています。これは要するに「誰かが誰かを知らないわけではない」ということです。次の 2 つの方法があります。

  1. 「誰かが誰も知らない」を手動でエンコードし、それを否定するだけです。

  2. (または) h0 を再利用し、その否定が「誰かが誰も知らない」であることに気付きます。

サッカー選手について話すには、変数x : Fansが を満たすことを確認するだけFootballer x ->です。たとえば、h3 は次のように始まります。

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

多分h5は少し難しいです。「1 人だけ」をエンコードする 1 つの方法は、彼が 1 人の人物 p0 を知っていると言い、別の人物 p1 を知っている場合、p1 = p0 であると言うことです。

難しいと思うことについての詳細がなければ、解決策ではない役立つ回答を提供することは困難です。

于 2012-10-21T02:56:58.557 に答える