SLD 분해능

SLD 분해능(Selective Linear 한정된 절 분해능)은 논리 프로그래밍에 사용되는 기본 추론 규칙이다. Horn 절에 대해 음성과 리퓨테이션이 모두 완료된 분해능의 정교함이다.

SLD 추론 규칙

해결해야 할 문제의 부정으로 대표되는 목표 조항이 주어진다.

${\displaystyle \neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_}}}}$

선택된 리터럴 L${\displaystyle \mathrm{}{i}_{}}$ ${\$$i}$ 및 입력 한정 조항:

${\displaystyle L\lor \neg K_{1}\lor \cdots \lor \neg K_{m}}$

그 양의 리터럴 $L{\displaystyle }${\$displaystyle$ L$\,}$은(는) 선택된 리터럴의${\displaystyle \mathrm{}{i}_{}}$ L i${\displaystyle {}_{}}$$displaystyle L_{i$ 원자와 통합되며, SLD 분해능은 입력 절의 마이너스 리터럴과 하위 리터럴로 대체되는 또 다른 목표 절을 도출한다.itution $\theta {\displaystyle }$ ${\$이(가) 적용됨$$:

${\displaystyle(\neg L_{1}\lor \cdots \lor \neg K_{1}\lor \cdots \lor \cdots \lor \lor \neg L_{n}\ta }$

가장 간단한 경우, 명제 논리에서는 원자 ${\displaystyle L_{}}$ $i{\displaystyle {}_{}}$ $displaystyle$ L_{$i}\,}$와 L$$ ${\$이(가) 동일하며$$, 단일 대체 $substitution{\displaystyle }$ ${\$은(는) 비어 있다$$. 그러나 보다 일반적인 경우, 두 리터럴을 동일시하기 위해서는 통일적 대체가 필요하다.

"SLD" 이름의 유래

"SLD 결의안"이라는 이름은 로버트 코왈스키가 도입한 이름 없는 추론 규칙에 대해 마아텐 판 엠덴이 붙인 이름이다.^[1] 그 이름은 SL 해상도에서 유래되었는데,^[2] 이는 제한되지 않은 형태의 논리 정리에 대해 음향과 재설정이 모두 완료된 것이다. "SLD"는 "확정 조항이 있는 SL 해상도"를 의미한다.

SL과 SLD 모두에서 "L"은 분해능 증명이 다음과 같은 조항들의 선형 순서에 제한될 수 있다는 사실을 의미한다.

${\displaystyle C_{1},C_{2},\cdots,C_{l}}$

where the "top clause" ${\displaystyle C_{1}\,}$ is an input clause, and every other clause ${\displaystyle C_{i+1}\,}$ is a resolvent one of whose parents is the previous clause ${\displaystyle C_{i}\,}$. The proof is a refutation if the last clause ${\displaystyle C_{l}\,}$ is the empty 조항

SLD에서, 시퀀스의 모든 조항은 목표 조항이며, 다른 상위 조항은 입력 조항이다. SL 분해능에서 다른 상위 항목은 입력 절이거나 시퀀스 초반의 상위 절이다.

SLD와 SLD에서 모두 "S"는 C ${\displaystyle i_{}{}_{}}${\$displaystyle C_{i}\,}$에서 확인된 유일한 리터럴이$$ 선택 규칙이나 선택 함수에 의해 고유하게 선택된다는 사실을 의미한다. SL 분해능에서 선택한 리터럴은 조항에 가장 최근에 도입된 리터럴로 제한된다. 가장 간단한 경우, 그러한 최종 선입선출 선택 함수는 프롤로그에서와 같이 리터럴을 쓰는 순서에 따라 지정할 수 있다. 단, SLD 분해능의 선택기능은 SLD 분해능과 Prolog의 선택기능보다 일반적이다. 선택할 수 있는 문자에는 제한이 없다.

SLD 분해능의 계산적 해석

폐쇄 논리학에서, SLD 반박은 조항의 입력 집합이 만족스럽지 못함을 증명한다. 그러나 로직 프로그래밍에서 SLD 리퓨테이션은 계산적 해석도 가지고 있다. The top clause ${\displaystyle \neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}}$ can be interpreted as the denial of a conjunction of subgoals ${\displaystyle L_{1}\land \cdots \land L_{i}\land \cdots \land L_{n}}$. ${\displaystyle {Ci}_{}}$ $displaystyle C_{i}\$에서 ${\displaystyle {\mathrm{조항}}_{}}$ C ${\displaystyle i_{}}$+ 1 $displaystyle C_{i}\,}$의 파생은 입력 절을 목표 감소 절차로 사용하는 새로운 하위 골의 집합의 역추론에 의해 파생된 것이다$$. 단일 대체 $\theta {\displaystyle }$ ${\$은(는) 모두 선택한 하위골격에서 절차 본문으로 입력을 전달하고 동시에 절차의 머리에서 선택되지 않은 나머지 하위골격으로 출력을 전달한다. 빈 절은 단순히 빈 하위 골 세트로, 상위 절에 있는 하위 골의 초기 결합이 해결되었음을 알리는 신호다.

SLD 해결 전략

SLD 분해능은 대체 계산의 검색 트리를 암묵적으로 정의하는데, 이 트리의 루트에는 초기 목표 조항이 연관되어 있다. 트리의 모든 노드와 프로그램의 모든 한정된 절에 대해 그리고 노드와 관련된 목표 절에서 선택된 리터럴과 양성 리터럴이 통일되는 프로그램의 모든 한정된 절에 대해, SLD 분해능으로 얻은 목표 절과 연관된 하위 노드가 있다.

자녀가 없는 리프 노드는 관련 목표 조항이 빈 조항이라면 성공 노드다. 관련 목표 조항이 비어 있지 않지만 선택된 문자 그대로가 프로그램에서 특정 조항의 긍정적인 리터럴 없이 통일되는 경우 이는 실패 노드다.

SLD 해상도는 검색 트리 탐색을 위한 검색 전략을 결정하지 않는다는 점에서 결정적이지 않다. 프롤로그는 장애 노드와 마주쳤을 때 역추적을 사용하여 트리 깊이를 먼저 한 번에 하나씩 검색한다. 깊이 우선 검색은 컴퓨팅 자원의 사용에 있어서 매우 효율적이지만, 검색 공간에 무한한 분기가 포함되어 있고 검색 전략이 유한 분기에 우선하여 이들을 검색한다면 불완전하다: 계산이 종료되지 않는다. 범위 우선, 베스트 우선, 지점 및 바인딩 검색 등 다른 검색 전략도 가능하다. 더구나 한 번에 한 노드씩 순차적으로, 또는 동시에 여러 노드를 동시에 검색할 수 있다.

SLD 해상도 역시 앞에서 언급한 바와 같이 선택 규칙은 추론 규칙에 의해 결정되는 것이 아니라 별도의 의사결정 절차에 의해 결정되어 프로그램 실행 과정의 역학관계에 민감할 수 있다는 의미에서 비결정론적이다.

SLD 해상도 검색 공간은 다른 분기가 대체 연산을 나타내는 오트리다. 명제 논리 프로그램의 경우, SLD를 일반화하여 검색 공간을 및/또는 트리로 만들 수 있으며, 이 트리의 노드는 단일 리터럴로 표시되고 하위 골격을 나타내며, 노드는 접속사 또는 분리에 의해 결합된다. 일반적으로 결합 하위 골이 변수를 공유하는 경우 및/또는 트리 표현이 더 복잡하다.

예

논리 프로그램 지정 시:

q :- p. p. 

그리고 최상위 목표:

q. 

검색 공간은 단일 분기로 구성되며, 검색 공간은 q 로 전락하다 p 빈 하위 골 집합으로 축소되어 성공적인 연산을 나타낸다. 이 경우 프로그램은 선택 기능에 대한 역할이 없고 검색도 필요 없을 정도로 단순하다.

폐쇄 논리에서 프로그램은 다음과 같은 조항으로 표현된다.

$\displaystyle q\lor \neg p}$

$p\displaystyle p\,}$

최상위 목표는 단일 음의 리터럴로 목표 조항으로 표현된다.

$\displaystyle \neg q}$

검색 공간은 단일 refutation으로 구성된다.

${\displaystyle \neg q,\neg p, {\mathit {false}}$

여기서 $f{\displaystyle \mathit{}}$ ${\displaystyle \mathit{l}}$ ${\displaystyle \mathit{s}}$ ${\displaystyle \mathit{e}}$ $displaystyle {\mathit {false}\,}$은(는) 빈 절을 나타낸다$$.

프로그램에 다음 조항이 추가된 경우:

q :- r. 

그러면 검색 공간에 추가 분기가 있을 것이고, 그 분기의 리프 노드는 r 장애 노드. 프롤로그에서 만약 이 조항이 원래 프로그램 전면에 추가되었다면, 프롤로그는 검색 공간의 분기가 조사되는 순서를 결정하기 위해 조항이 쓰여지는 순서를 사용하게 된다. 프롤로그는 먼저 이 새로운 분기를 시도하고, 실패하여, 원래의 프로그램의 단일 분기를 조사하여 성공하게 된다.

만약 그 조항이

p :- p. 

이제 프로그램에 추가되었고, 그러면 검색 트리는 무한 분기를 포함할 것이다. 만약 이 조항이 먼저 시도되었다면 프롤로그는 무한 루프에 빠져서 성공적인 지점을 찾지 못할 것이다.

SLDNF

SLDNF는^[3] 부정을 실패로 처리하기 위한 SLD 해상도의 확장이다. $SLDNF$에서 목표 절에는 고장이 발생한 $리터럴$로 부정이 포함될 수 있으며, 이는 변수가 $없는{\displaystyle }$ $경우$에만 선택할 수 있다$.$ 그러한 가변 없는 리터럴을 선택할 때, 상위 조항으로$$ 해당하는 비순수 리터럴 $p{\displaystyle }$ ${\$ p$\,}$에서 시작되는 SLDNF 리퓨테이션이 있는지 여부를 결정하기 위한 하위 컴퓨터(또는 하위 컴퓨터)가 시도된다. 선택한 하위 골(${\displaystyle \mathrm{no}}$ ${\displaystyle t}$(${\displaystyle p}$) ${\$ 서브 프루프가 실패하면 성공하고$$, 서브 프루프가 성공하면 실패한다.

참고 항목

• 존 앨런 로빈슨

참조

• 컴퓨터 과학을 위한 논리학 9장 SLD-해상도 및 논리 프로그래밍: 자동 정리 증명의 기초, 2003년 온라인 개정판(무료 다운로드), 원래 Wiley에 의해 출판된 1986년
• 존 C. 셰퍼드슨, SLDNF-Defolution with Equality, Journal of Automated Fraction 8: 297-306, 1992; 동등성을 가진 SLDNF-해상도 건전하고 완전한 의미론 정의

외부 링크

• [1] 무료 온라인 컴퓨팅 사전의 정의