Definition 1.1 (Aussagenlogik, Syntax) 형식론
aussagenlogischen Formeln (명제논리식) 는 아래와 같이 정의된다.
이 말인 즉 not, and, or 이 명제 논리식의 전부라는 말이다.
Semantik 의미론
Semantik
즉 ‘의미론’이 무슨 말일까요? 이 말은 명제 변수에 값을 집어 넣어준다는 의미입니다. 왜 값을 넣어줄까요? 왜냐하면 앞으로 우리는 한 명제가 참이 될 수 있는 지 없는 지를 알고 싶기 때문입니다. 예를 하나 들겠습니다.
위의 수식이 참이 될 수 있나요? 절대 될 수 없습니다. 이는 직관적으로도 와 닿지만 다른 방식으로도 풀 수 있습니다. 변수에 0 이나 1 같은 참, 거짓 값을 넣어보면 됩니다. 이 행위를 우리는 의미론이라 부르고 앞으로 이를 다룰겁니다.
Definition 1.2 (Aussagenlogik, Semantik) 의미론
‘값 집어넣기(Belegung)’ 란 함수다.
즉, 각각의 변수에 0 또는 1을 집어 넣는 것을 말한다. 더 나아가 V는 귀납적으로 다른 복합적인 명제논리식에도 적용된다.
‘값 집어넣기’ 예시
모델 (Modell)의 정의
만약 V()이 1이면, 우리는 명제논리식이 V로 인해 채워졌다고 말합니다. 우리는 이때 라고 하고 V 를 의 모델이라고 부릅니다.
‘모델’ 예시
Wahrheittabelle (진리표)
진리표를 활용하면 아주 쉽게 명제의 가능성을 판단할 수 있습니다. 이에 대한 설명은 생략하도록 하겠습니다. 이거는 한국어로도 많이 나와있으니 쉽게 배울 수 있을 겁니다.
‘진리표’ 예시
Implikation
한국어로 충분조건이라는 말이 있지만 한국어는 오히려 어려우니 쓰지 않겠습니다. Implikation은 만약..하면, ..하다 의 형식입니다.
→ 와 ↔
‘implicate’ 예시
XOR
‘XOR’ 예시
XOR은 Biimplikation의 부정입니다. 가만히 생각해보면 직관적으로 와 닿습니다.
A ↔ B 는 위와 같은 상황일 때만 1 을 가집니다. 다시 말해 XOR은 A와 B가 달라야만 1을 갖습니다. 그래서 Biimplikation을 부정해준겁니다.
추가로 알아두기
는 항상 0이고요. 는 항상 1입니다. 입니다.
SyntaxBäume 형식나무
명제 식을 형식 나무로 나타내면 아주 편합니다.
형식 나무 예시
각 노드는 전체 식의 갈래식입니다. 노드를 모르신다면 구글 검색을 하세용!
갈림길의 숫자 = 연결사의 숫자
나뭇잎의 숫자 = 변수의 숫자
Definition 1.4 (Teilformeln) 갈래식
가 명제논리식이라고 하자. 집합 는 의 갈래식이다. 이는 귀납적으로 아래와 같이 정의된다.
갈래식 예시
Lemma 1.3 (Koinzidenzlemma)
라는 한 명제가 있다고 하자. 더 나아가 라는 값 집어넣기 함수가 있다고 하자. 명제 에 있는 모든 변수 에 대해서 이라면 , 이다.
쉽게 말해 , 명제 속 모든 변수 대하여 두개의 서로 다른 ‘값 집어넣기’의 결과가 같다면 , 명제에 대한 두개의 서로 다른 ‘값 집어넣기’의 결과가 같다.
나중에 술어논리에 쓰입니다.
Auswertung und Äquivalenz (평가와 동일성)
이 강의에서는 논리와 관련된 다양한 알고리즘 문제들을 배우게 될 것입니다. 이러한 문제들은 평가 문제, 충족 가능성 문제 등이 포함됩니다.
알고리즘의 입력으로 사용하기 위해 수식은 유한한 알파벳을 사용하여 표현되어야 합니다. 여기서 우리는 ¬, ^, , (, ), 0, 1과 같은 알파벳 기호들을 사용합니다. 0과 1은 변수 이름의 표현에 사용됩니다. 예를 들어, '=¬x(y^z)'는 '¬00_(01^10)'으로 표현됩니다.
여기서 '를 표기한 것은 해당 표현의 크기, 즉 표현의 길이를 나타냅니다. 예를 들어,
|¬x _ (y ^ z)| = 11입니다.
하지만 대부분의 경우, 우리는 이러한 표현의 세부 사항들을 추상화하고 무시합니다.
요약하자면, 이 강의에서는 논리와 관련된 알고리즘 문제들을 다룰 것이며, 수식은 유한한 알파벳을 사용하여 표현되어야 합니다. 일반적으로 이러한 표현의 세부 사항들은 고려하지 않고 추상화됩니다.
이번 주제에서 우리의 목표는 한 명제논리식이 채워질 수 있는 지 입니다. ‘채워진다’ 는 한 명제를 참으로 만들 수 있음을 뜻합니다. 동일성은 명제식을 간단하게 만들기 위해서 씁니다.
Auswertung 평가
Def. 다음이 명제논리학의 평가문제 입니다.
주어진 것: 명제 논리식 이 주어질 때, 를 위한 할당
질문: ? // 가 의 모델인가요?
Th. 복잡성 평가 문제
평가문제는 다항시간 안에 풀릴 수 있습니다.
다항시간이란 입니다. 여기서 n은 입력의 크기입니다.
주석:
Auswertungsproblem은 두 가지 입력을 가지고 있지만, V는 보다 크지 않을 수 있으므로 입력 크기 n = | | 로 사용할 수 있습니다. 여기서 | |는 명제식 의 길이입니다.
여기에서는 이 문제의 다항 시간 내에 해결 가능함을 보여주기 위해 제곱 시간 내의 해결 가능성만을 보여주려고 합니다.
평가 알고리즘
Lemma
모든 논리식 φ와 할당 V에 대해 다음이 성립합니다: 이 성립하는 것은 가 성립한다는 것과 동일합니다.
Äquivalenz 동일성
이제 알고리즘의 실행 시간을 간단히 분석해보겠습니다. 명백히, 의 재귀 트리는 의 구문 트리와 정확히 일치합니다. 따라서 다음과 같이 표현할 수 있습니다:
재귀 호출 수 = 구문 트리의 노드 수, 즉
각 호출의 시간 복잡도: 를 에서 찾는 데 소요. 따라서 전체 실행 시간은 입니다.
Def. 두 수식 와 가 모든 대입에 대해 가 성립할 때, 이들은 동등(equivalent)하다고 합니다. 이를 로 표기합니다.
동일성 예시
Lemma Ersetzungslemma 바꾸기 보조 정리
와 가 동일한 수식이라고 가정하고, 가 를 포함하는 형태인 경우, 에서 임의의 을 대체한 결과인 에 대해 가 성립합니다.
쓸만한 동일성
독일어 번역 안해도 충분히 이해 하시겠죠?
Funktionale Vollständigkeit und Normalformen
함수적 완정성과 기본 모양
Funktionale Vollständigkeit 함수적 완정성
Definition 1.10 (Boolesche Funktion) 부울 함수
n 자리 수의 부울 함수는 함수 을 의미합니다. 여기서 이고,
• 은 모든 n자리 수의 부울 함수들의 집합을 나타냅니다.
• 는 모든 부울 함수들의 집합을 나타냅니다.
예시
은 상수로 이루어진 함수입니다. 이는 0 아니면 1이 됩니다.
은 네개의 함수로 이루어져 있습니다. :
부울 함수 예시
함수는 입력 0에 대해 0을 출력하고, 입력 1에 대해 0을 출력합니다.
함수는 입력 0에 대해 1을 출력하고, 입력 1에 대해 0을 출력합니다.
함수는 입력 0에 대해 1을 출력하고, 입력 1에 대해 1을 출력합니다.
함수는 입력 0에 대해 0을 출력하고, 입력 1에 대해 1을 출력합니다.
즉, 은 한 변수 속 두 개의 입력(0 아니면 1)을 가지는 함수들의 집합이며, 각 함수는 입력에 따라 0 또는 1을 출력합니다.
,
근데 한 번 생각을 해보면 변수가 하나인 함수 에는 과 같이 두자리가 필요하지 않을까요? 왜냐하면 변수 하나가 0 또는 1값을 가질 수 있으니까요. 만약에 그러면 변수가 개 라고 하면 어떨까요? 그러면 우리는 자리의 함수들이 필요하지 않을 까요? 다시말해
이런 형태의 함수들이 생기지 않을까요? 근데 여기서 각 자리수가 또 0 또는 1의 값을 가질 수 있지 않나요?
까지 말이죠. 그럼 이 가능성이 얼마나 될까요? 각 자리수 마다 2가지의 가능성이 번 반복되고 있으니
자세히 말해 이니.
이 되지 않을까요?
AL Formeln ⇒ Boolesche Funktionen 명제논리 → 부울 함수
가지의 변수를 지닌 각각의 명제 논리식 는 자리 수의 부울 함수 로 나타낼 수 있습니다.
, 즉 명제 논리식안에 여러개의 변수가 있다고 합시다.
를 위한 각각의 값 집어넣기 함수 은 부울 함수 에서 하나의 입력을 나타냅니다.
번째 입력의 함수값은 이겠네요.
의 함수값은 ‘값 집어넣기 함수’에서의 와 같습니다.
명제논리 → 부울 함수 예시
Boolesche Funktionen ⇒ AL Formeln 부울 함수 → 명제 논리
반대로, 모든 부울 함수에는 그것을 대표하는 명제 논리 수식이 존재합니다.
Theorem 1.11 (funktionale Vollständigkeit) 함수적 완정성
모든 부울 함수 에 대해, 를 만족하는 수식 가 존재합니다.
우리는 방금 명제 논리학이 부울 함수를 표현하는 언어로 이해될 수 있다는 사실을 발견했습니다. 모든 부울 함수가 명제 논리 수식으로 표현될 수 있다는 사실은 명제 논리의 함수적 완전성(Functional Completeness)으로 알려져 있습니다. 이는 칩 디자인 등에서 중요한 역할을 합니다.
그러나 표현하는 수식은 매우 커질 수 있습니다. 부울 함수 에 대해 라는 수식은 최대 개의 합집합 를 포함할 수 있습니다. 이는 일반적으로 피할 수 없음을 보여줍니다.
Lemma 1.12 (Exponentielle Größe unvermeidbar) 피할 수 없는 폭발적 크기
이 함수이고, 각각의 부울 함수 에 대해 를 만족하는 크기 의 수식 가 존재한다고 가정합니다. 그렇다면 은 에 속하지 않습니다.
(부울 함수의 승수 n 공식의 길이 n).
여기서 공식의 길이란 예를 들어 는 길이가 3이다.
자 그럼 이제 부울 함수를 보자.
부울 함수
은 이다. 이걸 가능하게 하려면 함수가 항거명제야 한다.
ex.
이런 항거명제의 최소길이는 4 이다.
이렇게 와 상응하는 명제의 최소길이를 찾아보자 . 그럼 그 결과가 아마도 아래와 같을 것이다.
그렇다면 부울 함수 에 상응하는 명제를 만들기 위해서 적어도 몇개의 길이가 필요할까?
답은 이다.
2. 더욱 확장하여 그럼이제 을 생각해보자.
의 경우의 수를 다 따져보고 이 필요한 최소길이를 구한다고 하자.
그렇다면 이는 보다 빠르게 성장할 것이다.
길이가 이하인 수식의 개수는 이다.
즉, 은 보다 작다. 함수 은 보다 더 빠르게 성장하지 못한다.
Normalformen 기본 모양
부울 함수 → 명제 논리로 변환가능하다는 걸 배웠습니다. 근데 여기서 재미있는 게 나옵니다. 모든 명제는 아래와 같은 형식과 동일하다는 거죠. ( 을 잘 숙지하세용)
Definition 1.16 (Erfüllbarkeit, Gültigkeit) 만족가능함, 타당함
한 명제식은..
- 각 ‘값 집어넣기’ 함수에 대해 진실만을 내놓을 때, 타당하다 혹은 항진명제라고 부릅니다.
- 각 ‘값 집어넣기’ 함수에 대해 진실이 한개라도 존재할 때, 만족 가능하다고 합니다.
타당한 명제 예시
만족 불가능한 명제 예시
Lemma 1.17 (Dualität Erfüllbarkeit, Gültigkeit) 만족 가능함과 타당함 사이 관계
한 명제식 는…
- 를 만족하는 게 불가능 할 때, 타당합니다.
- 가 타당하지 않을 때, 만족 가능합니다.
서로 서로 연관성이 있군요.
Definition 1.18 (Erfüllbarkeitsproblem, Gültigkeitsproblem) 만족 가능함 문제, 타당함 문제
만족 가능함 문제는 다음과 같습니다:
명제식이 주어졌을 때, 만족가능한가?
타당함 문제는 다음과 같습니다:
명제식이 주어졌을 때. 타당한가?
명제 논리의 주제가 바로 이것입니다. 한 명제가 주어졌을 때, 그게 가능해..?라는 질문에 대답하는 거죠. 물론 우리는 진리표라는 대단한 알고리즘이 있기는 합니다. 값을 하나하나 집어넣어보면서 명제식이 만족 가능한지 안한지 찾아보면 되죠. 근데 그 진리표의 줄이 이라는 게 문제입니다. 만약에 우리가 100개의 변수를 사용하는 명제식이 있다고 가정할 때 우리는 진리표를 줄이나 그려야 합니다. 이는 상상을 초월하는 숫자입니다. 그래서 컴퓨터 공학에서는 이 알고리즘을 최대한 최적화하려고 노력합니다.
SAT 문제(만족 가능함 문제)
만족 가능함 문제는 "SAT" (satisfiability의 영어 약자)라고도 불립니다.
이는 컴퓨터 과학에서 가장 중요한 문제 중 하나로, 효율적으로 해결할 수 없다고 추정되는 문제입니다.
이는 이론적인 컴퓨터 과학에서 가장 유명한 미해결 문제와 밀접하게 관련되어 있습니다.
"효율적"은 "다항 시간 내에"로 해석됩니다.
이는 "P vs NP 문제"와 깊은 관련이 있습니다.
"Berechenbarkeit"라는 강의에서 더 자세히 다루어집니다.
아래에서는 이와 관련된 지수 시간 가설에 대해 설명하겠습니다.
Exponentialzeitvermutung (ETH) 지수 시간 가설
ETH Vermutung (Exponential Time Hypothesis)
1. 세 개로 리터럴로 이루어진 KNF가 있다고 하자.
예를 들어 .
2. 이런 명제식 속 변수의 수를 이라고 하자.
3. 이때 실행시간이 이 되는 알고리즘은 없다.
예를 들어 실행시간이 인 알고리즘은 없다.
KNF 모양에서 만족 가능함 문제를 풀려고 하는 것은 어쩌면 어리석은 일임니다. 그래서 우리는 DNF를 사용합니다.
Lemma 1.19 (Einfache Fälle) 쉬운모양
다음과 같은 상황에서 DNF는 만족 가능합니다:
- 하나의 부분이라도 만족 가능할 때
- 같은 리터럴을 포함하지 않을 때
다음과 같은 상황에서 KNF는 타당합니다.
- 각 부분이 타당할 때
- 각 부분이 같은 리터럴 두개를 포함 할 때,
Fogerbarkeit 유도되기
Definition 1.20 (Folgerbarkeit, Konsequenz) 유도되기, 결과
값 집어넣기 함수인 일 때, 명제 식 는 다른 명제식 로부터 유도된다고 합니다.
이 경우에 은 의 결과라고 부르고 이라고 씁니다.
유도되기 예시
왼쪽이 참이면 , 오른쪽도 참이다. 정도로 이해하시면 좋습니다.
Lemma 1.21 (Folgerbarkeit und Gültigkeit) 유도되기와 타당함
모든 명제식 에 대해서:
1. 가 타당합니다. (aka 디덕정리)
2. 는 타당합니다. .
Modus Pones
Modus Ponens는 논리학에서 사용되는 추론 규칙 중 하나입니다. 이 규칙은 다음과 같이 표현됩니다.
즉, "P이면 Q"와 "P"가 참인 경우, "Q"를 결론으로 얻을 수 있습니다.
Hornlogik 호른 논리
우리는 좋은 계산법을 쓰기 위해 호른 논리를 배웁니다.
Horn-formel 호른 명제
Definition 1.22 (Horn-Formel) 호른 명제
호른 명제식이란 KNF 모양이면서 각 ‘이거나 결합’ 가 최대 한 개의 양의 리터럴을 가지고 있는 걸 말합니다.
호른 식 예시
에 라는 양의 리터럴이 하나있고 나머지 부분에도 두 개 이상의 양의 리터럴은 없으니까 위 식은 호른 식이 맞다.
직관적인 예:
Erfüllbarkeitsproblem für Horn-Formeln 만족 가능함 문제와 호른 명제
Theorem 1.23 (Effiziente Erfüllbarkeit) 효율적으로 만족 가능한가 알아보기
호른 논리에서 만족가능함 문제는 선형시간에 풀 수 있다.
Markierungsalgorithmus 마킹 알고리즘
예시2. 명제식 . 알고리즘을 이용해보자.
2번째 줄에 따라서 :
while 절에 따라서 (2 리터럴!)
명제식에 있는 한계는 이고 에 랑 가 없으니까 , if 절에 따라서 만족 가능이라는 대답을 내놓는다.
개의 변수가 있는 명제식은 최대 n번 while절을 돌아야 한다. 그러므로 이 알고리즘은 다항시간안에 끝난다.
Lemma 1.24
이 알고리즘은 입력 명제가 만족 가능하면 항상 “만족 가능” 하다를 내놓음.
증명은 나중에 적겠습니다. p. 76
Minimale Modelle 최소 모델
명제식 의 모델 이 최소모델이라면 다음을 만족한다:
명제식 의 각 모델 에 대하여
(를 참으로 만드는 모든 변수는 각 모델 안에서도 참이다.
마킹 알고리즘의 결과가 만족 가능이었다면, 그때 ‘값 집어넣기’ 가 최소모델이다.
Korollar 1.25
모든 만족 가능한 호른 명제식은 최소 모델이다.
Ausdrucksstärke 표현력
호른 논리는 어떤 모양을 표현할 수 있을까요? 세상에 있는 모든 명제 식을 호른 논리식으로 변환할 수 있을까요? 그렇기만 한다면 만족 가능 문제를 쉽게 풀 수 있겠네요.
Lemma 1.26 (Nicht-Horn-Ausdrückbarkeit) 호른 논리로 표현할 수 없는 모양
호른 논리식은 모양을 표현할 수 없다.
우리는 여기서 명제식 가 KNF 인 로 변환 되는 것을 한 번 더 관찰하겠습니다. 근데 만족 가능함에 관련해서 살펴보겠습니다.
erfüllbarkeitsäquivalent 만족 가능성 동등
이 만족 가능 이 만족 가능
이 만족 가능 이면 이 만족 가능이다 이 만족 가능이면 이 만족 가능이다.
주의사항:
"만족 가능성 동등"는 "의미적으로 동등한" 것보다 약한 성질입니다.
예를 들어, p ∨ q와 r은 "만족 가능성 동등 "를 가지지만 "의미적으로 동등하지는 않습니다.
"만족 가능성 동등 "는 일반적으로 식에 대입되어도 유지되지 않습니다.
예를 들어, 와 는 만족 가능성이 동등하지만, 와 는 그렇지 않습니다.
Tseitin-Transformation 체이틴 변환
Theorem 1.27
명제식 에서 체이틴 변환 가 유도 될 때, 랑 는 만족 가능성이 동등하다.
증명: p.83
체이틴 변환 주의점
Resolution 결론 도출
우리는 앞으로 명제식의 만족 가능성을 쉽게 판단하는 방법을 배울거다. 그게 바로 결론 도출이다.
Resolution은 새로운 논리식을 결론 도출하기 위해 추론 규칙을 사용하여 유도하는 한 유형의 추론 방법이다. Resolution에서 가장 중요한 메커니즘은 Resolventenbildung(결론 생성)입니다. Hilbert-Kalkül(힐베르트 계산법)과 Sequenzenkalkül(순서 계산법)과 같은 다른 종류의 계산법도 있습니다. 계산법은 알고리즘적으로 구현하거나 이론적인 목적으로 사용할 수 있습니다.
Resolution에는 입력 논리식이 형식화된 정규화된 표준 형태(CNF)여야 합니다.
우리는 이미 알고 있듯이, 이것은
일반성에 제한을 주지 않는다는 점과
다항식 시간 복잡성으로 달성할 수 있다는 점에서 중요합니다(Tseitin-Transformation). 그러나 Resolution은 KNF 형태의 논리식을 약간 다른 형태로 표현합니다: 절 집합으로 표현합니다.
Definition 1.28 (Klausel, Klauselmenge) 절, 절 집합
절(Klausel)은 리터럴이 있는 유한한 집합이다. 빈 절은 로 나타냄.
한 KNF 식 은 절들의 집합 으로 나타낼 수 있다:
- 번째 “이면 결합” 는 절 를 생성한다.
-
예시: 명제식
알아두기:
은 만족 불가능을 뜻하는 게 아니라 “빈 이면결합”을 뜻함.
을 포함하는 절 집합은 만족 불가능이다.
주요 아이디어: 반대되는 리터럴 서로 지우기. 어떻게 하는 지 보여 드릴게요.
Definition 1.29 (Resolvente) 결론 부분
를 절이라고 하자. 일때, 절 가 결론 부분이라고 한다.
결론 부분 예시
Lemma 1.30 (Resolutionslemma) 결론 도출 보조 정리
을 절 집합이라고 가정하고,이며, 가 랑 의 결론 부분(resolvent)이라고 가정하자. 그러면 이다.
Definition 1.31 (Res)
각 절 집합 에 대해
-
-
-
Res 예시
결론 도출은 만족 가능성을 확인하는 알고리즘이다.
일반적으로 다음과 같은 사항을 갖는다:
계산법은 종료된다:
각 입력에 대해 유한한 개수의 논리식만 생성될 수 있는 경우.
계산법은 올바르다:
원하는 논리식만 생성될 수 있는 경우.
계산법은 완전하다:
모든 원하는 논리식이 생성될 수 있는 경우.
Resolution의 경우:
원하는 논리식이 생성되는 경우 ⇔ 입력 논리식이 만족 불가능한 경우.
즉, 계산법이 종료되고, 원하는 논리식만 생성되며, Resolution의 경우 입력 논리식이 만족 불가능할 때 원하는 논리식이 생성됩니다.
Lemma 1.32 (Terminierung) 종료
모든 유한한 절 집합 에 대해 다음은 성립한다:
이 하나 존재한다.
다시 말해 언젠가는 가 종료된다.
Theorem 1.33 (Korrektheit) 정확성
이 유한한 절 집합이고 이면 은 만족 불가능이다.
Resolutionsbeweis (결과 증명):
Definition 1.34 (Resolutionsbeweis) 결과 증명
을 유한한 절 집합이라 하자. 절들의 모임 은 다음이 유효할 때 의 결과 증명이라고 한다:
- 모든 에 대해 이거나 는 의 결론 부분이다.
- .
결과 증명의 길이는 m이다.
Lemma 1.37
이 만족 불가능이면 안에 존재하는 각 변수 에 대해 다음이 유효하다:
- 는 만족 불가능이다.
-
-
최종적으로 우리는 다음과 같은 만족 가능성 문제를 위한 알고리즘을 얻을 수 있음.
추가 코스: 증명 길이
일부 Klauselmengen은 각 Resolutionsbeweis가 지수적으로 길 수 있는데,
그 예로 Schubfachprinzip(비둘기집의 오류) 을 들 수 있습니다. Schubfachprinzip은 n + 1개의 객체를 n개의 서랍에 분배할 때, 적어도 하나의 서랍에는 2개의 객체가 들어있게 됩니다.
위의 식은 항진 명제임.
Theorem 1.39 (AtseriasMiller 2019)
1. 어떠한 알고리즘도 주어진 불만족 가능한 절 집합 M에 대해 Resolutions 증명을 생성할 수 없습니다. 즉, M이 불만족 가능한 경우에도 해당 증명을 찾는 알고리즘이 존재하지 않습니다.
2. 주어진 불만족 가능한 절 집합 M에 대한 Resolutions 증명을 판별하는 알고리즘도 존재하지 않습니다. 즉, M이 불만족 가능한 경우 해당 증명이 있는지를 확인하는 알고리즘이 존재하지 않습니다.
3. 이러한 결과는 Resolutions 증명에 대한 알고리즘적인 한계를 보여줍니다. Resolutions 증명은 모든 가능한 경우를 탐색하는 데에 지수적인 시간이 소요되기 때문에, 일반적인 경우에는 효율적인 알고리즘이 존재하지 않습니다.
Einheitsresolution 단위 결정법
Einheitsresolution은 논리학의 Resolution 방법의 변형 중 하나입니다. 이 방법에서는 각 Resolution 단계에서 참여하는 Literal 중 적어도 하나는 양수 단위 리터럴(positive unit literal)이어야 합니다. 양수 단위 리터럴은 원자적인 리터럴(atomic literal)이거나 원자적인 리터럴의 부정입니다.
Einheitsresolution은 여전히 정확하다는 점에서 기존의 Resolution과 동일합니다. 즉, 원하는 결과만을 생성합니다. Einheitsresolution은 Resolution의 적용 규칙을 따르며 올바른 결과를 제공합니다. 그러나 일반적으로 전체적인 완전성(completeness)을 보장하지는 않습니다.
그러나 호른 식 집합에 대해서는 Einheitsresolution이 완전하다는 것이 입증되어 있습니다. 호른 식은 양수 단위 리터럴이 하나뿐인 절로 이루어진 논리식입니다. 이러한 경우 Einheitsresolution은 모든 원하는 논리식을 증명할 수 있습니다.
실제로 Einheitsresolution은 마킹 알고리즘과 밀접한 관련이 있습니다. 마킹 알고리즘은 Horn clause를 처리하기 위한 알고리즘으로 사용됩니다. 또한, 추가적인 수정인 "geordnete Einheitsresolution"을 적용하면 Horn 논리식의 충족 가능성 판정에 대한 다항 시간 복잡도 알고리즘이 생성됩니다.
다음은 Einheitsresolution을 사용하여 두 개의 절을 해결하는 예시입니다:
절 1: (A ∨ B)
절 2: (¬A ∨ C)
먼저, 첫 번째 절에서 양수 단위 리터럴을 찾습니다. 여기서는 A가 해당됩니다. 그리고 두 번째 절에서 A의 부정(¬A)을 찾습니다. 이제 이 두 리터럴을 사용하여 Resolution을 수행합니다.
Resolution 단계:
(A ∨ B) (절 1)
(¬A ∨ C) (절 2)
(B ∨ C) (Resolution: A 제거)
결과로 새로운 절 (B ∨ C)가 생성됩니다. 이것이 Einheitsresolution의 한 단계입니다.
위의 예시에서 볼 수 있듯이 Einheitsresolution은 한 번에 한 개의 양수 단위 리터럴을 사용하여 Resolution을 수행합니다. 이를 통해 새로운 절을 생성하고 원하는 결과를 도출할 수 있습니다.
증명:
Geordnete Einheitsresolution
SAT-Solver
현대 SAT-Solver는 Davis-Putnam-Logemann-Loveland(DPLL) 알고리즘을 기반으로 합니다.
DPLL은 Resolution과는 다른 알고리즘입니다만, Resolution으로부터 발전되었습니다.
SAT-Solver는 많은 정교한 (가끔은 꽤 복잡한) 최적화를 통해 실제로 효율적으로 동작합니다.
Lingeling, Minisat, Glucose, zchaff, precosat, Sat4J와 같은 구체적인 시스템들은 연례적으로 SAT 경쟁에서 서로 경쟁합니다.
DPLL은 기본 버전에서 간단한 재귀 알고리즘입니다. Resolution과 마찬가지로 절(Clause) 집합에 작업을 수행합니다.
다음과 같은 Klausel 집합 M에서 시작합니다:
• 변수 x를 선택하고 x를 1로 설정합니다.
• M을 로 단순화합니다 (Resolution 정리 참조): x를 포함하는 모든 절을 제거하고 남은 절에서 ¬x를 제거합니다.
• 가 충족 가능한지 확인합니다 (재귀 호출). 가능하다면 "충족 가능"을 반환합니다.
• 그렇지 않다면 x를 0으로 설정하고 를 시도합니다.
다음은 의사 코드로 표현된 DPLL 함수입니다:
최적화는 탐색 공간을 적절하게 제한합니다.
시간 복잡도 최적화 하는 법
Hilbert-Kalkül 힐버르트 계산
우리는 Hilbert-Kalkül이라고 불리는 다른 캘큘에 대해 간단히 살펴보겠습니다. 이 캘큘은 논리학자 David Hilbert에게 거슬러 올라갑니다. Resolution과는 몇 가지 차이가 있습니다:
• Hilbert-Kalkül은 입력을 받지 않습니다.
• 이는 차례로 모든 증명 가능한 공식을 생성합니다 (따라서 종료되지 않습니다).
• 이는 어느 정도로는 수학적 증명을 모델링합니다: 공리에서부터 추론규칙의 적용을 통해 점점 복잡한 명제(= 증명 가능한 공식)들이 증명됩니다.
Hilbert-Kalkül은 {->, ¬}로 구성된 연결어 집합 위의 공식을 사용하며, 다음과 같은 공리 체계에 기초합니다.
Kompaktheit 조밀성
가끔씩 명제 논리식의 무한한 집합을 다루는 것이 유용할 때가 있습니다.
무한한 논리식 집합 가 만족 가능하다는 것은 각 에 대해 를 만족하는 대입 가 존재한다는 것을 의미합니다. 무한한 논리식 집합을 이해하기 위한 중요한 결과는 'Kompaktheitssatz'라고도 하는 '조밀성 정리'입니다.
조밀성(Density)은 논리학에서 성립 가능한 문장들의 밀도를 나타내는 개념입니다. 조밀성이란 어떤 논리 체계에서 모든 참인 문장의 집합과 거짓인 문장의 집합 사이에 새로운 문장이 존재한다는 것을 의미합니다. 다시 말해, 어떤 논리 체계에서 참인 문장과 거짓인 문장 사이에는 다른 모든 가능한 참 값들을 나타내는 문장들이 존재한다는 것을 말합니다.
조밀성은 논리 체계의 완전성과 밀접한 관련이 있습니다. 완전성은 주어진 논리 체계에서 모든 참인 문장을 증명 가능하다는 것을 의미합니다. 조밀성 정리는 완전한 논리 체계가 있다면 그 논리 체계는 반드시 조밀성을 가지게 된다는 것을 주장합니다. 다시 말해, 어떤 논리 체계가 완전하다면 그 체계에서 참인 문장과 거짓인 문장 사이에는 반드시 다른 모든 가능한 참 값들을 나타내는 문장들이 존재하게 됩니다.
조밀성은 논리학의 기본적인 개념 중 하나로, 논리 체계의 성질을 분석하고 이해하는 데 도움을 줍니다. 조밀성 정리는 논리 체계의 완전성과 조밀성 사이의 관계를 밝히는 중요한 결과로, 논리학의 기초 이론과 응용 분야에서 널리 사용되고 있습니다.
Definition 1.48 (4-Färbbarkeit) 4색 색칠
양방향 그래프 가 4-색칠 가능하다는 것은, 함수 가 존재하여 모든 에 대해 임을 말합니다. 이러한 함수 를 4-색칠 이라고 합니다.
Theorem 1.49 (4-Farben-Satz, endliche Graphen)
각 유한한 지도는 4색으로 색칠 가능하다.
Theorem 1.50 (4-Farben-Satz, beliebige Graphen)
각 (가능한 무한한) 지도(플레너 그래프)는 4색 색칠가 가능하다.
