기본 논리

기본 논리는 Raymond Reiter가 기본 추측으로 추론을 공식화하기 위해 제안한 비 단조 적 논리입니다.

기본 논리는 “기본적으로 어떤 것이 사실”과 같은 사실을 나타낼 수 있습니다. 반대로 표준 논리는 무언가가 사실이거나 무언가가 거짓임을 표현할 수 있습니다. 추론은 대개의 경우 사실이지만 항상 그런 것은 아니기 때문에 종종 문제가됩니다. 전형적인 예는 “새들이 일반적으로 날다”입니다. 이 규칙은 펭귄이 날지 않는다는 사실과 일치하지 않는 “모든 새들이 날아 다닌다”거나 타조가 아닌 타조와 파리가 아닌 모든 새들에 의해 표준 논리로 표현 될 수있다. 지정된 규칙에 대한 예외. 기본 논리는 명시 적으로 모든 예외를 언급하지 않고 이와 같은 추론 규칙을 형식화하는 것을 목표로합니다.

기본 논리 구문
기본 이론은 한 쌍입니다.  . W는 배경 이론 (background theory)이라고하는 논리적 인 수식의 집합으로, 알려진 사실을 형식화합니다. D는 일련의 기본 규칙이며 각 규칙은 다음과 같은 형식입니다.

이 기본값에 따르면 선행 조건이 true이고 각 {\ displaystyle \ mathrm {Justification} _ {i}} 우리의 현재 신념과 일치하면, 우리는 결론이 진실하다는 것을 믿게됩니다.

W의 논리적 수식과 기본값의 모든 수식은 원래 1 차 논리 수식으로 간주되지만 잠재적으로 임의의 공식 논리에서 수식이 될 수 있습니다. 명제 논리의 공식 인 경우는 가장 많이 연구 된 것 중 하나입니다.

예제들
기본 규칙 “새들은 일반적으로 날아갑니다”는 다음 기본값에 의해 공식화됩니다.

이 규칙은 X가 새이고 파리가 있다고 가정 할 수 있다면 파리가 있다고 결론 내릴 수 있습니다. 조류에 관한 몇 가지 사실을 담고있는 배경 이론은 다음과 같습니다.
.

이 기본 규칙에 따르면, 전제 조건 조류 (Condor)가 참이고 정당화 파리 (Condor)가 현재 알려진 것과 일치하지 않기 때문에 콘도르가 날아갑니다. 반대로 조류 (펭귄)는 파리 (펭귄)의 결론을 허용하지 않습니다 : 기본 조류 (펭귄)의 전제 조건이 사실이라 할지라도 정당화 파리 (펭귄)는 알려진 것과 일치하지 않습니다. 이 기본 이론과이 기본 이론에서 기본 규칙은 Bird (X)에서 Flies (X)를 파생시킬 수 있기 때문에 Bird (Bee)는 결론 지을 수 없습니다. 결과로부터 추론 규칙의 선행을 도출하는 것은 결과에 대한 설명의 한 형태이며, 납득이 론적 추론의 목적이다.

일반적인 기본 가정은 사실로 알려지지 않은 것이 거짓이라고 믿는 것입니다. 이것은 Closed World Assumption으로 알려져 있으며 모든 사실 F에 대해 다음과 같은 기본값을 사용하여 기본 논리로 공식화됩니다.

예를 들어, 컴퓨터 언어 Prolog는 부정을 처리 할 때 일종의 기본 가정을 사용합니다. 음의 원자를 참이 될 수 없다면 거짓으로 가정합니다. 그러나 Prolog는 소위 부정 (negation)을 실패로 사용합니다 : 인터프리터가 원자를 평가해야 할 때  , 그것은 F가 참임을 증명하려고 시도하고,  실패하면 true입니다. 기본 논리에서는 대신  양쪽 정렬은 다음 경우에만 적용될 수 있습니다.  현재의 지식과 일치합니다.

제한 사항
전제 조건이없는 경우 기본값은 범주 형 또는 전제 조건 없음입니다 (또는 동등한 조건 인 경우 전제 조건이 동어 반복 임). 결론에 해당하는 한 가지 칭의가있는 경우 기본값은 normal입니다. 그것이 범주 적이고 정상적이라면 기본값은 초자연적입니다. 모든 정당화가 결론을 수반한다면 기본값은 비정규입니다. 기본 이론은 그것이 포함 된 모든 기본값이 범주 형, 보통 형, 초신성 형 또는 비정형 형인 경우 범주 형, 보통 형, 초자연 형 또는 비정형이라고합니다.

기본 논리의 의미
기본 규칙은 그 전제 조건이 이론에 의해 수반되고 그 정당화가 모두 이론과 일치하는 경우 이론에 적용될 수있다. 기본 규칙을 적용하면 이론에 결과가 추가됩니다. 그런 다음 다른 기본 규칙이 결과 이론에 적용될 수 있습니다. 다른 부도를 적용 할 수없는 이론이 존재할 때 그 이론을 기본 이론의 확장이라 부른다. 기본 규칙이 다른 순서로 적용될 수 있으며, 이는 다른 확장자로 이어질 수 있습니다. 닉슨 다이아몬드 예제는 두 가지 확장자를 가진 기본 이론이다.

닉슨은 공화당과 퀘이커 모두이기 때문에 두 가지 기본값을 모두 적용 할 수 있습니다. 그러나 첫 번째 기본값을 적용하면 닉슨은 평화 주의자가 아니며 두 번째 기본값을 적용 할 수 없다는 결론이 도출됩니다. 같은 방식으로 두 번째 기본값을 적용하면 닉슨이 평화 주의자라는 결론을 얻을 수 있으므로 첫 번째 기본값을 적용 할 수 없습니다. 따라서이 기본 이론은 평화 주의자 (닉슨)가 참인 확장자와 평화 주의자 (닉슨)가 거짓 인 확장자의 두 가지 확장자를 갖는다.

기본 논리의 원래 의미는 함수의 고정 점을 기반으로했습니다. 다음은 동일한 알고리즘 정의입니다.기본값에 자유 변수가있는 수식이 포함되어 있으면 이러한 모든 변수에 값을 부여하여 얻은 모든 기본값 집합을 나타내는 것으로 간주됩니다. 기본값  명제 이론 T에 적용 가능하다. if  모든 이론들  일관성이있다. 이 기본값을 T에 적용하면 이론에 이르게된다.  . 다음 알고리즘을 적용하여 확장을 생성 할 수 있습니다.

  T = W / * 현재 이론 * /
 A = 0 / * 지금까지 적용된 기본값 집합 * /
 
               / * 일련의 기본값 적용 * /
 반면 에 A에없는 디폴트 d가 있고 T에 적용 가능하다.
   d의 결과를 T에 더한다.
   A에 d 추가
 
               / * 마지막 일관성 검사 * /
 만약 
   A의 모든 기본 d에 대해
     T는 d의 모든 정당화와 일치한다.
 그때
   출력 T

이 알고리즘은 주어진 이론 T에 몇 가지 기본값을 다르게 적용 할 수 있기 때문에 비 결정적입니다. Nixon 다이아몬드 예제에서 첫 번째 기본값을 적용하면 두 번째 기본값을 적용 할 수없는 이론이 생기고 그 반대의 경우도 마찬가지입니다. 그 결과 닐슨은 평화 주의자이고 닉슨은 평화 주의자가 아닌 두 확장자가 생성됩니다.

적용된 모든 불이행에 대한 정당화의 일관성에 대한 최종 점검은 일부 이론에는 확장이 없음을 의미한다. 특히 적용 가능한 기본값의 모든 가능한 시퀀스에 대해이 확인이 실패 할 때마다이 작업이 발생합니다. 다음 기본 이론에는 확장이 없습니다.

이후  배경 이론과 일치하면 기본값을 적용 할 수 있으므로 결론은  거짓입니다. 그러나이 결과는 첫 번째 불이행을 적용하기위한 가정을 훼손시킵니다. 결과적으로,이 이론은 확장이 없다.

일반적인 기본 이론에서는 모든 기본값이 정상입니다. 각 기본값은 형식을가집니다.  . 정상적인 기본 이론은 적어도 하나의 확장을 보장합니다. 더욱이, 정상 기본 이론의 확장은 상호 불일치, 즉 서로 모순된다.

함락
기본 이론은 0 개, 1 개 또는 그 이상의 확장을 가질 수 있습니다. 기본 이론에서 수식의 함축은 두 가지 방법으로 정의 할 수 있습니다.

의심 많은
공식은 모든 확장에 의해 수반되는 경우 기본 이론에 의해 수반됩니다.

잘 믿는
공식은 그것의 확장 중 적어도 하나에 의해 수반되는 경우 기본 이론에 의해 수반된다.

따라서 닉슨 다이아몬드 예제 이론은 닉슨이 평화 주의자이고 평화 주의자가 아닌 이론가 인 두 가지 확장자를 가지고있다. 결과적으로, 평화 주의자 (닉슨)도 ¬ 평화 주의자 (닉슨)도 의심의 여지없이 수반되는 반면, 두 사람은 신실하게 수반된다. 이 예에서 알 수 있듯이, 기본 이론의 끔찍한 결과는 서로 일치하지 않을 수 있습니다.

다른 기본 추론 규칙
기본 논리에 대한 다음 대체 추론 규칙은 모두 원래 시스템과 동일한 구문을 기반으로합니다.

정당화 된
원래의 값과 다르다. 그 이유는 집합 T가 적용된 기본값의 양쪽 정렬과 일치하지 않는다면 기본값이 적용되지 않는다.

간결한
기본값은 그 결과가 T에 의해 수반되지 않는 경우에만 적용됩니다 (정확한 정의는이 것보다 더 복잡합니다; 이것은 뒤에있는 주요 개념입니다).

구속 된
배경 이론, 적용된 모든 기본값의 타당성 및 모든 적용된 기본값 (이 것을 포함하여)의 결과가 일치하는 경우에만 기본값이 적용됩니다.

Rational
제약 조건이있는 기본 논리와 유사하지만 기본값 추가의 결과는 일관성 검사에서 고려되지 않습니다.

조심성 있는
적용될 수 있지만 서로 상충되는 기본값 (Nixon 다이아몬드 예제와 같은)은 적용되지 않습니다.

추론 규칙의 정당화되고 제한된 버전은 모든 기본 이론에 적어도 하나의 확장을 할당합니다.

기본 논리의 변형
기본 논리의 다음 변형은 구문과 의미 모두에서 원래의 변형과 다릅니다.

어설 션 변형
어설 션은 한 쌍입니다.  수식과 수식 집합으로 구성됩니다. 이러한 쌍은 p가 참임을 나타내며,  p가 사실임을 증명하는 일관성이 있다고 가정되었습니다. 어설 션 기본 이론은 배경 이론이라고하는 단정 이론 (assertional formula)과 원래 구문과 같이 정의 된 일련의 기본값으로 구성됩니다. 기본값이 주장 이론에 적용될 때마다 그 결과와 정당화 세트로 구성된 쌍이 이론에 추가된다. 다음의 의미들은 assertional 이론을 사용한다 :

누적 기본 논리
가정 기본 논리에 대한 약속
준 기본 논리

약한 확장
전제 조건이 배경 이론과 적용된 기본값의 결과로 구성된 이론에서 유효한지 여부를 확인하기보다는, 전제 조건이 생성 될 확장의 유효성을 검사합니다. 즉, 확장을 생성하는 알고리즘은 이론을 추측하고이를 배경 이론 대신 사용함으로써 시작됩니다. 확장 생성 과정의 결과는 처음에 추측 된 이론과 동등한 경우에만 실제로 확장입니다. 이러한 기본 논리의 변형은 원칙적으로 자기 인식 론적 논리와 관련이 있으며, 여기서 이론  x가 참이라고 가정하는 모델을 가지고있다.  사실, 수식  초기 가정을 뒷받침합니다.

분리 논리
디폴트의 ​​결과는 단일 수식 대신 수식 세트입니다. 기본값이 적용될 때마다 그 결과 중 적어도 하나는 비 결정적으로 선택되어 사실로 만들어집니다.

디폴트의 ​​우선 순위
디폴트의 ​​상대적 우선 순위가 명시 적으로 지정 될 수 있습니다. 이론에 적용 가능한 기본값 중에서 가장 선호되는 것 중 하나만 적용 할 수 있습니다. 디폴트 로직의 일부 의미는 명시 적으로 우선 순위를 지정할 필요가 없다. 오히려보다 구체적인 기본값 (소수의 경우 적용 할 수있는 기본값)이 덜 구체적인 경우보다 선호됩니다.

통계 변형
통계적 기본값은 오류 빈도에 첨부 된 상한이있는 기본값입니다. 바꾸어 말하면, 디폴트는 잘못된 추론 규칙이라고 가정합니다.

번역
기본 이론은 다른 논리의 이론으로 변환 될 수 있으며 반대의 경우도 가능합니다. 번역에 대한 다음 조건들이 고려되었습니다 :

결과 – 보존
원본과 번역 된 이론은 동일한 (명제적인) 결과를 갖는다.

충실한
이 조건은 기본 논리의 두 변형 또는 기본 논리와 확장과 비슷한 개념이 존재하는 논리 (예 : 모달 논리의 모델) 사이를 변환 할 때만 의미가 있습니다. 원본과 번역 된 이론의 확장 (또는 모델) 사이에 매핑 (전형적으로 bijection)이 존재한다면 번역은 충실합니다.

모듈 식
디폴트와 백그라운드 이론이 따로 따로 번역 될 수 있다면 디폴트 로직에서 다른 로직으로의 변환은 모듈화됩니다. 또한 배경 이론에 공식을 추가하면 변환 결과에 새로운 공식 만 추가됩니다.

동일 알파벳
원래의 이론과 번역 된 이론은 같은 알파벳으로 만들어졌다.

다항식
번역의 실행 시간 또는 생성 된 이론의 크기는 원래의 이론의 크기에서 다항식이어야합니다.

번역은 일반적으로 충실하거나 적어도 결과 보존이 요구되는 반면, 모듈성과 같은 알파벳 조건은 때때로 무시됩니다.
명제 기본 논리와 다음 논리 사이의 변환 가능성을 연구했습니다.

고전적 명제 논리;
자동 인식 논리;
준 정규 이론에 제한된 명제 기본 논리;
기본 논리의 대체 의미론;
외접.

번역은 존재하는 조건이나 부과 된 조건에 의존하지 않습니다. 명제 기본 논리에서 고전 명제 논리로의 변환은 다항식 계층 구조가 붕괴되지 않는 한 항상 다항식 크기의 명제 논리를 생성 할 수 없습니다. 자동 인식 논리에 대한 번역은 모듈성 또는 동일한 알파벳의 사용이 필요한지 여부에 달려 있습니다.

복잡성
기본 논리에 대한 다음과 같은 문제의 계산 복잡성이 알려져 있습니다.

확장 기능의 존재
명제 적 기본 이론에 적어도 하나의 확장이 존재 하는지를 결정하는 것  -완전한;

회의적 함축
명제 불이행 이론이 회의론 적으로 명제식을 수반하는지 여부를 결정하는 것은  -완전한;

신중한 함의
명제적인 기본 이론이 명 제적으로 명제식을 수반하는지 여부를 결정하는 것은  -완전한;

확장 검사
명제식이 명제 기본 이론의 확장과 동등한지를 결정하는 것은  -완전한;

모델 검사
명제 해석이 명제 기본 이론의 확장 모델인지 여부를 결정하는 것은  -완전한.

구현
기본 논리를 구현하는 세 가지 시스템은 DeReS [영구 죽은 링크], XRay 및 GADeL입니다.