나는 석사 학위의 최종 시험을 준비하고 있는데, 이것은 과거의 시험 문제입니다. 정말 혼란 스럽습니다. 어디서부터 시작해야할지 모르겠군요.A * 알고리즘으로 입증 된 정리
제 생각에 허용 가능한 발견 적 도구 인 해결 규칙이 있습니다. 그런 다음 해결 규칙이 받아 들여질 수 있음을 증명하는 것이 맞습니까? 그렇다면 해결 규칙이 합법적임을 증명하기 위해 어디서부터 시작해야합니까? 도움을 주셔서 감사합니다.
정리 정리 응용을 고려하십시오. A * 알고리즘을 사용하여 가장 간단한 (가장 짧은) 증명을 검색 할 수 있습니다. 알려진 공리와 정리가 명제 논리에서 호른 절의 지식 기반으로 표현되고, 증명 기가 역방향 연쇄를 사용한다고 가정합니다.
(a) 허용되는 휴리스틱을 제안하십시오.
(b)는 제안 된 휴리스틱은 '예, theorm 증명이 결의의 종류 의미
허용 것을 증명한다.
호른 절은 명확한 절이거나 무결성 제약 조건입니다. 즉, 혼 (Horn) 절은 거짓 또는 보통 원자를 머리로가집니다.
무결성 제약 조건은
false ← a1∧ ... akak 형식의 절입니다.
무결성 제약 조건을 통해 원자 기반의 일부 모델이 지식 기반의 모든 모델에서 거짓이라는 것을 증명할 수 있습니다. 즉, 부정의 부정을 증명하는 것입니다.
호른 절 지식베이스는 원자 부정을 암시 할 수 있습니다.
예 : 기술 자료 KB1을 고려하십시오.
false←a∧b.
a←c.
b←c.
KB1의 모든 모델에서 원자 c는 false입니다. KB1의 모델 I에서 c가 true이면 a와 b는 모두 1에 해당합니다 (그렇지 않으면 KB1의 모델이 아닐 것입니다). I에서 false가 거짓이고 I에서 a와 b가 참이므로 첫 번째 절은 I에서 거짓이며 KB1의 모 델 인 모순입니다. 따라서 KB1의 모든 모델에서 c는 거짓입니다. 이것은 KB1 ¬c 으로 표시됩니다. 즉, ¬c는 KB1의 모든 모델에서 true이므로 KB1의 모든 모델에서 c가 거짓입니다.
답변에 설명 된 주제와 관련된 간단한 설명은 어디에서 볼 수 있습니까? (나는 AI에있어 초보자입니다.) –
vinash : http : //artint.info/html/ArtInt_122.html –
링크를 고맙습니다. :) –
A *는 가능한 트리를 검색하여 좋은 것을 찾거나 제한이있는 최상의 것을 찾는 알고리즘입니다. 당신은 그림에 꼭 맞는 것으로 입증 된 정리를 볼 수 있습니다 (나무와 같은 방식으로 증명을 열거 할 수있는 경우). –