어카운트 오더

이론 컴퓨터 과학에서, 특히 자동화된 정리 증명과 용어 재작성에 있어서, 격납 또는 포괄,^[1] 용어의 집합에 관한 사전 주문(사전 주문)은 다음에^[2] 의해 정의된다.

s s t의 하위 항이 s의 대체 인스턴스인 경우 t.

Knuth-Bendix 완료 알고리즘에서와 같이 사용된다.

특성.

• 아포메이션은 사전 순서, 즉 반사적, 전이적, 반대칭적,^{[note 1]} 총체적^{[note 2]} 순서로 되어 있지 않다.
• s ~ t로 정의되는 해당 동등성 관계는 s ≤ t ≤ s인 경우 동등성 modulo 이름 변경이다.
• s s는 t의 부항일 때마다 t가 된다.
• s substitution t는 s의 대체 인스턴스일 때마다 t이다.
• 근거가 충분한 모든 재작성 명령 R과^{[note 3]} (<)의 결합은 근거가 충분하며, 여기서 (<)는 ()의 불손한 알맹이를 나타낸다.^[3]특히 (<) 그 자체가 근거가 충분하다.

메모들

참조