[일반] Coq 실제로 활용하는 사람 있어?

[익명(14.36)]

배워볼까 하는데 입문 자체가 쉽지 않아보이네. 일단 참고자료가 많지 않다.

순수수학 하는 사람 중에 Coq 활용하는 사람 어느 정도 있는지 궁금하다.

선택공리 가정하는 명제도 구현 가능한가?

[익명(220.70)]

'선택공리 가정하는 명제도 구현 가능한가?' 이게 뭔 뜻임? Prop 레벨 선택공리는 증명 못함. 물론 진술은 됨.

[익명(220.70)]

입문은 Software Foundations 보면 됨

[익명(14.36)]

헉 교재 추천 고맙다. 예를 들어 cardinality trichotomy 이런 걸 증명할 수 있냐는 뜻임.

[익명(220.70)]

일단 Coq 자체가 type theory 기반이라서, 제대로 각 잡고 하려면 1차논리 추론규칙부터 정의하고 그 위에서 ZFC 가지고 놀아야 할걸? 공리꼴도 다뤄야 될 텐데, 잘 되길 빈다..............

[익명(14.36)]

교재 추천만 해도 ㅆㅅㅌㅊ ㄱㅅㄱㅅ