Coq

Пить или не пить? Про­грам­мис­ты при­вык­ли мыс­лить в рам­ках бу­ле­вой ло­ги­ки. Я хо­чу не­множ­ко по­ло­мать клас­си­чес­кие про­грам­мист­ские пред­став­ле­ния о том, что та­кое ло­гич­но. В клас­си­чес­кой ма­те­ма­ти­чес­кой ло­ги­ке есть та­кое по­ня­тие: про­по­зи­ция. Она же утверж­де­ние, суж­де­ние и т.д. Утверж­де­ние мо­жет быть вер­ным, вер­ным мо­жет быть и его от­ри­ца­ние. Пока вро­де всё нор­маль­но: int p=1; if (p) { printf ("OK!\n"); } int p=0; if (!p) { printf ("OK!\n"); } Но это — бу­ле­ва ло­ги­ка.