증명을 찾지 못한 일은 부정을 증명한 일과 다르다.
질의 시스템은 논리식처럼 보이는 규칙에 실제 탐색 절차를 붙입니다. 빠진 사실과 규칙 방향, 데이터베이스 가정, 종료 한도가 실행이 정직하게 내릴 수 있는 결론을 결정합니다.
어떤 결론은 논리 관계에서 나오고 어떤 결론은 특정 데이터베이스와 탐색 절차에서 나올까요?
- 논리적 부정과 실패를 부정으로 간주하는 방식을 구분하기
- 빠진 사실로 결론을 내릴 때 필요한 닫힌 세계 가정 설명하기
- 관계의 선언적 의미와 탐색 절차 구분하기
- 대칭 규칙이 한 질의를 증명하고 다른 질의에서는 반복되는 모습 관찰하기
- 종료하지 않는 탐색을 답처럼 보이지 않고 명시적인 한도로 보고하기
첫 프로그램은 not-known-role?을 역할 사실을 찾지 못한 것으로 일부러 정의합니다. ada와 cy와 zoe 모두 참을 반환하지만 정보의 뜻은 같지 않습니다. ada와 cy는 알려진 사람인데 manager 사실이 기록되지 않았고, zoe는 알려진 사람이라는 사실조차 없습니다. 모든 실패한 조회를 논리적 부정으로 해석하려면 데이터베이스가 관련된 사실을 빠짐없이 담았다는 닫힌 세계 가정이 필요합니다.
두 번째 프로그램은 married 관계에 대칭 탐색 규칙을 붙입니다. 직접 사실이 없으면 인자를 바꾸어 다시 찾습니다. 이 규칙은 반대 방향 사실이 있는 (married mickey minnie)를 한 번 뒤집어 증명합니다. 관련 없는 두 사람은 반복 탐지를 하거나 작업 예산을 쓰지 않으면 같은 두 질의를 끝없이 왕복합니다. 논리 관계가 대칭이어도 규칙의 방향과 제어가 실제 탐색의 동작을 결정합니다.
(begin
(define facts
'((known-person ada)
(known-person ben)
(known-person cy)
(role ada programmer)
(role ben manager)))
(define (fact? candidate remaining)
(cond ((null? remaining) #f)
((equal? candidate (car remaining)) #t)
(else (fact? candidate (cdr remaining)))))
(define (known-person? person)
(fact? (list 'known-person person) facts))
(define (known-role? person role)
(fact? (list 'role person role) facts))
(define (not-known-role? person role)
(not (known-role? person role)))
(define (role-status person role)
(cond ((known-role? person role) 'proved)
((known-person? person) 'not-proved-for-known-person)
(else 'unknown-person)))
(list (not-known-role? 'ada 'manager)
(not-known-role? 'cy 'manager)
(not-known-role? 'zoe 'manager)
(role-status 'ada 'manager)
(role-status 'cy 'manager)
(role-status 'zoe 'manager)))- 출력
- —
- 값
- —
- 진단
- —
첫 프로그램은 (#t #t #t not-proved-for-known-person not-proved-for-known-person unknown-person)을 반환합니다. 두 번째 프로그램은 mickey와 minnie 질의는 증명하고 donald와 daisy 질의는 같은 두 쌍을 반복하다 truncated로 보고합니다.
첫 실행에서는 같은 세 실패 booleans와 서로 다른 known-person 확인을 비교하세요. 두 번째 실행에서는 인자를 뒤집는 단계와 직접 사실 스캔, 경로 추가, 작업 예산 감소를 따라가세요. 한 질의는 한 번 뒤집어 사실에 닿고 다른 질의는 명시적인 한도에서 잘립니다.
힌트를 보기 전에 프로그램을 바꿔 보세요.
(known-person zoe)를 역할 없이 추가하고 (married daisy donald)를 추가하세요. 첫 실행에서 어떤 상태가 달라지고 두 번째 실행에서 어떤 대칭 질의가 이제 완료되는지 예상하세요.
힌트 하나 보기
known-person 사실은 역할을 증명하지 않지만 zoe에 대해 데이터베이스가 말할 수 있는 상태를 바꿉니다. 직접 married 사실은 반대 방향 질의에 한 번의 뒤집기 경로를 줍니다.