저는 2 학년 학생으로 이산 수학 2 과제는 자동 정리 정리를 만드는 것입니다. 나는 Propositional Logic에서 4 주 만에 작동하는 간단한 증명 프로그램을 만들어야합니다 (증명이 항상 존재한다고 가정). 나는 지금까지 googled했다. 그러나 물질은 4 주 만에 이해하기 정말로 어렵다. 누구나 초보자를위한 책/사이트/오픈 소스 코드 나 몇 가지 유용한 힌트를 추천 해 줄 수 있습니까? 미리 감사드립니다.자동 정리 정리 프로그램 - 어디에서 시작할까요?
참고 : 컴퓨터 과학 사이트로 이동할 수 있음을 알려주었습니다.저기서 ATP보다 훨씬 위에 위치했기 때문입니다.
당신이 봤던 것을 포함 할 수 있다면 왜 좋을까요? 그러면 우리는 당신에게 더 나은 것이 무엇인지 알 수 있습니다. 또한, 프로그램을 작성해야한다면, 알고있는 언어를 아는 것이 도움이 될 것입니다. 이 작업의 대부분은 OCaml이나 F #과 같은 함수 언어 나 Prolog 나 Mercury와 같은 논리 언어로 수행됩니다.
"Handbook of Practical Logic and Automated Reasoning"(WorldCat) John Harrison이 보셨나요? 나는 (WorldCat) 링크를 포함 시켰습니다. 그래서 당신은 대부분의 시간을 먹을 것 인 그것을 사기를 기다리는 것과 반대로 지역 도서관에서 책을 찾을 수 있습니다.
코드 하단에 OCaml 코드가 있으며 F # here 및 하스켈 here 코드가 있습니다.
위키 피 디아에서 ATP 또는 Proof Assistant을 볼 수없는 경우 일부 코드와 논문이 나올 수 있습니다.
오픈 소스 링크에 감사하지만 F #과 Haskell과 OCaml을 모르므로 C++을 고수 할 것입니다. 어쨌든 http://arxiv.org/ftp/cs/papers/9301/9301110.pdf에서 재미있는 사람을 발견했습니다. 나는 그와 잠시 놀아 나갈 것 같아. – minhnhat93
@ minhnhat93 좋은 종이. Paulson은 주제 분야에서 최고 중 하나입니다. 샘플 코드가 ML에 있고 OCaml과 F #의 전신 인 것은 알고 있습니까? 폴슨 (Paulson)이 "ML 프로그래머 용 ML"을 확보 할 수 있다면 코드를 이해하는 데 도움이 될 것입니다. –
이 증명 기가 대개 기능 언어로 작성되고 c, java, C# 같은 인기있는 언어로 작성되지 않는 특별한 이유가 있습니까? ML이 OCaml과 F #의 전신 인 경우 지금 F #을 배울 필요가 있다고 생각합니다. – minhnhat93