재작성

"오늘의AI위키"는 AI 기술로 일관성 있고 체계적인 최신 지식을 제공하는 혁신 플랫폼입니다.
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.

1. 개요

재작성은 논리학, 산술, 언어학, 컴퓨터 과학 등 다양한 분야에서 사용되는 개념으로, 표현식이나 규칙을 다른 형태로 변환하는 과정을 의미한다.

논리학에서는 명제 논리식을 결합 정규형으로 변환하는 데 사용되며, 이중 부정 제거, 드 모르간의 법칙, 분배 법칙 등이 재작성 규칙으로 활용된다. 산술에서는 자연수의 합과 곱을 계산하는 데 항 재작성 시스템이 사용되며, 언어학에서는 문법적으로 올바른 문장을 생성하기 위한 구조 규칙, 즉 재작성 규칙이 생성 문법 체계에서 활용된다. 추상 재작성 시스템(ARS)은 객체 집합과 재작성 규칙으로 구성되며, 문자열 재작성 시스템(SRS)은 알파벳 위의 문자열을 재작성하는 시스템으로, 모노이드의 표현과 관련이 있다. 항 재작성 시스템(TRS)은 중첩된 하위 표현식을 가진 항을 대상으로 하며, 튜링 머신의 모든 능력을 갖는다. 이 외에도 고차 재작성 시스템, 그래프 재작성 시스템, 추적 재작성 시스템 등이 존재하며, 크누스-벤딕스 완비화 알고리즘은 항 재작성 시스템을 합류성을 만족하는 시스템으로 변환하는 데 사용된다.

더 읽어볼만한 페이지

재작성 시스템 - 합류성
합류성은 재작성 시스템 이론에서 초기 상태에서 여러 재작성 규칙을 적용했을 때 최종 결과가 동일함을 보장하는 속성으로, 시스템의 동작 예측 가능성과 관련되며 항 재작성 시스템에서 규칙 적용 순서에 관계없이 동일한 정규형으로 수렴하는 것을 의미한다.
재작성 시스템 - 항 (논리학)
항(논리학)은 변수, 상수, 함수 기호로 재귀적으로 정의되는 구문 요소로서, 담론 영역에서 수학적 객체를 나타내며 트리 구조, 구조적 동일성, 기저항, 선형항 등의 속성을 가지고, 항 연산을 통해 부분항 대체, 깊이 측정, 패턴 매칭 등이 가능하다.
빈 문단이 포함된 문서 - 광주고등법원
광주고등법원은 1952년에 설치되어 광주광역시, 전라남도, 전북특별자치도, 제주특별자치도를 관할하며, 제주와 전주에 원외재판부를 두고 있다.
빈 문단이 포함된 문서 - 1502년
1502년은 율리우스력으로 수요일에 시작하는 평년으로, 이사벨 1세의 이슬람교 금지 칙령 발표, 콜럼버스의 중앙아메리카 해안 탐험, 바스쿠 다 가마의 인도 상관 설립, 크리미아 칸국의 킵차크 칸국 멸망, 비텐베르크 대학교 설립, 최초의 아프리카 노예들의 신대륙 도착 등의 주요 사건이 있었다.

재작성
개요
유형	계산 모델
분야	수학 전산학
상세 정보
하위 개념	그래프 변환 문자열 재작성
관련 개념	추상 재작성 시스템 오토마타 이론 람다 대수 마르코프 알고리즘 튜링 완전성 처치-튜링 테제

2. 논리학에서의 재작성

논리학에서 재작성은 명제 논리식을 결합 정규형(CNF)으로 변환하는 과정 등에 사용된다.^[6] ( $\to$ ) 기호는 좌측 규칙이 우측 규칙으로 재작성 가능함을 나타낸다.

2. 1. 논리식의 재작성 규칙

논리학에서 논리식을 재작성하는 데 사용되는 대표적인 규칙으로 이중 부정 제거, 드 모르간의 법칙, 분배 법칙이 있다.^[6]^[7]

여기서 (

\to

) 기호는 좌측의 규칙을 우측의 규칙으로 재작성할 수 있음을 나타낸다. 이러한 시스템에서 재작성은 좌측의 규칙을 우측의 규칙으로 해석하는 논리적 작동이다. 각 규칙은 왼쪽과 오른쪽이 논리적 동치가 되도록 선택되므로, 왼쪽 하위 표현식과 일치하는 경우 해당 하위 표현식을 오른쪽으로 재작성하여도 전체 표현식의 논리적 일관성과 값은 유지된다.

2. 1. 1. 이중 부정 제거

:

\neg \neg A \to A

(\[\[이중 부정 제거]])^[6]^[7]

2. 1. 2. 드 모르간의 법칙

:

\neg(A \land B) \to \neg A \lor \neg B

(드 모르간의 법칙)

:

\neg(A \lor B)  \to \neg A \land\neg B

^[6]^[7]

2. 1. 3. 분배 법칙

:

(A \land B) \lor C \to (A \lor C) \land (B \lor C)

(분배 법칙)

:

A \lor (B \land C) \to (A \lor B) \land (A \lor C)

^[6]^[7]

3. 산술에서의 재작성

항 재작성 시스템은 자연수에 대한 산술 연산을 계산하는 데 사용될 수 있다.^[8] 이를 위해 각 숫자는 항으로 인코딩되어야 한다. 가장 간단한 인코딩 방식은 페아노 공리에서 사용되는 방식으로, 상수 0(영)과 후계자 함수 ''S''를 기반으로 한다.

예를 들어, 2+2를 계산하여 4가 되는 것은 다음과 같이 항 재작성을 통해 나타낼 수 있다.

: $S(S(0)) + S(S(0))$ $\stackrel{(2)}{\to}$ $S( \; S(S(0)) + S(0) \; )$ $\stackrel{(2)}{\to}$ $S(S( \; S(S(0)) + 0 \; ))$ $\stackrel{(1)}{\to}$ $S(S( S(S(0)) ))$

여기서 규칙 번호는 ''~으로 재작성'' 화살표 위에 주어져 있다.

또 다른 예로, 2⋅2의 계산은 다음과 같다.

: $S(S(0)) \cdot S(S(0))$ $\stackrel{(4)}{\to}$ $S(S(0)) + S(S(0)) \cdot S(0)$ $\stackrel{(4)}{\to}$ $S(S(0)) + S(S(0)) + S(S(0)) \cdot 0$ $\stackrel{(3)}{\to}$ $S(S(0)) + S(S(0)) + 0$ $\stackrel{(1)}{\to}$ $S(S(0)) + S(S(0))$ $\stackrel{\textrm{s.a.}}{\to}$ $S(S( S(S(0)) ))$

여기서 마지막 단계는 이전 예제 계산을 포함한다.

일반적인 산술 규칙은 다음과 같은 규칙을 포함하는 항 재작성 시스템으로 간주할 수 있다.

: $\mathrm{plus}(a, b) \rightarrow a + b$

: $\mathrm{times}(a, b) \rightarrow a \times b$

여기서 ''a''+''b''는 ''a''와 ''b''의 덧셈을 의미하며, ''a'' × ''b''는 ''a''와 ''b''의 곱셈을 의미한다. 이하에서는 plus(''a'', ''b'')를 ''a''+''b''로 표기하고, times(''a'', ''b'')를 ''a'' × ''b''로 표기한다.

$(11 + 9) \times (2 + 4)$ 와 같은 식이 있다고 가정할 때, 이 식을 재작성하는 방법은 두 가지가 있다. 첫 번째 괄호 안을 단순화하거나, 두 번째 괄호 안을 단순화하는 것이다. 첫 번째 괄호 안을 먼저 항 재작성으로 단순화하면 $20 \times (2 + 4) = 20 \times 6 = 120$ 이 되고, 두 번째 괄호 안을 먼저 단순화하면 $(11 + 9) \times 6 = 20 \times 6 = 120$ 이 된다.

3. 1. 페아노 공리

가장 간단한 페아노 공리에서의 숫자 인코딩은 상수 0(영)과 후계자 함수 ''S''를 기반으로 한다. 예를 들어, 숫자 0, 1, 2, 3은 각각 항 0, S(0), S(S(0)), S(S(S(0)))으로 표시된다.^[8]

3. 2. 산술 연산 규칙

다음은 주어진 자연수의 합과 곱을 계산하는 데 사용될 수 있는 항 재작성 시스템이다.^[8]

식	설명
A + 0 → A	(1)
A + S(B) → S (A + B)	(2)
A ⋅ 0 → 0	(3)
A ⋅ S(B) → A + (A ⋅ B)	(4)

4. 언어학에서의 재작성

언어학에서, 구조 규칙 또는 '''재작성 규칙'''은 일부 생성 문법 체계에서 언어의 문법적으로 올바른 문장을 생성하는 수단으로 사용된다.^[9]

4. 1. 생성 문법

언어학에서, 구조 규칙 또는 '''재작성 규칙'''은 일부 생성 문법 체계에서 언어의 문법적으로 올바른 문장을 생성하는 수단으로 사용된다.^[9] 이러한 규칙은 일반적으로 A → X 형식을 취하는데, 여기서 A는 명사구 또는 문장과 같은 구문 범주 레이블이며, X는 이러한 레이블 또는 형태소의 시퀀스이다. 이는 문장의 구성 구조를 생성할 때 A를 X로 대체할 수 있다는 것을 의미한다. 예를 들어, 규칙 S → NP VP는 문장이 명사구(NP)와 동사구(VP)로 구성될 수 있음을 의미하며, 추가 규칙은 명사구와 동사구가 무엇으로 구성될 수 있는지 등을 지정한다.

5. 추상 재작성 시스템 (ARS)

추상 재작성 시스템(Abstract Rewriting System, ARS)은 객체 집합과 객체 간의 재작성 규칙(축약 관계)으로 구성된다. 재작성 시스템은 추상적인 표현을 통해 이해할 수 있으며, 이를 구체화하기 위해서는 객체 및 규칙들의 집합을 구체화해야 한다.

예를 들어, ''T'' = {''a'', ''b'', ''c''} 와 같이 객체 ''T''가 주어지고, ''a'' → ''b'', ''b'' → ''a'', ''a'' → ''c'', ''b'' → ''c'' 와 같은 이진 관계를 나타내는 규칙들이 있다고 하자. 여기서 ''a''와 ''b''는 모두 ''c''로 재작성될 수 있으며, ''c''는 더 이상 다른 형태로 재작성될 수 없는 가장 단순한 형태이다.

이러한 개념을 일반적으로 ''추상 축약 시스템''^[10] 또는 ''추상 재작성 시스템''(약자 ''ARS'')^[11]이라고 한다. ARS는 객체 집합 ''A''와 ''A'' 위에서의 이항 관계인 축약 관계(재작성 관계^[12], 또는 단순히 축약) → 로 구성된다.

5. 1. 기본 개념

\overset{*}\rightarrow

는

\rightarrow

의 반사적 추이적 폐포이다.

\leftrightarrow

는

\rightarrow

의 대칭 폐포이다.

\overset{*}{\leftrightarrow}

는

\rightarrow

의 반사적 추이적 대칭 폐포이다. 추상 재작성 시스템(ARS)에 대한 단어 문제는 주어진 ''x''와 ''y''에 대해

x \overset{*}{\leftrightarrow} y

인지 여부를 결정하는 것이다. ''A''의 객체 ''x''는

x \rightarrow y

인 다른 ''y''가 존재하면 ''축약 가능''이라고 한다. 그렇지 않으면 ''축약 불가능'' 또는 정규형이라고 한다. 객체 ''y''는

x \stackrel{*}{\rightarrow} y

이고 ''y''가 축약 불가능하면 "''x''의 정규형"이라고 한다. ''x''의 정규형이 고유하면 일반적으로

x{\downarrow}

로 표시한다. 모든 객체가 적어도 하나의 정규형을 가지면 ARS를 ''정규화''라고 한다.

x \downarrow y

또는 ''x''와 ''y''는

x \overset{*}{\rightarrow} z \overset{*}{\leftarrow} y

의 속성을 가진 ''z''가 존재하면 ''접합 가능''이라고 한다.^[31]

5. 2. 처치-로서 속성 및 합류성

ARS가

x \overset{*}{\leftrightarrow} y

이면

x \downarrow y

인 경우 처치-로서 성질을 가진다고 한다.^[11] ARS는 A에 있는 모든 ''w'', ''x'', ''y''에 대해

x \overset{*}{\leftarrow} w \overset{*}{\rightarrow} y

이면

x \downarrow y

인 경우 합류한다. ARS는 A에 있는 모든 ''w'', ''x'', ''y''에 대해

x \leftarrow w \rightarrow y

이면

x\mathbin\downarrow y

인 경우 ''국소적으로 합류''한다고 한다. 합류하고 종료되는 ARS를 ''수렴'' 또는 ''정규''라고 한다.^[11]

어떤 치환 규칙을 적용하더라도 최종적으로 동일한 표준형이 되는 항 재작성 시스템의 성질을 합류성이라고 부른다. 이는 표준형의 유일성과 관련된 특성이다.

5. 3. 종료성 (노에테리안)

무한 체인 x₀ → x₁ → x₂ → ... 이 없으면 추상 재작성 시스템(ARS)은 종료 또는 노에테리안이라고 불린다.^[11] 뉴먼의 보조정리에 따르면, 종료되는 ARS는 국소적으로 합류하는 경우에만 합류한다. ARS에 대한 단어 문제는 일반적으로 결정 불가능하다.^[10]

6. 문자열 재작성 시스템 (SRS)

문자열 재작성 시스템(String Rewriting System, SRS)은 알파벳 위의 문자열(단어)을 재작성하는 시스템으로, 반-Thue 시스템이라고도 한다. SRS는 자유 모노이드 구조를 활용하여 재작성 관계를 확장한다.

SRS에서 축약 관계는 모노이드 연산과 호환된다. 즉, x가 y로 축약될 수 있다면, 모든 문자열에 대해 uxv는 uyv로 축약될 수 있다.

반-Thue 시스템은 본질적으로 모노이드의 표현과 일치한다. 예를 들어, {ab → ε, ba → ε} 규칙을 갖는 알파벳 {a, b} (ε는 빈 문자열)는 한 생성자에 대한 자유군의 표현이다. 규칙이 {ab → ε}뿐이면 이중 사이클릭 모노이드의 표현이 된다. 따라서 반-Thue 시스템은 모노이드와 그룹에 대한 단어 문제를 해결하기 위한 자연스러운 프레임워크를 구성한다.^[13]

6. 1. 기본 개념 및 정의

형식적으로 반-Thue 시스템은 튜플 (Σ, R)로 표현되는데, 여기서 Σ는 (일반적으로 유한한) 알파벳이고, R은 알파벳 내의 일부 (고정된) 문자열 간의 이진 관계이며, 이를 ''재작성 규칙''의 집합이라고 한다. Σ^*에서 R에 의해 유도된 ''1단계 재작성 관계'' →_R는 다음과 같이 정의된다. s, t ∈ Σ^*가 임의의 문자열일 때, s = xuy, t = xvy이고 u R v인 x, y, u, v ∈ Σ^*가 존재하면 s →_R t이다. 관계 R이 대칭적이면, 그 시스템을 ''Thue 시스템''이라고 한다.^[13]

6. 2. Thue 합동

→_R의 반사적 추이적 대칭적 폐포(↔*_R)는 합동 관계이다. 이 관계 ↔*_R를 ''R''에 의해 생성된 ''Thue 합동''이라고 한다.^[13] Thue 합동에 의해 자유 모노이드 Σ*의 인자 모노이드 ℳ_R = Σ*/↔*_R을 정의할 수 있다. 모노이드 ℳ이 ℳ_R과 동형이면, (Σ, R)은 ℳ의 모노이드 표현이다.

6. 3. 단어 문제

반-Thue 시스템에 대한 단어 문제는 일반적으로 해결할 수 없다. 이 결과는 때때로 ''Post-Markov 정리''라고도 불린다.^[13]

7. 항 재작성 시스템 (TRS)

'''항 재작성 시스템''' ('''TRS''')은 중첩된 하위 표현식을 가진 표현식인 ''항''을 대상으로 하는 재작성 시스템이다. 이 시스템의 항은 이진 연산자 $(\vee)$ 및 $(\wedge)$ 와 단항 연산자 $(\neg)$ 로 구성된다. 규칙에는 모든 가능한 항을 나타내는 변수도 포함된다 (단일 변수는 단일 규칙 전체에서 항상 동일한 항을 나타낸다).

'''그림 1:''' 항에서 위치 $p$ 에서 재작성 규칙 $l \longrightarrow r$ 의 적용을 나타내는 개략적인 삼각형 다이어그램, 일치하는 치환 $\sigma$ 포함

항 재작성 시스템은 일부 프로그래밍 언어의 기반이 되기도 한다. 예를 들어, 수학적 응용을 위한 함수형 프로그래밍 언어인 Pure가 있다.^[15]^[16]

항 재작성 시스템은 자동 정리 증명에도 유용한 방법이다. 몇 가지 등식으로 이루어진 가설이 있을 때, 그것들을 일종의 항 재작성 규칙군으로 이용할 수 있다. 간단한 대수학에서 "유사한 항을 한쪽 변으로 모으는" 방법이 항 재작성 수법의 예시이다.

:''P''(''x'') = ''Q''(''x'')

여기서 ''P''와 ''Q''는 다항식이다. 통상적인 규칙을 몇 번 적용하면 다음과 같은 형태의 등식을 얻을 수 있다.

:''R''(''x'') = 0.

이는 일종의 표준형이지만, 재작성 경로에 따라 ''R''의 내용은 달라질 수 있다. ''R''이 정규형이라고 할 때는 ''R''(''x'')의 항들이 ''x''의 차수가 큰 것부터 작은 것 순서로 정렬되어 있을 때를 말한다.

7. 1. 기본 개념

항 재작성 시스템(TRS)은 중첩된 하위 표현식을 가진 표현식인 항을 대상으로 하는 재작성 시스템이다. 항은 주어진 서명에 의해 고정된 허용된 기호 집합인 기호의 트리로 시각화할 수 있다. 형식론으로서 항 재작성 시스템은 튜링 머신의 모든 능력을 가지고 있다. 즉, 모든 계산 가능한 함수는 항 재작성 시스템에 의해 정의될 수 있다.^[14]

규칙 좌변 항 $x*(y*z)$ 가 항 $\frac{a*((a+1)*(a+2))}{1*(2*3)}$ 과 일치

7. 2. 종료성 (Termination)

일반적인 재작성 시스템의 종료 문제는 추상 재작성 시스템#종료 및 수렴에서 다룬다. 항 재작성 시스템의 경우, 선형 좌변을 가진 규칙 하나로 구성된 시스템의 종료조차도 결정 불가능하다.^[20]^[21] 유한 ground 시스템의 경우는 결정 가능하다.^[22]

토야마의 예시는 종료되는 두 항 재작성 시스템(TRS)의 합집합이 종료되지 않는 예시를 제시하여 나훔 데르쇼비츠의 추측을 반증했다.^[26]^[27] 데르쇼비츠는 두 개의 종료 항 재작성 시스템

R_1

과

R_2

의 합집합은

R_1

의 모든 좌변과

R_2

의 우변이 선형이고,

R_1

의 좌변과

R_2

의 우변 사이에 "겹침"이 없으면 다시 종료된다고 주장했지만, 토야마의 예시는 이러한 속성들을 모두 만족하면서도 종료되지 않는다.

7. 3. 고차 재작성 시스템 (HRS)

람다 항에 대한 일차 항 재작성 시스템의 일반화로, 고차 함수와 바운드 변수를 허용한다.^[28] 일차 TRS에 대한 다양한 결과는 HRS에도 마찬가지로 재구성될 수 있다.^[29]

7. 4. 그래프 재작성 시스템

그래프 재작성 시스템은 그래프를 항/해당하는 트리 표현 대신에 사용하여 항 재작성 시스템을 일반화한 방법이다.^[1]

8. 추적 재작성 시스템

추적 이론은 추적 모노이드 및 이력 모노이드와 같이 다중 처리를 더 공식적인 용어로 논의할 수 있는 수단을 제공한다. 추적 시스템에서도 재작성이 수행될 수 있다.

9. 크누스-벤딕스 완비화 알고리즘

크누스-벤딕스 완비화 알고리즘은 주어진 항 재작성 시스템을 동등하면서 합류성을 만족하는 시스템으로 변환하는 알고리즘이다.

10. 한국의 재작성 시스템 연구 및 활용

대한민국에서는 재작성 시스템이 소프트웨어 공학, 이론 전산학, 인공지능 등 다양한 분야에서 연구 및 활용되고 있다.

10. 1. 이론 전산학

자동 정리 증명에서 항 재작성 시스템은 유용한 방법으로 활용된다. 예를 들어, 몇 가지 등식으로 이루어진 가설이 있을 때, 이 등식들을 일종의 항 재작성 규칙으로 사용할 수 있다. 간단한 대수학에서 "유사한 항을 한쪽 변으로 모으는" 방법은 항 재작성의 예시이다.

예를 들어, ''P''(''x'') = ''Q''(''x'') 와 같은 등식이 있을 때 (여기서 ''P''와 ''Q''는 다항식) 통상적인 규칙을 적용하면 ''R''(''x'') = 0과 같은 형태의 등식을 얻을 수 있다. 이때, ''R''(''x'')가 정규형이라면, ''x''의 차수가 큰 항부터 작은 항 순서로 정렬되어 있다.

논리학에서 연언 정규형(CNF)을 얻는 과정은 항 재작성 시스템으로 표현할 수 있다. 이 시스템의 규칙은 다음과 같다.

$\neg\neg A \to A$ (이중 부정 제거)
$\neg(A \land B) \to \neg A \lor \neg B$ (드 모르간의 법칙)
$\neg(A \lor B) \to \neg A \land\neg B$
$(A \land B) \lor C \to (A \lor C) \land (B \lor C)$ (분배 법칙)
$A \lor (B \land C) \to (A \lor B) \land (A \lor C)$

여기서 화살표(

\to

)는 규칙의 좌변을 우변으로 재작성할 수 있음을 의미한다. 즉, 조건문(～라면～)을 나타내는 논리 함축이 아니다.

참조

_[1] 간행물 "Proving and Rewriting" International Conference on Algebraic and Logic Programming Nancy, France 1990
_[2] 논문 The Kansas University rewrite engine http://irep.ntu.ac.u[...] 2019-02-12
_[3] 논문 The term rewriting approach to automated theorem proving
_[4] 논문 Theory and practice of constraint handling rules
_[5] 논문 Maude: Specification and programming in rewriting logic
_[6] 서적 Programming with Constraints: An Introduction https://books.google[...] MIT Press
_[7] 문서
_[8] 서적 Formal Techniques in Artificial Intelligence Elsevier
_[9] 서적 Foundations of Generative Syntax https://books.google[...] MIT Press
_[10] 문서
_[11] 문서
_[12] 문서
_[13] 문서
_[14] 문서
_[15] 논문 Signal Processing in the Pure Programming Language https://archive.org/[...] 2009
_[16] 웹사이트 Pure – eine einfache funktionale Sprache https://www.heise.de[...] 2009-11-18
_[17] 웹사이트 Term Rewriting Systems http://www.cs.tau.ac[...] Tel Aviv University 2021-08-14
_[18] 서적 Rewrite Systems Elsevier
_[19] 문서
_[20] 서적 Proc. 3rd Int. Conf. on [[Rewriting Techniques and Applications]] Springer
_[21] 논문 Simulation of Turing machines by a regular rewrite rule 1992-09
_[22] 간행물 On the Uniform Halting Problem for Term Rewriting Systems http://www.ens-lyon.[...] 1978-03
_[23] 문서
_[24] 문서
_[25] 서적 Proc. International Conference on Logic Programming and Automated Reasoning (LPAR) Springer 1993-06
_[26] 논문 Counterexamples to Termination for the Direct Sum of Term Rewriting Systems http://www.nue.ie.ni[...]
_[27] 서적 Proc. RTA Springer
_[28] 서적 The Clausal Theory of Types Cambridge University Press 1993
_[29] 서적 Automated Deduction - A Basis for Applications. Volume I: Foundations Kluwer 1998
_[30] 문서
_[31] 문서

본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.

문의하기 : help@durumis.com