예일 사격 문제
Yale shooting problem예일 사격 문제는 프레임 문제에 대한 초기 논리적 해결이 실패하는 공식 상황 논리의 난제 또는 시나리오입니다.이 문제의 이름은 발명가 스티브 행크스와 드류 맥더못이 예일 대학에서 이 문제를 제안했을 때 그들이 일했던 것에서 유래했다.이 시나리오에서는 Fred(나중에 칠면조라고 식별)가 처음에 살아있고 총이 최초로 장전된다.총을 장전하고 잠시 기다렸다가 프레드를 향해 총을 쏘면 프레드가 죽을 것으로 예상된다.그러나 이 상황의 변화를 최소화함으로써 관성을 논리적으로 공식화한다면 프레드가 장전, 대기, 사격 후에 죽었다는 것을 유일하게 증명할 수 없다.어떤 해결책에서는 프레드가 정말로 죽는다; 또 다른 해결책에서는, 의문의 총이 장전되고 프레드는 살아남는다.
기술적으로 이 시나리오는 v \ alive d d d d d d의 2가지 fluents(유창한 것은 true 값)로 기술됩니다.처음에는 첫 번째 조건은 true이고 두 번째 조건은 false입니다.그리고 나서, 총이 장전되고, 시간이 지나고, 총이 발사된다.이러한 문제는 4개의 0 0 1 22) 및 3)을 고려하여 시간에 따라 alive와 모든 유창한 것을 로 으로써 논리적으로 공식화할 수 있습니다.예일 총기난사 문제의 논리를 직접 공식화한 것은 다음과 같다.
처음 두 공식은 초기 상태를 나타냅니다.세 번째 공식은 (\ 0에 총을 장전하는 효과를 나타냅니다.네 번째 공식은 에 프레드를 쏘는 를 공식화한다이는 액션 이름이 무시되고 액션의 효과가 액션 실행 시점에 직접 지정되는 단순한 형식화입니다.자세한 내용은 상황 미적분을 참조하십시오.
위의 공식은 알려진 사실의 직접적인 공식이지만 도메인을 올바르게 특징짓기에는 충분하지 않습니다. 프레드가 총격을 당하기 전에 사망했다고 믿을 이유는 이 과 일치한다문제는 위의 공식에 작용의 효과만 포함될 뿐 작용에 의해 변경되지 않는 모든 감응이 동일하게 유지되도록 지정하지 않는다는 것입니다., i v e ( 0) ( alive ( )\ alive ( ){ alive ( 1 )}의 은 총기를 장전하면 l 의 값만 변경되고 v의 값은 변경되지 않는다는 암묵적인 가정을 공식화하기 위해 추가되어야 합니다.액션이 조건을 변경하지 않는 한 조건이 변하지 않는다는 명백한 사실을 기술하는 다수의 공식의 필요성을 프레임 문제라고 합니다.
프레임 문제의 초기 해결책은 변경을 최소화하는 것이었습니다.즉, 시나리오는 위의 공식(작용의 효과만 명시)과 시간의 경과에 따른 플루엔트의 변화가 가능한 최소라는 가정에 의해 공식화된다.그 근거는 위의 공식은 발생하는 모든 조치의 효과를 강제하는 반면, 최소화는 해당 조치의 결과로 인한 변경을 정확히 제한해야 한다는 것이다.
예일 사격 시나리오에서, 변화가 최소화되는 향수에 대한 가능한 한 가지 평가는 다음과 같습니다.
이것이 예상된 해결책입니다.여기에는 두 가지 유창한 변경이 포함되어 .즉, 1에서 d true가 되고 3에서 vfalse가 됩니다.다음 평가도 위의 모든 공식을 만족합니다.
이 평가에서는 두 가지 변경만 있습니다. d d d loaded { style}는 시간 1에서 true가 되고 시간 2에서 false가 됩니다.결과적으로 이 평가는 상태 진화에 대한 유효한 설명으로 간주됩니다.단, 2에서 l d d dd d \ styleloaded가 거짓이라고 할 수 있는 타당한 이유는 없습니다.변화의 최소화가 잘못된 해결책으로 이어진다는 점이 예일 총기난사 문제의 도입 동기다.
예일 총기 난사 문제는 역동적인 시나리오를 공식화하기 위한 논리 사용에 심각한 장애물로 여겨져 왔지만, 이에 대한 해법은 1980년대 후반부터 알려져 있다.한 가지 해결책은 동작의 사양에 술어 완성을 사용하는 것입니다.이 솔루션에 따르면 총을 쏘면 프레드가 죽는다는 사실은 살아있는 것과 적재된 것이라는 전제조건에 의해 공식화되며, 그 결과 살아있는 것이 값이 바뀝니다(이전에는 살아있는 것이 참이었기 때문에, 이것은 산 것이 거짓이 되는 것에 해당합니다.이 암시를 if와 if만의 문장으로 바꿈으로써 사격의 효과가 올바르게 공식화된다(복수의 암시가 있는 경우 사전 완료는 더 복잡해진다).
에릭 샌더월(Erik Sandewall)이 제안한 해결책은 새로운 폐색 조건을 포함하는 것이었습니다. 이 조건은 유창한 사람에게 "변경 허용"을 공식화하는 것입니다.따라서 fluent를 변경할 수 있는 액션의 효과는 fluent가 새로운 값을 가지며 폐색이 (일시적으로) 참이 되는 것입니다.최소화된 것은 일련의 변경이 아니라 일련의 폐색입니다.폐색이 true가 아닌 한 유창하게 변경되지 않도록 지정하는 또 다른 제약 조건이 이 솔루션을 완성합니다.
예일 사격 시나리오는 또한 상황 미적분, 유창한 미적분, 그리고 행동 기술 언어에 의해 정확하게 공식화된다.
2005년, 예일 총기 사건이 처음 묘사된 1985년 논문은 AAAI 클래식 페이퍼 상을 받았다.해결된 문제임에도 불구하고, 그 예는 여전히 최근의 연구 논문에서 언급되고 있으며, 문제로서 제시되는 것이 아니라 예시적인 예(예를 들어 행동에 대한 추론을 위한 새로운 논리의 구문 설명)로 사용된다.
「 」를 참조해 주세요.
레퍼런스
- M. Gelfond와 V.Lifschitz(1993)논리 프로그램으로 동작과 변화를 표현합니다.논리 프로그래밍 저널, 17:301–322.
- S. 행크스와 D.McDermott(1987년).비단조적 논리와 시간적 투영.인공지능, 33(3):379~412.
- J. 매카시(1986년).상식적인 지식을 공식화하기 위한 제한 적용.인공지능, 28:89~116.
- T. Mitchell과 H. Levesque(2006).2005년 AAAI 클래식 페이퍼상."AI 매거진", 26(4):98~99.
- R. 반복(1991)상황 미적분의 프레임 문제: 단순한 해결책(가끔)과 목표 회귀의 완전성 결과.블라디미르 리프시츠 편집자, 인공지능과 수학 계산 이론: 존 맥카시를 기리는 논문, 359-380페이지.뉴욕, 학술 출판사
- E. Sandewall(1994)특징과 향기.옥스퍼드 대학 출판부