-
Notifications
You must be signed in to change notification settings - Fork 8
Expand file tree
/
Copy pathmeet-the-robinson-2.html
More file actions
298 lines (286 loc) · 14.4 KB
/
meet-the-robinson-2.html
File metadata and controls
298 lines (286 loc) · 14.4 KB
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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
<!DOCTYPE html>
<html>
<head>
<link rel="canonical" href="https://hardmath123.github.io/meet-the-robinson-2.html"/>
<link rel="stylesheet" type="text/css" href="/static/base.css"/>
<title>Meet the Robinson: 2 - Comfortably Numbered</title>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
<meta charset="utf-8"/>
<meta name="viewport" content="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no" />
<link rel="alternate" type="application/rss+xml" title="Comfortably Numbered" href="/feed.xml" />
<!--
<script src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script>
<script>
MathJax.Hub.Config({
tex2jax: {inlineMath: [['$','$']]}
});
</script>
-->
<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.13.11/dist/katex.min.css" integrity="sha384-Um5gpz1odJg5Z4HAmzPtgZKdTBHZdw8S29IecapCSB31ligYPhHQZMIlWLYQGVoc" crossorigin="anonymous">
<script defer src="https://cdn.jsdelivr.net/npm/katex@0.13.11/dist/katex.min.js" integrity="sha384-YNHdsYkH6gMx9y3mRkmcJ2mFUjTd0qNQQvY9VYZgQd7DcN7env35GzlmFaZ23JGp" crossorigin="anonymous"></script>
<script defer src="https://cdn.jsdelivr.net/npm/katex@0.13.11/dist/contrib/auto-render.min.js" integrity="sha384-vZTG03m+2yp6N6BNi5iM4rW4oIwk5DfcNdFfxkk9ZWpDriOkXX8voJBFrAO7MpVl" crossorigin="anonymous"></script>
<script>
document.addEventListener("DOMContentLoaded", function() {
renderMathInElement(document.body, {
// customised options
// • auto-render specific keys, e.g.:
delimiters: [
{left: '$$', right: '$$', display: true},
{left: '$', right: '$', display: false},
{left: '\\begin{align}', right: '\\end{align}', display: true},
{left: '\\(', right: '\\)', display: false},
{left: '\\[', right: '\\]', display: true}
],
// • rendering keys, e.g.:
throwOnError : false
});
});
</script>
</head>
<body>
<header id="header">
<script src="static/main.js"></script>
<div>
<a href="/"><span class="left-word">Comfortably</span> <span class="right-word">Numbered</span></a>
</div>
</header>
<article id="postcontent" class="centered">
<section>
<h1>Meet the Robinson: 2</h1>
<center><em><p>Continuing on our quest to build an automatic theorem-prover.</p>
</em></center>
<h4>Thursday, November 5, 2015 · 6 min read</h4>
<p>Welcome back.</p>
<p>In the <a href="meet-the-robinson.html">previous article</a>, we learned how <strong>rules of
inference</strong> allow us to prove theorems. We also learned that a rule of
inference is not necessarily <strong>complete</strong>: it might be impossible to prove a
true sentence with a valid rule of inference.</p>
<p>Today’s article is about a complete rule of inference.</p>
<p>Before you get excited, though, let’s talk about what we really mean by
“complete” in this case.</p>
<ol>
<li>If a statement <em>must</em> be true given some axioms, then the rule of inference
can construct a proof for the statment.</li>
<li>If a statement is false given some axioms, then the rule of inference will
not construct a proof. It is not guaranteed to even terminate in this case.</li>
<li><p>If a statement could either be true or false given some axioms, then the
rule of inference will not construct a proof. It is not guaranteed to even
terminate in this case.</p>
</li>
<li><p>Prove that “Robert is a frog” given “It rained on Monday” and “Seven is a
prime number”.</p>
</li>
<li>Prove that “Robert is not a frog” given “It rained on Monday” and “Seven is a
prime number”.</li>
<li>Explain what we mean by statements that could either be true or false, and
connect this to the discussion of undecidable problems (or independent
statements) in the previous article. These statements are (choose one)
<em>satisfiable/valid</em> but not <em>satisfiable/valid</em>.</li>
<li>How can you use this rule of inference to prove that something is false?</li>
<li>How can you use this rule of inference to discover whether a statement is
true or false, given that it is necessarily either valid or invalid? (Hint:
you’re allowed to fork two processes and kill them if needed.)</li>
</ol>
<p>For the purposes of this article, we can assume that the algorithm will
terminate. Later, though, we will generalize to higher forms of logic where
termination is not guaranteed.</p>
<hr>
<p>The rule of inference we are going to use is called <strong>resolution</strong>, first used
practically by John Alan Robinson in 1965. It goes like this:</p>
<p>\[
\frac{(P \vee \neg Q), (Q \vee R)}{P \vee R}
\]</p>
<ul>
<li>Prove, with a truth table, that this rule is valid.</li>
<li>Convert both premises of the rule to <strong>Kowalski Normal Form</strong>, which means
they should both be in the form “A implies B”.</li>
<li>Use your expressions above to explain how resolution is really the same thing
as “P implies Q, Q implies R together mean P implies R”.</li>
</ul>
<p>Resolution proofs rely on the idea of <strong>refutation</strong> or <em>reductio ad absurdum</em>,
which is more commonly known as <strong>proof by contradiction</strong>.</p>
<p>Refutation relies on the idea that if not-S causes a contradiction with your
axioms and rules of inference, then not-S is invalid, so S must be valid.</p>
<ul>
<li>What do we mean by “contradiction”?</li>
</ul>
<p>To use the resolution-refutation scheme to prove S given some axioms, we can
repeatedly apply resolution to pairs of sentences taken from the axioms and
not-S. If you end up deriving a contradiction, you have proven S.</p>
<p>The rest of this post will be dedicated to proving that this scheme actually
works.</p>
<hr>
<p>Resolution operates on <strong>clauses</strong>, which is just a set of propositions that
are joined with “or”s. These propositions can be negated.</p>
<ul>
<li>Which one of the following three sentences is a clause?<ol>
<li>A ∨ (B ∧ C)</li>
<li>¬ (A ∧ B) ∨ C</li>
<li>¬ A ∨ ¬ B ∨ C</li>
</ol>
</li>
</ul>
<p>Sentences are in <strong>clausal-normal form (CNF)</strong> if they are a set of clauses
that are joined with “and”s.</p>
<ul>
<li>Which of the following three sentences is in CNF?<ol>
<li>A ∨ (B ∧ C)</li>
<li>A ∧ (B ∨ ¬C) ∧ D</li>
<li>¬ (A ∧ B)</li>
</ol>
</li>
</ul>
<p>It turns out that any sentence can be written in CNF. To do this, you can
repeatedly apply the following rules:</p>
<ol>
<li>Remove implication using the expression for “A ⇒ B” you’ve already
found.</li>
<li>Use De Morgan’s laws to move “not” inwards:<ul>
<li>What is ¬ ¬ A?</li>
<li>What is ¬ (A ∧ B)?</li>
<li>What is ¬ (A ∨ B)?</li>
</ul>
</li>
<li>Distribute ∨ over ∧ by replacing A ∨ (B ∧ C) with (A ∨ B)
∧ (A ∨ C).<ul>
<li>Prove that this is true with a truth table.</li>
</ul>
</li>
</ol>
<p>You can use induction to show that applying these rules again and again will
eventually turn your sentence into CNF.</p>
<ul>
<li>Show that none of these rules apply to a sentence already in CNF.</li>
</ul>
<p>Why do we care so much about sentences in CNF? We can now extend the resolution
rule to sentences in CNF:</p>
<p>\[
\frac{(P_1 \vee \dots \vee P_{i} \vee \neg X), (Q_1 \vee \dots \vee Q_{i} \vee X)}{P_1 \vee \dots \vee P_{i} \vee Q_1 \vee \dots \vee Q_{i}}
\]</p>
<ul>
<li>Convince yourself that that’s a reasonable thing to do, using the concept of
associativity.</li>
</ul>
<p>In short, if a proposition appears in both positive and negative polarities in
two clauses, you can join the clauses and remove that proposition.</p>
<ul>
<li>Is the singleton clause “P” technically in CNF?</li>
<li>Use clause-resolution on “P” and “not-P” to find out whether the empty clause
is true or false (hint: is “P ∧ ¬P” invalid?).</li>
<li>Is the empty conjunction true? The empty disjunction? Explain what a vacuous
truth is.</li>
<li>Use resolution-refutation to prove <em>modus ponens</em>. If you only do one
exercise in this article, do this one. (Hint: use the inference rule twice.) </li>
<li>Ryan Marcus has a nice article on propositional resolution
<a href="http://rmarcus.info/blog/2015/09/02/vulcan.html">here</a>, which includes an
interactive demo. Play with that demo.</li>
</ul>
<hr>
<p>We’re now going to prove if you have an unsatisfiable set of clauses, then you
can repeatedly resolve them to derive the empty clause. This provides a model
for us to have a terminating theorem-proving algorithm!</p>
<p>This proof is taken almost directly from Russell and Norvig’s textbook, though
I tried to cut down on the notation.</p>
<p>Imagine we’ve already applied resolution to each pair of clauses,
and recursively resolved the results, and so on to obtain an (infinite?) set
of clauses. We call this the resolution <em>closure</em> of these clauses.</p>
<p>Suppose also that the set of clauses was unsatisfiable, but this set of
resolved clauses does not contain the empty clause. We’re going to show that
you can, in fact, satisfy the clauses, leading to a contradiction.</p>
<p>To satisfy the clauses, follow the following algorithm:</p>
<ol>
<li>Number your propositions from 1 to <em>k</em>.</li>
<li>For the <em>i</em>th proposition P[i]:<ol>
<li>If one of the clauses in the set contains ¬P[i], and all other
propositions in that clause are false based on the values assigned to
P[1], P[2], …, P[i-1], then set P[i] to <em>false</em>. This is basically
clauses that look like (<em>false</em> ∨ <em>false</em> ∨ … ∨ ¬ P[i]).</li>
<li>Otherwise, set P[i] to <em>true</em>.</li>
</ol>
</li>
</ol>
<p>The claim is that this procedure will always work, that is, none of these
assignments will make a clause false. To see this, suppose assigning P[i] did,
in fact, cause a clause to be false. Specifically, no clauses were falsified
by any of the previous assignments. Then the following could happen:</p>
<ol>
<li>That clause was empty from the beginning, and thus always false. We can
ignore this case because we’re assuming the set of resolved clauses does <em>not</em>
contain the empty clause.</li>
<li>The clause was of the form (<em>false</em> ∨ <em>false</em> ∨ … ∨ P[i]) and we
assigned P[i] to <em>false</em>. (Why is this the only other case?)</li>
</ol>
<p>If the latter case occurs, then we must also have (<em>false</em> ∨ <em>false</em> ∨
… ∨ ¬ P[i]), because that’s the only situation in which P[i] is
assigned false.</p>
<p>Now, here’s the crucial bit: these two clauses resolve! Since they contain P[i]
and ¬P[i], respectively, we resolve them to obtain a clause that has only
false values in it. This contradicts our assumption that no clauses were
falsified by any of the previous assignments.</p>
<p>So, we know that if the empty clause is not part of the set of resolved
clauses, then the clauses are satisfiable. By contrapositive, it follows that
you can always resolve some set of them to get the empty clause. Q.E.D. ■</p>
<hr>
<p>There’s another argument that explains this: an inductive one which you can
read <a href="http://www.mathcs.duq.edu/simon/Fall04/notes-6-20/node3.html">here</a>. In
short, it inducts on the total number of propositions, where the base case is
that if you have only one literal per clause, then either it’s satisfiable, or
it’s unsatisfiable and you can resolve to get the empty clause.</p>
<ul>
<li>Convince yourself that this base case is true.</li>
</ul>
<hr>
<p>So where are we? We have an algorithm that will definitely terminate on a valid
statement, though we have not yet said anything about what happens when it is
given anything else.</p>
<p>The resolution method should feel extremely powerful. Of course, as the number
of propositions increases, it will get exponentially slower (boolean
satisfiability was actually one of the first problems to be proved as
NP-complete—and, in fact, constraint solving algorithms like DPLL correspond
pretty much to resolution-refutation).</p>
<p>But that’s okay! It works!</p>
<p>One question you should have is, “What can I prove with propositional logic?”</p>
<ul>
<li>Can you use propositional logic to reason about the integers? Why or why not?</li>
</ul>
<p>Propositional logic is bound to a <em>finite</em> number of propositions. That means
you can’t say things like “1 is an integer”, “2 is an integer”, “3 is an
integer”, etc.</p>
<p>In the <a href="meet-the-robinson-3.html">next article</a>, we will extend propositional
logic to a much richer form that supports an infinite number of propositions,
and show that resolution-refutation still works.</p>
<ul>
<li>Write your own resolution theorem prover so that you can experiment with
some large proofs. It’s not hard; you can think of this as a code golf
challenge if you’d like.</li>
<li>Find three more things you liked and three more things that could be
improved about this article series, and report them to me.</li>
</ul>
</section>
<div id="comment-breaker">◊ ◊ ◊</div>
</article>
<footer id="footer">
<div>
<ul>
<li><a href="https://github.com/kach">
Github</a></li>
<li><a href="feed.xml">
Subscribe (RSS feed)</a></li>
<li><a href="https://twitter.com/hardmath123">
Twitter</a></li>
<li><a href="https://creativecommons.org/licenses/by-nc/3.0/deed.en_US">
CC BY-NC 3.0</a></li>
</ul>
</div>
<script>
(function(i,s,o,g,r,a,m){i['GoogleAnalyticsObject']=r;i[r]=i[r]||function(){
(i[r].q=i[r].q||[]).push(arguments)},i[r].l=1*new Date();a=s.createElement(o),
m=s.getElementsByTagName(o)[0];a.async=1;a.src=g;m.parentNode.insertBefore(a,m)
})(window,document,'script','//www.google-analytics.com/analytics.js','ga');
ga('create', 'UA-46120535-1', 'hardmath123.github.io');
ga('require', 'displayfeatures');
ga('send', 'pageview');
</script>
</footer>
</body>
</html>