-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.html
74 lines (73 loc) · 4.77 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
<!DOCTYPE html>
<html lang="en-US">
<head>
<meta charset="UTF-8"/>
<link rel="stylesheet" type="text/css" href="./css/style.css">
<script src="./build/script.js" type="text/javascript"></script>
<script id="MathJax-script" async src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
</head>
<body>
<div id="MainInput">
<label for="SetInput">Input Clausal Form:</label>
<input id="SetInput" type="text" placeholder="Clausal form of formula" value="{{A,B}, {C,-B,D}, {-D}, {A,-C}, {-A}}"></br>
<button id="SetInputButton">Use Resolution</button>
<button id="ClearButton">Clear Graph</button>
<input id="RedundantClauseCheckbox" type="checkbox">Remove redundant Clauses</input></br>
<svg id="ResolutionTree"></svg>
</div>
<div id="Explanation">
<p>
<h1>Resolution: Propositional Logic</h1>
Resolution is a technique for proving theorems.
It works by taking any formula, and transforming it first into the conjunctive normal form and then in Clausal Form.
Then we can prove that the formula is unsatisfiable using the rules of resolution. In the following, I will outline how resolution works, and will try to give a rough, intuitive way to understand resolution :).
</p>
<p>
<h1>Conjunctive Normal Form/CNF</h2>
<p>
A formula is in CNF when it's of the form \((C_1 \land C_2 \land \dots \land C_n)\) with every clause \(C_i\) being disjunctive, meaning for some literals \(L_1, L_2, \dots, L_n\) it looks like \((L_1 \lor L_2 \lor \dots \lor L_n)\)<br>
Some examples include:</br>
\[\begin{align*}
&(A \lor B \lor \neg C) \land (A \lor \neg B) \land (\neg A \lor C) \land \neg C\\
&(A) \land (\neg A) \land (B \land C \land D \land E)\\
&(A \lor B) \land (\neg A \lor B) \land (A \lor \neg B) \land (\neg A \lor \neg B)
\end{align*}\]
</p>
<p>
The benefit of the CNF is that for the entire formula to be true, every clause must be true.
This means that, if we want to show that a formula is unsatisfiable, we can try to compare 2 clauses, and see if they contradict each other. <br>
Take for example the second example above. Since \(A\) and \(\neg A\) cannot be true at the same time, we know that the entire formula is false.<br>
We can also compare 2 clauses, and see if we can derive/resolve a new clause, that might help us. For example, look at the clauses \((A \lor B)\) and \((\neg A \lor B)\).
Depending on the value of \(A\), one Clause is always true, while the other one will just become \(B\). Therefore, we can conclude that we can add \(B\) to our formula while keeping it equivalent:
\[(A \lor B) \land (\neg A \lor B) \equiv (A \lor B) \land (\neg A \lor B) \land B\]
We can call \(B\) the resolvant of \((A \lor B)\) and \((\neg A \lor B)\). <br>
Every time we have a clause with a variabe like \(A\), and another clause with \(\neg A\), we can just combine both clauses, but remove both \(A\) and \(\neg A\) from it.<br>
But before we use this property of the CNF, we want to change it's form to better utilize these properties, leading us to the clausal form.
</p>
</p>
<p>
<h1>Clausal Form/CF</h1>
<p>
When our formula is in CNF, we can bring it to the CF to make it easier to formalize and utilize the afformentioned properties.<br>
The clausal form of a formula \(\phi\) in CNF is a set \(\mathcal K\) consisting of sets with literals.
Every set in \(\mathcal K\) represents a clause in \(\phi\), so for every clause in \(\phi\), we put all its literals in a set.
For example:
\[\mathcal K((A \lor B \lor \neg C) \land (A \lor \neg B) \land (\neg A \lor C) \land \neg C) = \{\{A,B,\neg C\}, \{A, \neg B\}, \{\neg A, C\}, \{\neg C\}\}\]
We basically just remove the \(\land\) and \(\lor\), because we only really care about what literals are inside what clauses for resolution.
Since we also don't need to care about the order of literals inside of clauses (\(\lor\) is commutative), we can just put all literals in a set.
</p>
</p>
<p>
<h1>Defining Resolution</h1>
<p>
With the CF, we can now define the rule of resolution:<br>
<p>
If we have 2 clauses \(C_1\) and \(C_2\), with \(L \in C_1\) and \(\neg L \in C_2\), then \(C = (C_1 / \{L\}) \cup (C_2 / \{\neg L\})\) is the resolvant of \(C_1\) and \(C_2\). <br>
Let \(\text{Res}(\mathcal K) = \mathcal K \cup \{C \mid C \text{ is resolvant of 2 clauses in }\mathcal K\}\). If \(\emptyset \in \text{Res}(\mathcal K)\), then \(\mathcal K\) is unsatisfiable.
</p>
Now, we can use \(\text{Res}\) repeatedly until we either have \(\emptyset \in \text{Res}(\mathcal K)\), or until we can't find any new resolvants.
</p>
</p>
</div>
</body>
</html>