결막정상형

부울 논리학에서 공식은 하나 이상의 절이 결합된 경우 결합 정상형(CNF) 또는 폐쇄 정상형(Clause normal)이며, 여기서 절은 문맹의 분리형이며, 그렇지 않으면 합계의 산물 또는 OR의 AND이다.표준적인 정상 형태로서 자동화된 정리 증명과 회로 이론에 유용하다.

리터럴의 모든 접속사와 리터럴의 모든 접속사는 CNF에 있는데, 각각 1리터럴 절의 접속사와 단일 절의 접속사로 볼 수 있기 때문이다.분리 정규 형태(DNF)에서와 같이, CNF의 유일한 명제 연결 공식은 다음과 같으며, 또는 그렇지 않다.연산자는 리터럴의 일부로만 사용할 수 있으며, 이는 명제 변수나 술어 기호 앞에만 사용할 수 있다는 것을 의미한다.

자동화된 정리 증명에서, "claular normal form"이라는 개념은 종종 좁은 의미로 사용되는데, 이는 일련의 리터럴로서 CNF 공식의 특정한 표현을 의미한다.

예시 및 비예시

$변수$ $A,$ $B,$ $C,$ $D,$ E $A,B,C,D,E$ 및 $F$ $F$ 에 있는 다음 공식은 모두 결합 정상 형식이다 $F$ .

$(A\lor \neg B\lor \neg C)\land (\neg D\lor E\lor F)}$
$(A\displaystyle (A\lor B)\land (C)}$
$(A\displaystyle (A\lor B)}$
$(\displaystyle (A)}$

명확하게 하기 위해 위의 괄호 안에 이절조항이 쓰여 있다.괄호화된 결막 절이 있는 절연 정상형에서는 마지막 경우는 같지만 마지막은 $(A)\lor (B)$ ( $(A)\lor (B)$ ) $(A)\lor (B)$ ( $(A)\lor (B)$ ) ∨ (B ) $(A)\lor (B)$ 이다 $(A)\lor (B)$ 참과 거짓의 상수는 빈 결막과 빈 결막으로 구성된 하나의 절에 의해 표시되지만, 일반적으로 명시적으로 쓰여진다.^[1]

다음 공식은 결합 정규 형식이 아니다.

$\neg (B\lor C)$ OR이 NOT 내에 중첩되기 때문에 $\neg (B\lor C)$ ( $\neg (B\lor C)$ $\neg (B\lor C)$ $\neg (B\lor C)$ ) $\neg (B\lor C)$
$디스플레이 스타일(A\land B)\lor C}$
$A\land (B\lor (D\land E))$ AND가 수술실 내에 중첩되기 때문에 $A\land (B\lor (D\land E))$ $A\land (B\lor (D\land E))$ ( $A\land (B\lor (D\land E))$ $A\land (B\lor (D\land E))$ ( $A\land (B\lor (D\land E))$ $A\land (B\lor (D\land E))$ E $A\land (B\lor (D\land E))$ ) $A\land (B\lor (D\land E))$ ) ${\displaystyle A\land (B\lor (D\land E$

모든 공식은 결벽 정상 형태의 공식으로 동등하게 쓰여질 수 있다.CNF의 세 가지 비예제는 다음과 같다.

$(\displaystyle (\neg B)\land (\neg C)}$
$[\displaystyle (A\lor C)\land (B\lor C)}$
$(B\displaystyle (A)\land (B\lor D)\land (B\lor E).}$

CNF로의 전환

^[2]모든 명제 공식은 CNF에 있는 동등한 공식으로 변환될 수 있다.이 변환은 논리적 동등성에 관한 규칙에 근거한다: 이중 부정 제거, 드 모건의 법칙, 그리고 분배 법칙.

모든 명제 공식은 결합 정상 형태의 등가 공식으로 변환될 수 있기 때문에, 증명들은 종종 모든 공식들이 CNF라는 가정에 근거한다.그러나 경우에 따라 CNF로의 변환은 수식의 지수 폭발로 이어질 수 있다.예를 들어 다음과 같은 비 CNF 공식을 CNF로 변환하면 $2^{n}$ ${\$ 2 $^{n}$ 절의 $2^{n}$ 공식이 생성된다.

(X_{1}\wedge Y_{1})\ve(X_{2}\wedge Y_{2}\ve)\dots \ve(X_{n}\wedge Y_{n})\ve.

특히 생성된 공식은 다음과 같다.

(X_{1}\vee X_{2}\vee \cdots \vee X_{n})\wedge (Y_{1}\vee X_{2}\vee \cdots \vee X_{n})\wedge (X_{1}\vee Y_{2}\vee \cdots \vee X_{n})\wedge (Y_{1}\vee Y_{2}\vee \cdots \vee X_{n})\wedge \cdots \wedge (Y_{1}\vee Y_{2}\vee \cdots \vee Y_{n}).

이 공식에는 $2^{n}$ ${\$ 2 $^{n}$ 절이 $2^{n}$ 포함되어 있으며, 각 $X_{i}$ 에는 $X_{i}$ $i$ ${\displaystyle X_$ ${i}$ 또는 $X_{i}$ $Y_{i}$ $Y_{i}$ ${\$ $}$ 가 포함되어 있다 $i$

등가성보다는 만족도를 보존함으로써 기하급수적으로 규모가 커지는 것을 피하는 CNF로의 전환이 존재한다.^[3]^[4]이러한 변환은 공식의 크기를 선형적으로 증가시킬 뿐 아니라 새로운 변수를 도입할 수 있다.예를 들어 다음과 같이 $Z_{1},\ldots ,Z_{n}$ 변수 $Z_{1},\ldots ,Z_{n}$ 1 $Z_{1},\ldots ,Z_{n}$ , $Z_{1},\ldots ,Z_{n}$ … $Z_{1},\ldots ,Z_{n}$ , $Z_{1},\ldots ,Z_{n}$ $Z_{1},\ldots ,Z_{n}$ ${\$ 을 추가하여 위의 공식을 CNF로 변환할 수 있다.

(Z_{1}\vee \cdots \vee Z_{n})\wedge (\neg Z_{1}\vee X_{1})\wedge (\neg Z_{1}\vee Y_{1})\wedge \cdots \wedge (\neg Z_{n}\vee X_{n})\wedge (\neg Z_{n}\vee Y_{n}).

해석은 적어도 하나의 새로운 변수가 참일 경우에만 이 공식을 만족한다.이 변수가 $Z_{i}$ ${\$ 인 경우 $X_{i}$ ${\$ 와 $X_{i}$ $Y_{i}$ ${\$ 모두 참이다 $Y_{i}$ .이는 이 공식을 만족하는 모든 모델이 원래의 공식을 만족한다는 것을 의미한다.한편, 원본 공식의 일부 모델만이 이것을 만족시킨다: ${\$ 는 원본 공식에서 언급되지 $Z_{i}$ 않기 때문에, 그들의 가치는 그것의 만족과 무관하며, 마지막 공식에서는 그렇지 않다.이는 본래의 공식과 번역의 결과가 같기는 하지만 동등하지는 않다는 것을 의미한다.

An alternative translation, the Tseitin transformation, includes also the clauses $Z_{i}\vee \neg X_{i}\vee \neg Y_{i}$ . With these clauses, the formula implies $Z_{i}\equiv X_{i}\wedge Y_{i}$ ; this formula is often regarded to "define" $Z_{i}$ $Z_{i}$ $X_{i}\wedge Y_{i}$ $X_{i}\wedge Y_{i}$ $display$ Y i {\ $displaystyle$ $X_{i}\wedge Y_{i}}$ 의 이름 $X_{i}\wedge Y_{i}$

1차 논리

첫 번째 순서 논리에서는 결합 정상 형태를 더 취하여 논리 공식의 폐쇄 정상 형태를 산출할 수 있으며, 그 다음에는 1차 분해능을 수행하는 데 사용할 수 있다.분해능 기반 자동 정리 검증에서 CNF 공식

(\displaystyle)(}

l_{11}

\displaystyle \lor }

\displaystyle \ldots }

\displaystyle \lor }

l_{1n_{1}

(\displaystyle )}

\displaystyle \land }

\displaystyle \ldots }

\displaystyle \land }

(\displaystyle)(}

l_{m1

\displaystyle \lor }

\displaystyle \ldots }

\displaystyle \lor }

l_{mn_{m}

(\displaystyle )}

, l

l_{ij}

l_{ij}

{\

Literals와

l_{ij}

함께 일반적으로 집합으로 표시됨

\{

\{

l_{11}

,

\displaystyle \ldots }

,

l_{1n_{1}

\}

,

\displaystyle \ldots }

,

\{

l_{m1

,

\displaystyle \ldots }

,

l_{mn_{m}

\}

\}

.

예를 보려면 아래를 참조하십시오.

계산 복잡성

계산 복잡성의 중요한 문제 집합에는 결막 정상 형태로 표현된 부울 공식의 변수에 대한 할당을 찾는 것이 포함된다.k-SAT 문제는 CNF에 표현된 부울 공식에 대한 만족스러운 할당을 찾는 문제로서, 각 결합에는 최대 k 변수가 포함되어 있다. 3-SAT는 NP-완전(k>2의 다른 k-SAT 문제처럼)이며, 2-SAT는 다항 시간 내에 해결책이 있는 것으로 알려져 있다.결과적으로,^[5] 공식을 만족도를 보존하고 DNF로 변환하는 작업은 NP-hard이며, 일반적으로 유효성을 보존하는 CNF로 변환하는 것도 NP-hard이므로 동등성 보존형 변환은 다시 NP-hard이다.

이 경우 일반적인 문제는 "3CNF"의 공식과 관련된다. 즉, 결막당 변수가 3개 이하인 결막 정상형이다.실제에서 접하는 그러한 공식의 예는 매우 클 수 있다. 예를 들어 변수 10만 개와 결막 100만 개와 같은 것이다.

A formula in CNF can be converted into an equisatisfiable formula in "kCNF" (for k≥3) by replacing each conjunct with more than k variables $X_{1}\vee \cdots \vee X_{k}\vee \cdots \vee X_{n}$ by two conjuncts ${\displaystyle X_{1}\vee \cdots \vee X_{k-1}\ve$ $e Z}$ 및 $X_{1}\vee \cdots \vee X_{k-1}\vee Z$ $\neg Z\vee X_{k}\cdots \vee X_{n}$ $\neg Z\vee X_{k}\cdots \vee X_{n}$ $\neg Z\vee X_{k}\cdots \vee X_{n}$ $\neg Z\vee X_{k}\cdots \vee X_{n}$ $\neg Z\vee X_{k}\cdots \vee X_{n}$ $\neg Z\vee X_{k}\cdots \vee X_{n}$ n ${\$ $Z$ 가 새로운 $\neg Z\vee X_{k}\cdots \vee X_{n}$ 변수인 경우 필요에 따라 자주 반복한다.

1차 로직에서 변환

1차 로직을 CNF로 변환하려면:^[2]

부정 정규 형식으로 변환하십시오.
1. Eliminate implications and equivalences: repeatedly replace $P\rightarrow Q$ with $\lnot P\lor Q$ ; replace $P\leftrightarrow Q$ with $(P\lor \lnot Q)\land (\lnot P\lor Q)$ . Eventually, this will eliminate all occurre→ $\displaystyle \rightarrow }$ 및 $\rightarrow$ $\leftrightarrow$ £ {\ $displaystyle \leftrightarrow }$ 의 nce $\leftrightarrow$
2. De Morgan's Law를 반복적으로 적용하여 NOT를 안쪽으로 이동하십시오.Specifically, replace $\lnot (P\lor Q)$ with $(\lnot P)\land (\lnot Q)$ ; replace $\lnot (P\land Q)$ with $(\lnot P)\lor (\lnot Q)$ ; and replace $\lnot \lnot P$ with $P$ $P$ ; replace $\lnot (\forall xP(x))$ with $\exists x\lnot P(x)$ ; $\lnot (\exists xP(x))$ with $\forall x\lnot P(x)$ . After that, a $\lnot$ may occur only imm술어 기호 앞에 가까이 있다.
변수 표준화
1. 동일한 변수 이름을 두 번 사용하는 $(\forall xP(x))\lor (\exists xQ(x))$ ( $(\forall xP(x))\lor (\exists xQ(x))$ $(\forall xP(x))\lor (\exists xQ(x))$ $(\forall xP(x))\lor (\exists xQ(x))$ ( x $(\forall xP(x))\lor (\exists xQ(x))$ ) $(\forall xP(x))\lor (\exists xQ(x))$ ( x ) $(\forall xP(x))\lor (\exists xQ(x))$ ( $(\forall xP(x))\lor (\exists xQ(x))$ ) $(\forall xP(x))\lor (\exists xQ(x))$ { ( x ) { ( $(\forall xP(x))\lor (\exists xQ(x))$ { x $(\forall xP(x))\lor (\exists xQ(x))$ ( ) ) $(\forall xP(x)\lor (\exists xQ(x))})$ 과 같은 문장의 경우 변수 중 하나의 이름을 변경한다.이것은 나중에 정량자를 떨어뜨릴 때 혼란을 피할 수 있다.For example, $\forall x[\exists y\mathrm {Animal} (y)\land \lnot \mathrm {Loves} (x,y)]\lor [\exists y\mathrm {Loves} (y,x)]$ is renamed to ${$ $\displaystyle \forall x[\exists y\mathrm {animal}(y)\lnot \lnot \$ mathrm { $loves}(x,y)]\lor [\exists z\mathrmatrm {loves}(z,x$
진술을 스콜레마이징하다.
1. Move quantifiers outwards: repeatedly replace $P\land (\forall xQ(x))$ with $\forall x(P\land Q(x))$ ; replace $P\lor (\forall xQ(x))$ with $\forall x(P\lor Q(x))$ ; replace $P\land (\exists xQ(x))$ $P\land (\exists xQ(x))$ with $\exists x(P\land Q(x))$ ; replace $P\lor (\exists xQ(x))$ with $\exists x(P\lor Q(x))$ .이러한 대체품은 이전 가변 $표준화$ 단계에서x {\ $displaystyle$ x $}$ 이 $($ P {\ $displaystyle$ P}에서 발생하지 않도록 $x$ 보장했기 때문에 동등성을 보존한다 $P$ 이러한 대체 후에 계량기는 공식의 초기 접두사에서만 발생할 수 있지만, $\lnot$ never ${\displaystyle$ \ $lnot$ $\lnot$ }, $\lnot$ $∧ {\displaystylean$ 내부에서는 발생하지 않는다. $d }$ , 또는 $\lor$ ${\displaystyle \lor$ $\lor$
2. Repeatedly replace $\forall x_{1}\ldots \forall x_{n}\;\exists y\;P(y)$ with $\forall x_{1}\ldots \forall x_{n}\;P(f(x_{1},\ldots ,x_{n}))$ , where $f$ is a new $n$ -ary 함수 기호, 이른바 "Skolem 함수".이것은 동등성보다는 만족성만을 보존하는 유일한 단계다.그것은 모든 실존적 정량자를 제거한다.
모든 범용 수량자를 삭제하십시오.
안쪽으로 안쪽으로 OR 배포: $P\lor (Q\land R)$ P $P\lor (Q\land R)$ ( $P\lor (Q\land R)$ $P\lor (Q\land R)$ $P\lor (Q\land R)$ ) $displaystyle P\lor (Q\land R)}$ 을(를) $(P\lor Q)\land (P\lor R)$ ( $(P\lor Q)\land (P\lor R)$ $(P\lor Q)\land (P\lor R)$ $(P\lor Q)\land (P\lor R)$ ) $(P\lor Q)\land (P\lor R)$ ( $(P\lor Q)\land (P\lor R)$ R $(P\lor Q)\land (P\lor R)$ ) {\ $displaystyle (P\lor Q)\land (P\lor$ R $)}$ 로 $P \lor (Q \land R)$ 반복 교체 $(P\lor Q)\land (P\lor R)$

예를 들어, "모든 동물을 사랑하는 사람은 차례대로 누군가에게 사랑받는다"는 공식은 다음과 같이 CNF(이후 마지막 줄의 절 형태로)로 변환된다( ${\color {red}{\text{red}}}$ ${\displaystyle$ {\ $color}{\text}}}}).$

\displaystyle \forall x}

(\displaystyle)(}

\displaystyle \forall y}

{\displaystyle \mathrm {Animal}(})

(\displaystyle y}

(\displaystyle )}

\displaystyle \color {red}\오른쪽 화살표 }

{\displaystyle \mathrm {loves}(x,})

(\displaystyle y}

(\displaystyle )}

(\displaystyle )}

\displaystyle \rightarrow }

(\displaystyle)(}

\displaystyle \reason }

(\displaystyle y}

{\displaystyle \mathrm {loves}(})

(\displaystyle y}

(\displaystyle ,x)}

(\displaystyle )}

\displaystyle \forall x}

(\displaystyle)(}

\displaystyle \forall y}

\displaystyle \lnot }

{\displaystyle \mathrm {Animal}(})

(\displaystyle y}

(\displaystyle )}

\displaystyle \lor }

{\displaystyle \mathrm {loves}(x,})

(\displaystyle y}

(\displaystyle )}

(\displaystyle )}

\displaystyle \color {red}\오른쪽 화살표 }

(\displaystyle)(}

\displaystyle \reason }

(\displaystyle y}

{\displaystyle \mathrm {loves}(})

(\displaystyle y}

(\displaystyle ,x)}

(\displaystyle )}

1.1로

\displaystyle \forall x}

\displaystyle \color {red}\lnot }

(\displaystyle)(}

{\color {red}{\all y}

\displaystyle \lnot }

{\displaystyle \mathrm {Animal}(})

(\displaystyle y}

(\displaystyle )}

\displaystyle \lor }

{\displaystyle \mathrm {loves}(x,})

(\displaystyle y}

(\displaystyle )}

(\displaystyle )}

\displaystyle \lor }

(\displaystyle)(}

\displaystyle \reason }

(\displaystyle y}

{\displaystyle \mathrm {loves}(})

(\displaystyle y}

(\displaystyle ,x)}

(\displaystyle )}

1.1로

\displaystyle \forall x}

(\displaystyle)(}

\displaystyle \display y}

\displaystyle \color {red}\lnot }

(\displaystyle)(}

\displaystyle \lnot }

{\displaystyle \mathrm {Animal}(})

(\displaystyle y}

(\displaystyle )}

\displaystyle \color {red}\lor }

{\displaystyle \mathrm {loves}(x,})

(\displaystyle y}

(\displaystyle )}

(\displaystyle )}

(\displaystyle )}

\displaystyle \lor }

(\displaystyle)(}

\displaystyle \reason }

(\displaystyle y}

{\displaystyle \mathrm {loves}(})

(\displaystyle y}

(\displaystyle ,x)}

(\displaystyle )}

1.2로

\displaystyle \forall x}

(\displaystyle)(}

\displaystyle \display y}

\displaystyle \color {red}\lnot }

\displaystyle \color {red}\lnot }

{\displaystyle \mathrm {Animal}(})

(\displaystyle y}

(\displaystyle )}

\displaystyle \land }

\displaystyle \lnot }

{\displaystyle \mathrm {loves}(x,})

(\displaystyle y}

(\displaystyle )}

(\displaystyle )}

\displaystyle \lor }

(\displaystyle)(}

\displaystyle \reason }

(\displaystyle y}

{\displaystyle \mathrm {loves}(})

(\displaystyle y}

(\displaystyle ,x)}

(\displaystyle )}

1.2로

\displaystyle \forall x}

(\displaystyle)(}

{\color {red}{\red}{\red y}

{\displaystyle \mathrm {Animal}(})

(\displaystyle y}

(\displaystyle )}

\displaystyle \land }

\displaystyle \lnot }

{\displaystyle \mathrm {loves}(x,})

(\displaystyle y}

(\displaystyle )}

(\displaystyle )}

\displaystyle \lor }

(\displaystyle)(}

\displaystyle \color {red}\cHB }

\color {red}y

{\displaystyle \mathrm {loves}(})

(\displaystyle y}

(\displaystyle ,x)}

(\displaystyle )}

1.2로

\displaystyle \forall x}

(\displaystyle)(}

\displaystyle \display y}

{\displaystyle \mathrm {Animal}(})

(\displaystyle y}

(\displaystyle )}

\displaystyle \land }

\displaystyle \lnot }

{\displaystyle \mathrm {loves}(x,})

(\displaystyle y}

(\displaystyle )}

(\displaystyle )}

\displaystyle \color {red}\lor }

(\displaystyle)(}

\displaystyle \color {red}\cHB }

\color {red}z

{\displaystyle \mathrm {loves}(})

(\displaystyle z}

(\displaystyle ,x)}

(\displaystyle )}

2시까지

\displaystyle \forall x}

\displaystyle \property z}

(\displaystyle)(}

{\color {red}{\red}{\red y}

{\displaystyle \mathrm {Animal}(})

(\displaystyle y}

(\displaystyle )}

\displaystyle \land }

\displaystyle \lnot }

{\displaystyle \mathrm {loves}(x,})

(\displaystyle y}

(\displaystyle )}

(\displaystyle )}

\displaystyle \color {red}\lor }

{\displaystyle \mathrm {loves}(})

(\displaystyle z}

(\displaystyle ,x)}

3.1로

\displaystyle \forall x}

{\color {red}{\red z}

\displaystyle \display y}

(\displaystyle)(}

{\displaystyle \mathrm {Animal}(})

(\displaystyle y}

(\displaystyle )}

\displaystyle \land }

\displaystyle \lnot }

{\displaystyle \mathrm {loves}(x,})

(\displaystyle y}

(\displaystyle )}

(\displaystyle )}

\displaystyle \lor }

{\displaystyle \mathrm {loves}(})

(\displaystyle z}

(\displaystyle ,x)}

3.1로

\displaystyle \forall x}

{\color {red}{\red}{\red y}

(\displaystyle)(}

{\displaystyle \mathrm {Animal}(})

(\displaystyle y}

(\displaystyle )}

\displaystyle \land }

\displaystyle \lnot }

{\displaystyle \mathrm {loves}(x,})

(\displaystyle y}

(\displaystyle )}

(\displaystyle )}

\displaystyle \lor }

{\displaystyle \mathrm {loves}(})

g(x)

(\displaystyle ,x)}

3.2로

(\displaystyle)(}

{\displaystyle \mathrm {Animal}(})

f(x)

(\displaystyle )}

\displaystyle \color {red}\land }

\displaystyle \lnot }

{\displaystyle \mathrm {loves}(x,})

f(x)

(\displaystyle )}

(\displaystyle )}

\displaystyle \color {red}\lor }

{\displaystyle \mathrm {loves}(})

g(x)

(\displaystyle ,x)}

4시까지

(\displaystyle)(}

{\displaystyle \mathrm {Animal}(})

f(x)

(\displaystyle )}

\displaystyle \color {red}\lor }

{\displaystyle \mathrm {loves}(})

g(x)

(\displaystyle ,x)}

(\displaystyle )}

\displaystyle \color {red}\land }

(\displaystyle)(}

\lnot \mathrm {Loves}(x,f(x))

\displaystyle \color {red}\lor }

\mathrm {Loves}(g(x),x)

(\displaystyle )}

5시까지

\{

\{

{\displaystyle \mathrm {Animal}(})

f(x)

(\displaystyle )}

,

{\displaystyle \mathrm {loves}(})

g(x)

(\displaystyle ,x)}

\}

,

\{

\lnot \mathrm {Loves}(x,f(x))

,

\mathrm {Loves}(g(x),x)

\}

\}

(상호 표현)

비공식적으로 스콜렘 함수 $g(x)$ ( $g(x)$ ) ${\displaystyle$ $g$ $(x)}$ 은(는) $x$ ${\displaystyle$ x $}$ 이(가) 사랑하는 $x$ 사람을 양보하는 것으로 생각할 $g(x)$ 수 $f(x)$ , f $f(x)$ ( x $f(x)$ ) ${\displaystyf(x)}$ 은( $f(x)$ 경우) $x$ ${\displaystystyty$ x $}$ 가 사랑하지 않는 $x$ 동물을 산출한다 $f(x)$ .그 다음 세 번째 마지막 줄은 " $x$ $x$ 이( $f(x)$ ) 동물 $f(x)$ ( x $f(x)$ ) $f(x)$ 을(를) 좋아하지 않거나 $x$ $f(x)$ $그렇지$ 않으면 x ${\$ $displaystyle x$ $}$ 이 $)$ $g(x)$ ( $x)}$ 에 의해 사랑받는다 $x$ $g(x)$

The 2nd last line from above, $(\mathrm {Animal} (f(x))\lor \mathrm {Loves} (g(x),x))\land (\lnot \mathrm {Loves} (x,f(x))\lor \mathrm {Loves} (g(x),x))$ , is the CNF.

메모들

^ 피터 B.Andrews, 2013년 수학 논리 및 유형 이론 소개 ISBN9401599343, 페이지 48
^ ^a ^b 인공지능: Wayback Machine에 2017-08-31년 보관된 현대적 접근 방식 [1995년...] 러셀러와 Norvig
^ 쎄이틴 (1968년)
^ 잭슨과 셰리던(2004)
^ CNF 만족도를 확인하는 한 가지 방법은 CNF를 DNF로 변환하는 것이며, CNF 만족도는 선형 시간 내에 확인할 수 있다.

참고 항목

참조

J. Eldon Whitesitt (24 May 2012). Boolean Algebra and Its Applications. Courier Corporation. ISBN 978-0-486-15816-7.
Hans Kleine Büning; Theodor Lettmann (28 August 1999). Propositional Logic: Deduction and Algorithms. Cambridge University Press. ISBN 978-0-521-63017-7.
Paul Jackson, Daniel Sheridan: Boolean Circuits의 절 형태 변환.인: 홀거 H.후스, 데이비드 G.미첼(에드스):만족도 시험의 이론과 적용, 제7차 국제 회의, SAT 2004, 밴쿠버, BC, 캐나다, 2004년 5월 10일-13일, 개정 선택 논문컴퓨터 과학 3542, 2005, 페이지 183–198
지에스 티틴:명제 미적분학의 파생의 복잡성에 대해.In: Sliensko, A.O. (ed.) 건설적 수학과 수학 논리에서의 구조, Part II, Semina in Mathematics (러시아어에서 번역), 페이지 115–125.스테클로프 수학 연구소 (1968년)

외부 링크

[1] 피터 B.Andrews, 2013년 수학 논리 및 유형 이론 소개 ISBN9401599343, 페이지 48

[:0-2] 인공지능: Wayback Machine에 2017-08-31년 보관된 현대적 접근 방식 [1995년...] 러셀러와 Norvig

[3] 쎄이틴 (1968년)

[4] 잭슨과 셰리던(2004)

[5] CNF 만족도를 확인하는 한 가지 방법은 CNF를 DNF로 변환하는 것이며, CNF 만족도는 선형 시간 내에 확인할 수 있다.

[1]

[2]

[3]

[4]

[5]

Search

결막정상형

네임스페이스

더

목차

예시 및 비예시

CNF로의 전환

1차 논리

계산 복잡성

1차 로직에서 변환

메모들

참고 항목

참조

외부 링크