이 코칭 연습 문제를 해결하십시오.

코큐를 배우고 있고 책 연습 중 하나에 붙어 있습니다. 이 책은 나에게 해결책을주지 않으므로 해야할지 모르겠다. 나는 첫번째 것을 끝내었다. 나는 술어 논리에이 문장을 번역 할 수 있습니다이 코칭 연습 문제를 해결하십시오.

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

합니다.

도와 주시겠습니까? 정말 고맙습니다!

출처

2012-10-21 Nayr

"The Book"은 [Coq'Art] (http://labri.fr/perso/casteran/CoqArt/index.html)입니다. 맞습니까? – minopret

본인은 이러한 정의가 귀하에게 제공된 것으로 가정하므로 "모든 사람"은 Fans의 회원으로 표시됩니다.

무엇이 붙어 있습니까?

예를 들어, h1은 "아무도 아무도 모릅니다"라고 말합니다. 이 사실이 "사람이 누구를 알지 못하는 것은 아니다"라는 사실에 달려있다. 이제 당신이 진행하는 두 가지 방법이 있습니다

당신은 인코딩

수동으로 "사람이 사람을 알지 못한다"하고 그냥 부정.
(또는) h0을 다시 사용하면서 부정을 "누군가는 알지 못합니다"라는 것을 알았습니다.

은 축구에 대해 이야기하려면 변수 x : Fans이 Footballer x ->을 만족하는 것을 그냥 확인합니다.

어쩌면 H5

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

조금 어렵습니다 : 같은 예를 들어 는, H3는 시작합니다. "한 사람 만"을 인코딩하는 한 가지 방법은 한 사람을 p0으로 알고, 다른 사람이 p1을 알고 있으면 p1 = p0이라고 말합니다.

어려운 점을 자세히 설명하지 않으면 해결책이 아닌 유용한 답을 제공하기가 어렵습니다.

출처

2012-10-21 02:56:58 Ptival

이 코칭 연습 문제를 해결하십시오.

답변

관련 문제