인수를 자동으로 검증하는 소프트웨어가 있습니까?
나는하고 싶어요
- 영어에서 논리적 인 주장을 도출하고
- 프로그램을 사용하여 유효성을 테스트하십시오.
2 단계 용 소프트웨어가 있습니까? 포기한다면 괜찮을 텐데
- 유효성을 계산할 수 없거나
- 결과를보고하는 데 시간이 오래 걸립니다.
나는이 질문을하는 것이 논리에 대한 나의 무지를 드러 낼 수 있다는 것을 알고 있으므로, 그것이 어리석은 질문이라면 그 이유를 설명하는 몇 가지 참고 자료에 감사 할 것입니다. 저는 Metalogic : An Introduction to the Metatheory of Standard First Order 로 시작 하겠습니다 .
답변
당신은 소위 자동화 된 정리 증명 자를 찾고 있습니다.
예를 들어 , 고전 명제 및 1 차 논리에 대한 분석 테이블 의 미적분의 두 가지 구현에 대해서는 pyPL 또는 Tree Proof Generator 를 참조하십시오 .
tableau 미적분은 1 차 타당성에 대해 완전합니다. 즉, 모든 유효한 추론이 그대로 감지됩니다.
그러나 1 차 논리는 반 결정이 불가능합니다. 즉, 모든 비 추론을 탐지하는 알고리즘을 찾을 수 없습니다. 잘못된 추론에서 tableau 알고리즘은 무한대로 실행됩니다.
반면에 명제 논리는 완전히 결정 가능합니다. tableau 알고리즘은 결국 모든 유효하고 모든 유효하지 않은 명제 인수를 감지합니다.
또한 복잡성 제약이 존재합니다. tableau 트리는 정교한 휴리스틱이 구현되지 않는 한 조합 폭발에 특히 취약하므로 위의 두 프로그램은 비교적 단순한 인수에 대해서만 현실적으로 작동합니다.
다른 많은 증명 시스템의 구현도 수행되었습니다. Wikipedia에 여러 가지가 나열되어 있지만 직접 작업 한 적이 없으므로 비 학문 및 비 산업용 사용 사례에 적합한 것이 무엇인지 확인해야합니다.