로어유닛

증명 압축에서 LowerUnits(LowerUnits)는 명제 논리 분해능 증명 압축에 사용되는 알고리즘이다.LowerUnits의 주요 아이디어는 다음과 같은 사실을 이용하는 것이다.^[1]

정리: $\varphi$   $\varphi$ 을(를) 잠재적으로 중복되는 증명이 되도록 $\varphi$  하고,  $\eta$   $\eta$ 을 $\eta$ (를) 중복되는 증명이 되도록 한다. $\displaystyle \eta }$ 의 $\eta$ s 절이 단위 절이면  $\varphi$   $\varphi$ 은(는) 중복된다 $\varphi$ .

알고리즘은 단위 절이 있는 복수 분해능에서 기인하는 전역 중복성 등급을 정확히 대상으로 한다.알고리즘은 이 재작성이 완료되고 그 결과 입증 자료가 DAG(직접적인 애시클릭 그래프)로 표시될 때 단위 노드 $\eta$ 이 $\eta$ (가) 원래 증명에 나타나던 것보다 더 낮게(즉, 루트에 더 가깝게) 나타난다는 사실에서 그 이름을 따온 것이다.

정리를 이용하는 순진한 구현은 각 단위 노드를 낮춘 후에 증거를 통과하고 수정해야 할 것이다.그러나 한 번의 트래버설에서 먼저 모든 장치 노드를 수집하고 제거한 다음, 한 번의 트레버설로 전체 증거를 고정함으로써 더 나은 작업을 할 수 있다.마지막으로 수집된 고정 장치 노드는 증빙 하단에 다시 삽입해야 한다.

Care must be taken with cases when a unit node $\eta ^{\prime }$ occurs above in the subproof that derives another unit node $\eta$ . In such cases, $\eta$ depends on $\eta ^{\prime }$ . Let $\ell$ be the single liter ${\$ 의 단위 절의 al $\eta ^{\prime }$ 그러면 $\eta ^{\prime }$ $\eta }}$ 위에 있는 방호벽에 있는 ${\overline {\ell }}$ ${\overline {\ell }}$ ${\$ 의 어떠한 발생도 $\eta ^{\prime }$ η에 $\eta ^{\prime }$ 의한 해결 추론으로도 취소되지 않을 것이다 $\eta$ .이에 따라 ${\$ 은(는) 증빙이 고정되면 아래쪽으로 $\eta$ 되어 $\{\displaystyle \eta}$ 의 절에 나타나게 ${\overline {\ell }}$ 된다. $\eta$ $\eta ^{\prime }$ 을 다시 삽입한 $\eta ^{\prime }$ 후 상위 단위 노드 ${{$ 을 다시 삽입하면 이러한 의존성을 가진 어려움을 쉽게 피할 수 있다.nit 노드 ${\$ $displaystyle \eta$ $\eta$ }( $\eta$ 즉, 다시 삽입한 $\eta ^{\prime }$ $\$ {\ $displaystyle$ $\eta$ ^{\ $prime$ $\eta$ 아래에 나타나야 $\eta ^{\prime }$ $\eta$ ${\$ $displaystyle$ $\eta$ 의 $\overline {\ell }$ 추가 리터럴터럴터럴트럴을 취소할 수 있다.이는 증빙의 상향 이동 중에 대기열에 장치 노드를 수집하고 대기열에 있는 순서대로 다시 삽입함으로써 보장할 수 있다.

많은 루트가 포함된 증거를 수정하기 위한 알고리즘은 증명의 하향 횡단을 수행하고, 생존 부모(예: 다른 부모)에 의해 분해제를 다시 계산하고 손상된 노드(예: 부모 중 하나로서 노드 삭제)를 대체한다.

단위 노드를 수집하여 조항 $\kappa$ $\kappa$ 의 증빙에서 제거하고 $\kappa$ 그 증빙이 고정되면, 새로운 증빙의 루트 노드에 있는 $\kappa ^{\prime }$ $\kappa$ $\kappa ^{\prime }$ κ ${\$ $kappa$ $^{\prime}}$ 조항은 더 이상 $\kappa$ some ${\displaystystylement }$ 과 같지 않지만 (일부) 단위 절의 리터럴이 포함되어 있다.증거에서 삭제되었다.증명 하단에 있는 단위 노드를 다시 삽입하면 수집된 단위 노드 중 (일부)의 조항으로 $\kappa ^{\prime }$ ${\$ 이(가) 해결되어 $\kappa$ $\kappa }$ 의 증거를 다시 $\kappa$ 얻는다.

알고리즘.

알고리즘의 일반 구조

알고리즘 LowerUnits 입력: 증명  $\psi$   $\psi$  출력 $\psi$ : $\psi ^{\prime }$  중복 노드가 있는 글로벌 이중화가 없는 $\psi ^{\prime }$  증거 ${{\$

(unitsQueue,  $\psi _{b}$ ) ← collectUnits( $\psi$ );     $\psi _{f}$  ← fix( $\psi _{b}$ );    fixedUnitsQueue ← fix(unitsQueue);     $\psi ^{\prime }$  ← reinsertUnits( $\psi _{f}$ ,FixedUnitsQueue); 반환  $\psi ^{\prime }$  {\ $displaystyle \psi$ ^{\ $prime }$ ;

"직접"은 할당을 의미한다.예를 들어, "가장 큰 ←항목"은 가장 큰 값이 항목의 가치를 변화시킨다는 것을 의미한다.
"return"은 알고리즘을 종료하고 다음 값을 출력한다.

다음과 같이 단위 조항을 수집한다.

알고리즘 수집유닛 입력: :  $\psi$   $\psi$  출력 $\psi$ : $\psi$   $\psi$ 에서 두 번 이상 사용되는 모든 장치 노드(unitsQueue)의 대기열과 $\psi$  파손된 증빙  $\psi _{b}$  b  ${\$ 이(가) 포함된 쌍.

 $\psi _{b}$  ←  $\psi$ ;  traverse  $\psi _{b}$  bottom-up and foreach node  $\eta$  in  $\psi _{b}$  do if  $\eta$  is unit and  $\eta$  has more than one child then $\eta$   $\eta$ 을(를) 장치에 추가대기열 $\eta$ ; $\eta$  $\psi _{b}$   $\psi _{b}$   ${\$  엔드 엔드 리턴(unitsQueue,  $\psi _{b}$   $\psi _{b}$   ${\$

"직접"은 할당을 의미한다.예를 들어, "가장 큰 ←항목"은 가장 큰 값이 항목의 가치를 변화시킨다는 것을 의미한다.
"return"은 알고리즘을 종료하고 다음 값을 출력한다.

그런 다음 유닛을 다시 삽입한다.

알고리즘 재퍼트유닛 입력:  $\psi _{f}$   $\psi _{f}$   ${\$ 단일 루트로) 및 루트 노드의 $q$  대기열  $q$   $q$  출력:증명서  ${\$ }}}

 $\psi ^{\prime }$  ←  $\psi _{f}$ ;  while  $q\neq \emptyset$  do  $\eta$  ← first element of  $q$ ;      $q$  ← tail of  $q$ ;     if  $\eta$  is resolva ${\$  $prime$   $}}$ 을(를) 뿌리로 표백한 다음 $\psi ^{\prime }$  $\psi ^{\prime }$  $\psi ^{\prime }$   ${\displaystyle \$  $eta$  $}}$ 을 $($ 를 $)$  뿌리째 $\eta$  뽑은 후 $\psi ^{\prime }$  $\psi ^{\prime }$  $\psi ^{\prime }$ {\ $displaystyle$ \ \ $\psi ^{\prime }$  $\premium$ 을(를 $\psi ^{\prime }$ 로 하여  $\psi ^{\prime }$  $displaystatestatestatestatestate{\$ discla stypres)을(으)을(으)로 한다.

"직접"은 할당을 의미한다.예를 들어, "가장 큰 ←항목"은 가장 큰 값이 항목의 가치를 변화시킨다는 것을 의미한다.
"return"은 알고리즘을 종료하고 다음 값을 출력한다.

메모들

^ 퐁텐, 파스칼, 메르스, 스테판, 울첸로겔 팔레오, 브루노.부분적 정규화를 통한 제안 결의안 증명 압축. 제23회 자동 공제 국제 회의, 2011.

[1] 퐁텐, 파스칼, 메르스, 스테판, 울첸로겔 팔레오, 브루노.부분적 정규화를 통한 제안 결의안 증명 압축. 제23회 자동 공제 국제 회의, 2011.

[1]

Search

로어유닛

네임스페이스

더

알고리즘.

메모들