대체(로직)

Substitution (logic)

대체는 논리학의 기본 개념이다.치환은 형식 표현식의 구문 변환입니다.표현식에 대체를 적용하는 것은 변수 또는 자리 표시자를 다른 표현식으로 일관되게 대체하는 것을 의미합니다.결과 표현식은 원래 표현식의 대체 인스턴스 또는 줄여서 인스턴스라고 불립니다.

명제논리

정의.

여기서 and 및 represent는 명제논리의 공식이며, ,의 기호들을 in의 공식으로 치환하여 by에서 may를 구할 수 있는 경우에만 ution의 치환 예이며, 동일한 기호의 각 발생을 동일한 공식의 발생으로 치환한다.예를 들어 다음과 같습니다.

(R → S) 및 (T → S)

는 다음 대체 인스턴스입니다.

P&Q

그리고.

(A ↔ A) ↔ (A ↔ A)

는 다음 대체 인스턴스입니다.

(A ↔ A)

명제논리를 위한 일부 감점시스템에서는 파생상품의 이전 행의 치환 인스턴스일 경우 파생상품의 행에 새로운 표현(명제)을 입력할 수 있다(Hunter 1971, 페이지 118).이것이 일부 자명한 시스템에서 새로운 행이 도입되는 방법입니다.변환규칙을 사용하는 시스템에서 규칙은 특정 변수를 파생상품에 도입할 목적으로 대체 인스턴스의 사용을 포함할 수 있다.

1차 논리에서는 열린 명제식 θ로부터 치환에 의해 얻을 수 있는 모든 닫힌 명제식을 θ의 치환 인스턴스라고 한다.만약 θ가 닫힌 명제식이라면 우리는 θ 자체를 그것의 유일한 치환 사례로 간주한다.

토우토로지

명제 공식은 술어 기호의 모든 평가(또는 해석)에서 참일 경우 동치이다.δ가 쌍방향성이고 δ가 δ의 치환 인스턴스인 경우 δ는 다시 쌍방향성입니다.이 사실은 앞 절에서 설명한 공제 규칙의 건전성을 암시한다.

1차 논리

1차 논리학에서 치환이란 변수에서 항으로의 총 매핑 θ: V → T이다.[1]: 73 [2]: 445 많은 것들이지만 모든 저자들이 완전히 많은 변수 x에 대해 추가로 θ(x) = x를 요구하는 것은 아니다[3]: 250 .{ x1 t1 t, …, xk tk t }[note 1] 표기법은 각 변수 x를 대응하는 항 t에 매핑하는 치환을 말합니다. i=1, …, k 및 기타 모든 변수는 그i 자체로i 구분되어야 합니다. x는 쌍으로i 구분되어야 합니다.용어 t에 대한 치환 적용은 postfix 표기로 t { x1 t1 t, ..., xk tk t }로 표기되어 있다.이것은 (동시에) t의 각i x의 발생을 [note 2]t로i 치환하는 것을 의미한다.항 t에 치환 θ를 적용한 결과 tθ를 해당 항 t의 인스턴스라고 한다.예를 들어, { x , z, z ( h(a,y)} 치환 적용

f( z , a, g( x ), y) 수율
f( h(a, y) , a, g( z ), y) .

치환 θ의 도메인 dom(dom)은 일반적으로 실제로 치환된 변수 집합으로 정의된다. 즉, dom(dom) = { x ∈ V x x x x x }.그 영역의 모든 변수를 그라운드에 매핑하는 경우, 즉 변수가 없는 항을 그라운드 치환이라고 한다.그라운드 치환의 치환 인스턴스 tθ는 모든 t의 변수가 θ의 영역에 있는 경우, 즉 vars(t) θ dom(θ)인 경우 그라운드 항이다.치환 θ가 θ의 영역의 변수를 정확하게 포함하는 일부(따라서 모든) 선형 항 t에 대한 선형 항인 경우, 즉 vars(t) = dom(dom)을 갖는 경우, 치환 θ를 선형 치환이라고 한다.x가 변수 x마다 변수인 경우 치환 θ를 플랫 치환이라고 하고, 모든 변수 집합의 치환인 경우 치환 θ를 이름 바꾸기 치환이라고 합니다.모든 치환과 마찬가지로, 이름 바꾸기 치환 θ는 항상 역치환 θ를−1 가지며, 따라서 모든 항 t에 대해 tθ−1 = t= tθ이다−1.단, 임의의 치환에 대해서는 역치환을 정의할 수 없습니다.

예를 들어,{)↦ 2, y ↦ 3+4} 않는 지상 대체 내용은{)↦ x1, y↦ y2+4}과 비평 판형지만, 선형,{)↦ y2, y↦ y2+4}과 비평 판형 비선형적인,{)↦ y2, y↦ y2}가 평평하지만, 비선형,{)↦ x1, y↦ y2}은 평평한 것은 아니지만 선형은 개명,non-ground은 이후 매핑 둘 다는 y와 y2에 y2;쿠키의 이러한 대체품을 사용하고 있는 집합.{x, y}로도메인입니다.이름 변경 대체의 예로는 { x x1 x, x1 y y, y y2 y, y2 y x}가 있습니다.이 예에는 역 { x y2 y, y2 y y, y y1 x, x1 }가 있습니다.평탄 치환 { x z z, y z z }은(는) 역수를 가질 수 없습니다. 예를 들어, (x+y) { x , z, y z z } = z+z이므로, z의 유래에 대한 정보가 손실되므로, 후자의 항은 x+y로 다시 변환할 수 없습니다.지반 치환 { x 2 2 }은(는) 유사한 원점 정보 손실 때문에 역수를 가질 수 없습니다. 예를 들어, 변수에 의한 상수 치환이 "일반화된 치환"의 어떤 가상 유형에 의해 허용되었더라도 말입니다.

두 가지 치환은 각 변수를 구조적으로 동일한 결과 항에 매핑하는 경우 동일한 것으로 간주됩니다. 공식적으로는 각 변수 x each V에 대해 = = x x x = x two for two 。두 개의 치환 = { x1 t1 t, …, xk ↦ tk } 및 τ = { y1 , u1, …, yl ↦ ul }의 구성은 { x1 t1 t,, …, xk ↦ t,, y1 , uk, …, yl u1l u }의ii 치환에서 제거하여 얻을 수 있습니다. 이 쌍들은i {x }에1 대해 {x u, …, …}입니다k.and과 is의 구성은 τ로 나타낸다.합성은 연상연산으로 치환적용, 즉 (으)ㄹ=(으)ㄹ=(으)ㄹ=t(으)ㄹ=t(으)를 각각 치환적용과 호환된다.모든 변수를 자신에게 매핑하는 아이덴티티 치환은 치환 구성의 중립 요소입니다.치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환치환1 { x t1 t, …, xk tk t }은 변수i x가 t에서i 발생하지 않는 경우에만 유효합니다.치환조성은 치환성이 아니다.즉, comp과 are가 [1]: 73–74 [2]: 445–446 등가성이라도 σ과 다를 수 있다.

예를 들어 { x 2 2, y 3 3+4 }은(는) { y 3 3+4, x 2 2 }와 같지만 { x 2 2, y 7 7 }과는 다릅니다.치환 { x + y+y }은(는) idempotent(예: (x+y) {xxxy+y} = (y+y)+y)는 non-idempotent(x+y)입니다.예를 들어 { x non y } { y z z } = { x ↦ z, y z z }이지만 { y }, z} { x y y } = { x ↦ y, y z z } 입니다.

「 」를 참조해 주세요.

메모들

  1. ^ 일부 저자는 [t1/x1, …, tk/xk]를 사용하여 치환을 나타냅니다.M. Wirsing (1990). Jan van Leeuwen (ed.). Algebraic Specification. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 675–788., 여기: 페이지 682;
  2. ^ 용어 대수의 관점에서, 항의 집합 T는 변수의 집합 V에 걸친 자유항 대수이므로, 각 치환 매핑 θ: V → T에 대한 θ와 일치하는 고유한 동형사상 θ: T → T가 존재한다. 그 후, 항 t에 대한 θ의 위에서 정의된 적용은 함수 t에 적용되는 것으로 간주된다.

레퍼런스

  1. ^ a b David A. Duffy (1991). Principles of Automated Theorem Proving. Wiley.
  2. ^ a b Franz Baader, Wayne Snyder (2001). Alan Robinson and Andrei Voronkov (ed.). Unification Theory (PDF). Elsevier. pp. 439–526.
  3. ^ N. Dershowitz; J.-P. Jouannaud (1990). "Rewrite Systems". In Jan van Leeuwen (ed.). Formal Models and Semantics. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320.

외부 링크