WEBVTT
X-TIMESTAMP-MAP=LOCAL:00:00:00.000,MPEGTS:900000

00:00:00.000 --> 00:00:03.912
[MUSIC PLAYING]

00:00:17.707 --> 00:00:18.540
BRIAN YU: All right.

00:00:18.540 --> 00:00:21.420
Welcome back, everyone, to an
introduction to artificial intelligence

00:00:21.420 --> 00:00:22.470
with Python.

00:00:22.470 --> 00:00:24.510
Last time we took a
look at search problems

00:00:24.510 --> 00:00:26.820
in particular, where
we have AI agents that

00:00:26.820 --> 00:00:29.760
are trying to solve some sort
of problem by taking actions

00:00:29.760 --> 00:00:32.009
in some sort of environment,
whether that environment

00:00:32.009 --> 00:00:34.730
is trying to take actions
by playing moves in a game,

00:00:34.730 --> 00:00:37.980
or whether those actions are something
like trying to figure out where to make

00:00:37.980 --> 00:00:41.983
turns in order to get driving
directions from point A to point B.

00:00:41.983 --> 00:00:44.400
This time we're going to turn
our attention more generally

00:00:44.400 --> 00:00:46.470
to just this idea of knowledge.

00:00:46.470 --> 00:00:49.620
The idea that a lot of intelligence
is based on knowledge, especially

00:00:49.620 --> 00:00:51.510
if we think about human intelligence.

00:00:51.510 --> 00:00:53.130
People know information.

00:00:53.130 --> 00:00:54.900
We know facts about the world.

00:00:54.900 --> 00:00:57.030
And using that information
that we know, we're

00:00:57.030 --> 00:00:59.820
able to draw conclusions--
reason about the information

00:00:59.820 --> 00:01:03.570
that we know in order to figure out
how to do something or figure out

00:01:03.570 --> 00:01:07.230
some other piece of information that
we conclude based on the information we

00:01:07.230 --> 00:01:09.360
already have available to us.

00:01:09.360 --> 00:01:13.650
What we'd like to focus on now is the
ability to take this idea of knowledge

00:01:13.650 --> 00:01:15.630
and being able to reason
based on knowledge,

00:01:15.630 --> 00:01:18.570
and apply those ideas to
artificial intelligence.

00:01:18.570 --> 00:01:20.520
In particular, we're
going to be building what

00:01:20.520 --> 00:01:22.980
are known as knowledge-based agents.

00:01:22.980 --> 00:01:27.340
Agents that are able to reason and act
by representing knowledge internally.

00:01:27.340 --> 00:01:30.240
Somehow inside of our AI,
they have some understanding

00:01:30.240 --> 00:01:32.250
of what it means to know something.

00:01:32.250 --> 00:01:34.890
And ideally, they have some
algorithms, or some techniques

00:01:34.890 --> 00:01:37.740
they can use based on that
knowledge that they know in order

00:01:37.740 --> 00:01:40.980
to figure out the solution
to a problem, or figure out

00:01:40.980 --> 00:01:45.000
some additional piece of information
that can be helpful in some sense.

00:01:45.000 --> 00:01:47.400
So what do we mean by
reasoning based on knowledge

00:01:47.400 --> 00:01:48.960
to be able to draw conclusions?

00:01:48.960 --> 00:01:52.260
Well, let's look at a simple example
drawn from the world of Harry Potter.

00:01:52.260 --> 00:01:55.890
We take one sentence
that we know to be true.

00:01:55.890 --> 00:01:59.370
If it didn't rain, then
Harry visited Hagrid today.

00:01:59.370 --> 00:02:02.150
So one fact that we might
know about the world.

00:02:02.150 --> 00:02:03.480
And then we take another fact.

00:02:03.480 --> 00:02:07.081
Harry visited Hagrid or
Dumbledore today, but not both.

00:02:07.081 --> 00:02:08.789
So it tells us something
about the world.

00:02:08.789 --> 00:02:11.490
That Harry either visited
Hagrid but not Dumbledore,

00:02:11.490 --> 00:02:13.910
or Harry visited
Dumbledore but not Hagrid.

00:02:13.910 --> 00:02:16.410
And now we have a third piece
of information about the world

00:02:16.410 --> 00:02:19.020
that Harry visited Dumbledore today.

00:02:19.020 --> 00:02:21.240
So we now have three
pieces of information now.

00:02:21.240 --> 00:02:25.872
Three facts inside of a knowledge base,
so to speak-- information that we know.

00:02:25.872 --> 00:02:28.080
And now we, as humans, can
try and reason about this,

00:02:28.080 --> 00:02:30.720
and figure out based on
this information, what

00:02:30.720 --> 00:02:33.570
additional information
can we begin to conclude?

00:02:33.570 --> 00:02:35.730
And well, looking at
these last two statements,

00:02:35.730 --> 00:02:39.570
Harry either visited Hagrid
or Dumbledore but not both,

00:02:39.570 --> 00:02:41.882
and we know that Harry
visited Dumbledore today.

00:02:41.882 --> 00:02:43.590
Well, then it's pretty
reasonable that we

00:02:43.590 --> 00:02:46.620
could draw the conclusion that,
you know what, Harry must not

00:02:46.620 --> 00:02:48.120
have visited Hagrid today.

00:02:48.120 --> 00:02:50.790
Because based on a combination
of these two statements,

00:02:50.790 --> 00:02:53.010
we can draw this inference, so to speak.

00:02:53.010 --> 00:02:56.282
A conclusion that Harry
did not visit Hagrid today.

00:02:56.282 --> 00:02:59.490
But it turns out we can even do a little
bit better than that-- get some more

00:02:59.490 --> 00:03:02.010
information-- by taking a
look at this first statement

00:03:02.010 --> 00:03:03.480
and reasoning about that.

00:03:03.480 --> 00:03:08.222
This first statement says, if it didn't
rain, then Harry visited Hagrid today.

00:03:08.222 --> 00:03:09.180
So what does that mean?

00:03:09.180 --> 00:03:13.350
In all cases where it didn't rain,
then we know that Harry visited Hagrid.

00:03:13.350 --> 00:03:16.950
But if we also know now that
Harry did not visit Hagrid,

00:03:16.950 --> 00:03:19.743
then it tells us something
about our initial premise

00:03:19.743 --> 00:03:20.910
that we were thinking about.

00:03:20.910 --> 00:03:24.330
In particular, it tells
us that it did rain today.

00:03:24.330 --> 00:03:28.560
Because we can reason if it didn't rain,
that Harry would have visited Hagrid.

00:03:28.560 --> 00:03:33.150
But we know for a fact that
Harry did not visit Hagrid today.

00:03:33.150 --> 00:03:36.060
So it's this kind of reasoning,
the sort of logical reasoning

00:03:36.060 --> 00:03:38.250
where we use logic
based on the information

00:03:38.250 --> 00:03:42.113
that we know in order to take
information and reach conclusions.

00:03:42.113 --> 00:03:45.280
That is going to be the focus of what
we're going to be talking about today.

00:03:45.280 --> 00:03:48.810
How can we make our artificial
intelligence logical so

00:03:48.810 --> 00:03:52.860
that they can perform the same kinds of
deduction, the same kinds of reasoning

00:03:52.860 --> 00:03:54.960
that we've been doing so far.

00:03:54.960 --> 00:03:59.070
Of course, humans reason about logic
generally in terms of human language.

00:03:59.070 --> 00:04:02.490
That I just now was speaking
in English, talking in English,

00:04:02.490 --> 00:04:05.280
about these sentences and
trying to reason through how

00:04:05.280 --> 00:04:06.900
it is that they relate to one another.

00:04:06.900 --> 00:04:09.300
We're going to need to be a
little bit more formal when

00:04:09.300 --> 00:04:11.760
we turn our attention
to computers and being

00:04:11.760 --> 00:04:15.900
able to encode this notion of logic,
and truthhood and falsehood inside

00:04:15.900 --> 00:04:17.050
of a machine.

00:04:17.050 --> 00:04:20.310
So we're going to need to introduce a
few more terms and a few symbols that

00:04:20.310 --> 00:04:22.740
will help us reason
through this idea of logic

00:04:22.740 --> 00:04:24.780
inside of an artificial intelligence.

00:04:24.780 --> 00:04:27.107
And we'll begin with
the idea of a sentence.

00:04:27.107 --> 00:04:29.190
Now, a sentence in a natural
language like English

00:04:29.190 --> 00:04:32.340
is just something that I'm saying,
like what I'm saying right now.

00:04:32.340 --> 00:04:37.190
In the context of AI though, a sentence
is just an assertion about the world

00:04:37.190 --> 00:04:41.040
in what we're going to call a
knowledge representation language,

00:04:41.040 --> 00:04:45.413
some way of representing
knowledge inside of our computers.

00:04:45.413 --> 00:04:47.580
And the way that we're going
to spend most of today,

00:04:47.580 --> 00:04:49.710
reasoning about knowledge,
is through a type

00:04:49.710 --> 00:04:51.932
of logic known as propositional logic.

00:04:51.932 --> 00:04:55.140
There are a number of different types
of logic, some of which we'll touch on.

00:04:55.140 --> 00:04:59.280
But propositional logic is based
on a logic of propositions, or just

00:04:59.280 --> 00:05:01.090
statements about the world.

00:05:01.090 --> 00:05:03.510
And so we begin in propositional
logic with the notion

00:05:03.510 --> 00:05:05.400
of propositional symbols.

00:05:05.400 --> 00:05:08.430
We will have certain symbols
that are oftentimes just letters,

00:05:08.430 --> 00:05:12.090
something like P or Q or R,
where each of those symbols

00:05:12.090 --> 00:05:16.200
is going to represent some fact
or sentence about the world.

00:05:16.200 --> 00:05:20.160
So P, for example, might represent
the fact that it is raining.

00:05:20.160 --> 00:05:23.550
And so P is going to be a symbol
that represents that idea.

00:05:23.550 --> 00:05:27.300
And Q, for example, might represent
Harry visited Hagrid today.

00:05:27.300 --> 00:05:30.930
Each of these propositional
symbols represents some sentence

00:05:30.930 --> 00:05:33.660
or some fact about the world.

00:05:33.660 --> 00:05:36.750
But in addition to just having
individual facts about the world,

00:05:36.750 --> 00:05:40.380
we want some way to connect these
propositional symbols together

00:05:40.380 --> 00:05:44.880
in order to reason more complexly about
other facts that might exist inside

00:05:44.880 --> 00:05:46.560
of the world in which we're reasoning.

00:05:46.560 --> 00:05:49.740
So in order to do that, we'll need to
introduce some additional symbols that

00:05:49.740 --> 00:05:51.930
are known as logical connectives.

00:05:51.930 --> 00:05:54.150
Now, there are a number of
these logical connectives,

00:05:54.150 --> 00:05:57.275
but five of the most important, and
the ones we're going to focus on today,

00:05:57.275 --> 00:06:00.840
are these five up here, each
represented by a logical symbol.

00:06:00.840 --> 00:06:03.690
Not is represented by this symbol here.

00:06:03.690 --> 00:06:07.050
And is represented as sort
of an upside-down V. Or

00:06:07.050 --> 00:06:08.970
is represented by a V shape.

00:06:08.970 --> 00:06:11.910
Implication-- and we'll talk about
what that means in just a moment--

00:06:11.910 --> 00:06:13.680
is represented by an arrow.

00:06:13.680 --> 00:06:16.850
And biconditional-- again, we'll talk
about what that means in a moment--

00:06:16.850 --> 00:06:18.900
is represented by these double arrows.

00:06:18.900 --> 00:06:21.570
But these five logical
connectives are the main ones

00:06:21.570 --> 00:06:24.630
we're going to be focusing on
in terms of thinking about how

00:06:24.630 --> 00:06:27.270
it is that a computer
can reason about facts

00:06:27.270 --> 00:06:30.760
and draw conclusions based
on the facts that it knows.

00:06:30.760 --> 00:06:32.760
But in order to get there
we need to take a look

00:06:32.760 --> 00:06:36.480
at each of these logical connectives
and build up an understanding for what

00:06:36.480 --> 00:06:38.400
it is that they actually mean.

00:06:38.400 --> 00:06:40.950
So let's go ahead and
begin with the not symbol.

00:06:40.950 --> 00:06:42.570
So this not symbol here.

00:06:42.570 --> 00:06:45.510
And what we're going to show for
each of these logical connectives

00:06:45.510 --> 00:06:47.670
is what we're going
to call a truth table.

00:06:47.670 --> 00:06:50.280
A table that demonstrates
what this word not

00:06:50.280 --> 00:06:55.080
means when we attach it to a
propositional symbol or any sentence

00:06:55.080 --> 00:06:56.910
inside of our logical language.

00:06:56.910 --> 00:07:01.200
And so the truth table for
not is shown right here.

00:07:01.200 --> 00:07:04.680
If P-- some propositional symbol
or some other sentence, even--

00:07:04.680 --> 00:07:08.940
is false, then not P is true.

00:07:08.940 --> 00:07:13.290
And if P is true, then not P is false.

00:07:13.290 --> 00:07:15.540
So you can imagine
placing this not symbol

00:07:15.540 --> 00:07:18.420
in front of some sentence
of propositional logic.

00:07:18.420 --> 00:07:20.460
Just says the opposite of that.

00:07:20.460 --> 00:07:24.280
So if, for example, P
represented it is raining,

00:07:24.280 --> 00:07:28.230
then not P would represent the
idea that it is not raining.

00:07:28.230 --> 00:07:32.820
And as you might expect, if P is false,
meaning if the sentence it is raining

00:07:32.820 --> 00:07:37.200
is false, well, then the
sentence not P must be true.

00:07:37.200 --> 00:07:40.530
The sentence that it is not
raining is, therefore, true.

00:07:40.530 --> 00:07:44.310
So not, you can imagine, just takes
whatever is in P and it inverts it.

00:07:44.310 --> 00:07:47.730
It turns false into true,
and true into false.

00:07:47.730 --> 00:07:50.820
Much analogously to what
the English word not means.

00:07:50.820 --> 00:07:55.500
Just taking whatever comes after it
and inverting it to mean the opposite.

00:07:55.500 --> 00:07:58.080
Next up, and also very
English-like, is this idea

00:07:58.080 --> 00:08:02.460
of and, represented by this upside-down
V shape, or this point shape.

00:08:02.460 --> 00:08:05.760
And as opposed to just taking a
single argument the way not does--

00:08:05.760 --> 00:08:08.100
we have P and we have not P--

00:08:08.100 --> 00:08:11.370
and is going to combine
two different sentences

00:08:11.370 --> 00:08:13.440
and propositional logic together.

00:08:13.440 --> 00:08:16.760
So I might have one sentence
P and another sentence Q,

00:08:16.760 --> 00:08:21.110
and I want to combine them
together to say P and Q.

00:08:21.110 --> 00:08:24.300
And the general logic for
what P and Q means is it

00:08:24.300 --> 00:08:26.790
means that both of
its operands are true.

00:08:26.790 --> 00:08:30.910
P is true, and also, Q is true.

00:08:30.910 --> 00:08:33.480
And so here's what that
truth table looks like.

00:08:33.480 --> 00:08:36.360
This time we have two
variables, P and Q.

00:08:36.360 --> 00:08:39.840
And when we have two variables, each
of which can be in two possible states,

00:08:39.840 --> 00:08:42.820
true or false, that
leads to two squared,

00:08:42.820 --> 00:08:46.890
or four, possible combinations
of truth and falsehood.

00:08:46.890 --> 00:08:49.320
So we have P is false and Q is false.

00:08:49.320 --> 00:08:51.460
We have P is false and Q is true.

00:08:51.460 --> 00:08:53.040
P is true and Q is false.

00:08:53.040 --> 00:08:55.510
And then P and Q both are true.

00:08:55.510 --> 00:08:57.300
And those are the only
four possibilities

00:08:57.300 --> 00:08:59.650
for what P and Q could mean.

00:08:59.650 --> 00:09:03.750
And in each of those situations,
this third column here, P and Q,

00:09:03.750 --> 00:09:08.100
is telling us a little bit about what it
actually means for P and Q to be true.

00:09:08.100 --> 00:09:12.360
And we see that the only case where
P and Q is true is in this fourth row

00:09:12.360 --> 00:09:17.160
here, where P happens to be
true, Q also happens to be true.

00:09:17.160 --> 00:09:22.320
And in all other situations, P and
Q is going to evaluate to false.

00:09:22.320 --> 00:09:25.920
So this, again, is much in line with
what our intuition of and might mean.

00:09:25.920 --> 00:09:33.620
If I say P and Q, I probably mean
that I expect both P and Q to be true.

00:09:33.620 --> 00:09:36.620
Next up, also potentially
consistent with what we mean,

00:09:36.620 --> 00:09:39.680
is this word or, represented
by this V shape, sort

00:09:39.680 --> 00:09:42.020
of an upside-down and symbol.

00:09:42.020 --> 00:09:45.890
And or, as the name might suggest,
is true if either of its arguments

00:09:45.890 --> 00:09:46.550
are true.

00:09:46.550 --> 00:09:51.780
As long as P is true or Q is true,
then P or Q is going to be true.

00:09:51.780 --> 00:09:56.960
Which means the only time that P or
Q is false is if both of its operands

00:09:56.960 --> 00:09:57.710
are false.

00:09:57.710 --> 00:10:03.050
If P is false and Q is false,
then P or Q is going to be false.

00:10:03.050 --> 00:10:07.430
But in all other cases, if at
least one of the operands is true--

00:10:07.430 --> 00:10:08.880
maybe they're both true--

00:10:08.880 --> 00:10:12.890
in which case P or Q is
going to evaluate to true.

00:10:12.890 --> 00:10:16.760
Now, this is mostly consistent with the
way that most people might use the word

00:10:16.760 --> 00:10:19.603
or, in the sense of speaking
the word or in normal English.

00:10:19.603 --> 00:10:21.770
Though there is sometimes
when we might say or where

00:10:21.770 --> 00:10:24.620
we mean P or Q, but not both.

00:10:24.620 --> 00:10:27.770
Or we mean sort of it can
only be one or the other.

00:10:27.770 --> 00:10:33.220
It's important to note that this symbol
here, this or, means P or Q or both.

00:10:33.220 --> 00:10:34.640
That those are totally OK.

00:10:34.640 --> 00:10:38.210
As long as either or both of
them are true, then the or

00:10:38.210 --> 00:10:40.680
is going to evaluate to be true as well.

00:10:40.680 --> 00:10:43.040
It's only in the case
where all of the operands

00:10:43.040 --> 00:10:47.570
are false that P or Q ultimately
evaluates to false as well.

00:10:47.570 --> 00:10:51.200
In logic there's another symbol
known as the exclusive or, which

00:10:51.200 --> 00:10:55.188
encodes this idea of exclusivity of,
like, one or the other, but not both.

00:10:55.188 --> 00:10:57.230
But we're not going to be
focusing on that today.

00:10:57.230 --> 00:11:01.110
Whenever we talk about or, we're
always talking about either or both,

00:11:01.110 --> 00:11:05.830
in this case, as represented
by this truth table here.

00:11:05.830 --> 00:11:09.140
So that now is not, and an, and or.

00:11:09.140 --> 00:11:12.120
And next step is what we might
call implication, as denoted

00:11:12.120 --> 00:11:13.560
by this arrow symbol.

00:11:13.560 --> 00:11:16.860
So we have P and Q.
And this sentence here

00:11:16.860 --> 00:11:20.820
will generally read as
P implies Q. And what

00:11:20.820 --> 00:11:27.790
P implies Q means is that if P
is true, then Q is also true.

00:11:27.790 --> 00:11:32.040
So I might say something like, if it
is raining, then I will be indoors.

00:11:32.040 --> 00:11:36.140
Meaning it is raining
implies I will be indoors

00:11:36.140 --> 00:11:38.760
is the logical sentence
that I'm saying there.

00:11:38.760 --> 00:11:42.010
And the truth table for this can
sometimes be a little bit tricky.

00:11:42.010 --> 00:11:48.570
So obviously, if P is true and Q is
true, then P implies Q, that's true.

00:11:48.570 --> 00:11:50.400
That definitely makes sense.

00:11:50.400 --> 00:11:55.030
And it should also stand to reason
that when P is true and Q is false,

00:11:55.030 --> 00:11:56.880
then P implies Q is false.

00:11:56.880 --> 00:12:01.680
Because if I said to you, if it is
raining, then I will be indoors,

00:12:01.680 --> 00:12:05.640
and it is raining, but I'm
not indoors, well, then it

00:12:05.640 --> 00:12:08.940
would seem to be that my
original statement was not true.

00:12:08.940 --> 00:12:13.620
P implies Q means that if P is
true, then Q also needs to be true.

00:12:13.620 --> 00:12:17.670
And if it's not, well, then
the statement is false.

00:12:17.670 --> 00:12:21.840
Also worth noting, though, is
what happens when P is false.

00:12:21.840 --> 00:12:26.580
When P is false, the implication
makes no claim at all.

00:12:26.580 --> 00:12:30.960
If I say something like, if it is
raining, then I will be indoors,

00:12:30.960 --> 00:12:33.720
and it turns out it's not
raining, then in that case,

00:12:33.720 --> 00:12:35.910
I am not making any
statement as to whether

00:12:35.910 --> 00:12:38.130
or not I will be indoors or not.

00:12:38.130 --> 00:12:41.880
P implies Q just means that
if P is true, Q must be true.

00:12:41.880 --> 00:12:44.940
But if P is not true, then
we make no claim about

00:12:44.940 --> 00:12:47.440
whether or not Q is true at all.

00:12:47.440 --> 00:12:50.610
So in either case, if P is
false, it doesn't matter

00:12:50.610 --> 00:12:52.440
what Q is, whether it's false or true.

00:12:52.440 --> 00:12:54.900
We're not making any
claim about Q whatsoever.

00:12:54.900 --> 00:12:58.060
We can still evaluate
the implication to true.

00:12:58.060 --> 00:13:00.920
The only way that the
implication is ever false

00:13:00.920 --> 00:13:05.250
is if our premise, P is true, but
the conclusion that we're drawing,

00:13:05.250 --> 00:13:07.360
Q, happens to be false.

00:13:07.360 --> 00:13:13.710
So in that case, we would say P
does not imply Q in that case.

00:13:13.710 --> 00:13:17.520
Finally, the last connective that
we'll discuss is this biconditional.

00:13:17.520 --> 00:13:21.910
You can think of a biconditional as a
condition that goes in both directions.

00:13:21.910 --> 00:13:24.850
So originally, when I said
something like, if it is raining,

00:13:24.850 --> 00:13:26.880
then I will be indoors.

00:13:26.880 --> 00:13:29.280
I didn't say what would
happen if it wasn't raining.

00:13:29.280 --> 00:13:31.680
Maybe I'll be indoors,
maybe I'll be outdoors.

00:13:31.680 --> 00:13:35.760
This biconditional you can
read as an if and only if.

00:13:35.760 --> 00:13:41.280
So I can say, I will be indoors
if and only if it is raining.

00:13:41.280 --> 00:13:43.920
Meaning if it is raining,
then I will be indoors.

00:13:43.920 --> 00:13:47.910
And if I am indoors, it's reasonable
to conclude that it is also raining.

00:13:47.910 --> 00:13:52.960
So this biconditional is only
true when P and Q are the same.

00:13:52.960 --> 00:13:57.750
So if P is true and Q is true, then
this biconditional is also true--

00:13:57.750 --> 00:14:00.360
P implies Q. But also
the reverse is true.

00:14:00.360 --> 00:14:05.572
Q also implies P. So if P and
Q both happen to be false,

00:14:05.572 --> 00:14:06.780
we would still say it's true.

00:14:06.780 --> 00:14:10.050
But in any of these other two
situations, this P if and only

00:14:10.050 --> 00:14:13.260
if Q is going to ultimately
evaluate to false.

00:14:13.260 --> 00:14:15.540
So a lot of trues and
falses going on there,

00:14:15.540 --> 00:14:18.270
but these five basic
logical connectives are

00:14:18.270 --> 00:14:21.300
going to form the core of the
language of propositional logic,

00:14:21.300 --> 00:14:24.780
the language that we're going to
use in order to describe ideas,

00:14:24.780 --> 00:14:28.200
and the language that we're going to
use in order to reason about those ideas

00:14:28.200 --> 00:14:30.970
in order to draw conclusions.

00:14:30.970 --> 00:14:33.330
So let's now take a look at
some of the additional terms

00:14:33.330 --> 00:14:35.163
that we'll need to know
about in order to go

00:14:35.163 --> 00:14:38.070
about trying to form this
language of propositional logic,

00:14:38.070 --> 00:14:41.940
and writing AI that's actually able
to understand this sort of logic.

00:14:41.940 --> 00:14:43.950
The next thing we're going
to need is the notion

00:14:43.950 --> 00:14:46.930
of what is actually
true about the world.

00:14:46.930 --> 00:14:49.050
We have a whole bunch of
propositional symbols--

00:14:49.050 --> 00:14:51.210
P and Q and R and maybe others.

00:14:51.210 --> 00:14:54.450
But we need some way of knowing, like,
what actually is true in the world.

00:14:54.450 --> 00:14:58.680
Is P true or false, is Q true
or false, so on and so forth.

00:14:58.680 --> 00:15:01.870
And to do that, we'll introduce
the notion of a model.

00:15:01.870 --> 00:15:07.590
A model just assigns a truth value where
a truth value is either true or false

00:15:07.590 --> 00:15:10.120
to every propositional symbol.

00:15:10.120 --> 00:15:13.650
In other words, it's creating what
we might call a possible world.

00:15:13.650 --> 00:15:15.250
So let me give an example.

00:15:15.250 --> 00:15:18.090
If, for example, I have
two propositional symbols,

00:15:18.090 --> 00:15:22.230
P is it is raining, and
Q is it is a Tuesday,

00:15:22.230 --> 00:15:25.350
a model just takes each
of these two symbols

00:15:25.350 --> 00:15:29.050
and assigns a truth value to
them, either true or false.

00:15:29.050 --> 00:15:30.460
So here's a sample model.

00:15:30.460 --> 00:15:33.720
In this model, in other
words, in this possible world,

00:15:33.720 --> 00:15:38.320
it is possible that P is true,
meaning it is raining, and Q is false,

00:15:38.320 --> 00:15:40.260
meaning it is not a Tuesday.

00:15:40.260 --> 00:15:43.660
But there are other possible
worlds or other models as well.

00:15:43.660 --> 00:15:46.230
There is some model where both
of these variables are true.

00:15:46.230 --> 00:15:48.610
Some model where both of
these variables are false.

00:15:48.610 --> 00:15:52.620
In fact, if there are N variables that
are propositional symbols like this,

00:15:52.620 --> 00:15:56.010
that are either true or false,
then the number of possible models

00:15:56.010 --> 00:15:59.880
is two to the N, because each
of these possible models--

00:15:59.880 --> 00:16:02.250
possible variables
within my model could be

00:16:02.250 --> 00:16:08.130
set to either true or false, if I
don't know any information about it.

00:16:08.130 --> 00:16:09.803
So now that I have the symbols--

00:16:09.803 --> 00:16:11.720
the symbols and the
connectives that I'm going

00:16:11.720 --> 00:16:15.380
to need in order to construct
these parts of knowledge,

00:16:15.380 --> 00:16:17.690
we need some way to
represent that knowledge.

00:16:17.690 --> 00:16:20.180
And to do so, we're going
to allow our AI access

00:16:20.180 --> 00:16:22.700
to what we'll call a knowledge base.

00:16:22.700 --> 00:16:26.180
And a knowledge base is
really just a set of sentences

00:16:26.180 --> 00:16:28.590
that our AI knows to be true.

00:16:28.590 --> 00:16:31.460
Some set of sentences
in propositional logic

00:16:31.460 --> 00:16:35.340
that are things that our
AI knows about the world.

00:16:35.340 --> 00:16:38.510
And so we might tell our AI
some information, information

00:16:38.510 --> 00:16:40.910
about a situation that
it finds itself in,

00:16:40.910 --> 00:16:44.135
or situation about a problem that
it happens to be trying to solve.

00:16:44.135 --> 00:16:46.010
And we would give that
information to the AI,

00:16:46.010 --> 00:16:49.190
that the AI would store
inside of its knowledge base.

00:16:49.190 --> 00:16:51.710
And what happens next
is the AI would like

00:16:51.710 --> 00:16:54.140
to use that information
in the knowledge base

00:16:54.140 --> 00:16:57.810
to be able to draw conclusions
about the rest of the world.

00:16:57.810 --> 00:16:59.780
And what do those conclusions look like?

00:16:59.780 --> 00:17:01.613
Well, to understand
those conclusions, we'll

00:17:01.613 --> 00:17:04.400
need to introduce one more
idea, one more symbol, and that

00:17:04.400 --> 00:17:06.890
is the notion of entailment.

00:17:06.890 --> 00:17:10.803
So this sentence here, with this double
turnstile and these Greek letters--

00:17:10.803 --> 00:17:13.220
this is the Greek letter alpha
and the Greek letter beta--

00:17:13.220 --> 00:17:17.180
and we read this as alpha entails beta.

00:17:17.180 --> 00:17:21.589
And alpha and beta here are just
sentences in propositional logic.

00:17:21.589 --> 00:17:27.150
And what this means is that alpha
entails beta means that in every model,

00:17:27.150 --> 00:17:31.640
in other words, in every possible
world in which sentence a is true--

00:17:31.640 --> 00:17:35.880
or sentence alpha is true, then
sentence beta is also true.

00:17:35.880 --> 00:17:39.830
So if something entails something
else, if alpha entails beta,

00:17:39.830 --> 00:17:42.500
it means that if I
know alpha to be true,

00:17:42.500 --> 00:17:45.600
then beta must, therefore, also be true.

00:17:45.600 --> 00:17:52.160
So if my alpha is something like, I
know that it is a Tuesday in January,

00:17:52.160 --> 00:17:54.440
then a reasonable beta
might be something

00:17:54.440 --> 00:17:56.930
like, I know that it is January.

00:17:56.930 --> 00:17:59.810
Because in all worlds, where
it is a Tuesday in January,

00:17:59.810 --> 00:18:03.500
I know for sure that it must
be January, just by definition.

00:18:03.500 --> 00:18:06.230
This first statement, or
sentence about the world,

00:18:06.230 --> 00:18:08.150
entails the second statement.

00:18:08.150 --> 00:18:11.720
And we can reasonably use deduction,
based on that first sentence,

00:18:11.720 --> 00:18:16.640
to figure out that the second
sentence is, in fact, true as well.

00:18:16.640 --> 00:18:19.130
And ultimately, it's
this idea of entailment

00:18:19.130 --> 00:18:21.560
that we're going to try and
encode into our computer.

00:18:21.560 --> 00:18:24.500
We want our AI agent to
be able to figure out

00:18:24.500 --> 00:18:26.360
what the possible entailments are.

00:18:26.360 --> 00:18:30.380
We want our AI to be able to take
these three sentences, sentences like,

00:18:30.380 --> 00:18:32.750
if it didn't rain, Harry visited Hagrid.

00:18:32.750 --> 00:18:35.750
That Harry visited Hagrid
or Dumbledore but not both.

00:18:35.750 --> 00:18:37.460
And that Harry visited Dumbledore.

00:18:37.460 --> 00:18:40.340
And just using that
information, we'd like our AI

00:18:40.340 --> 00:18:45.350
to be able to infer, or figure out,
that using these three sentences inside

00:18:45.350 --> 00:18:48.380
of a knowledge base, we
can draw some conclusions.

00:18:48.380 --> 00:18:50.780
In particular, we can
draw the conclusions here

00:18:50.780 --> 00:18:53.810
that one, Harry did
not visit Hagrid today.

00:18:53.810 --> 00:18:58.140
And we can draw the entailment two,
that it did, in fact, rain today.

00:18:58.140 --> 00:19:00.130
And this process is known as inference.

00:19:00.130 --> 00:19:01.880
And that's what we're
going to be focusing

00:19:01.880 --> 00:19:06.230
on today, this process of deriving
new sentences from old ones.

00:19:06.230 --> 00:19:09.380
That I give you these three sentences,
you put them in the knowledge base

00:19:09.380 --> 00:19:13.970
in, say, the AI, and the AI is able to
use some sort of inference algorithm

00:19:13.970 --> 00:19:18.420
to figure out that these two
sentences must also be true.

00:19:18.420 --> 00:19:21.000
And that is how we define inference.

00:19:21.000 --> 00:19:23.060
So let's take a look
at an inference example

00:19:23.060 --> 00:19:26.840
to see how we might actually go about
inferring things in a human sense,

00:19:26.840 --> 00:19:29.720
before we take a more algorithmic
approach to see how we could

00:19:29.720 --> 00:19:31.670
encode this idea of inference in AI.

00:19:31.670 --> 00:19:35.240
And we'll see there are a number of
ways that we can actually achieve this.

00:19:35.240 --> 00:19:38.210
So again, we'll deal with a
couple of propositional symbols.

00:19:38.210 --> 00:19:41.930
We'll deal with P, Q and
R. P is it is a Tuesday.

00:19:41.930 --> 00:19:43.490
Q is it is raining.

00:19:43.490 --> 00:19:45.410
And R is Harry will go for a run.

00:19:45.410 --> 00:19:48.920
Three propositional symbols that
we are just defining to mean this.

00:19:48.920 --> 00:19:51.710
We're not saying anything yet about
whether they're true or false.

00:19:51.710 --> 00:19:54.220
We're just defining what they are.

00:19:54.220 --> 00:19:58.280
Now we'll give ourselves, or an
AI, access to a knowledge base,

00:19:58.280 --> 00:20:01.910
abbreviated to KB, to knowledge
that we know about the world.

00:20:01.910 --> 00:20:03.710
We know this statement.

00:20:03.710 --> 00:20:05.210
All right, so let's try to parse it.

00:20:05.210 --> 00:20:07.252
The parentheses here are
just used for precedent,

00:20:07.252 --> 00:20:09.530
so we can see what associates with what.

00:20:09.530 --> 00:20:15.763
But you would read this
as P and not Q implies R.

00:20:15.763 --> 00:20:17.180
All right, so what does that mean?

00:20:17.180 --> 00:20:18.800
Let's put it piece by piece.

00:20:18.800 --> 00:20:21.140
P is it is a Tuesday.

00:20:21.140 --> 00:20:22.790
Q is it is raining.

00:20:22.790 --> 00:20:25.910
So not Q is it is not raining.

00:20:25.910 --> 00:20:29.360
And implies R is Harry
will go for a run.

00:20:29.360 --> 00:20:33.140
So the way to read this entire sentence
in human natural language at least,

00:20:33.140 --> 00:20:39.760
is if it is a Tuesday and it is not
raining, then Harry will go for a run.

00:20:39.760 --> 00:20:43.820
So if it is a Tuesday and it is not
raining, then Harry will go for a run.

00:20:43.820 --> 00:20:45.900
And that is now inside
of our knowledge base.

00:20:45.900 --> 00:20:48.650
And let's now imagine that our
knowledge base has two other pieces

00:20:48.650 --> 00:20:49.770
of information as well.

00:20:49.770 --> 00:20:54.020
It has information that P is
true, that it is a Tuesday.

00:20:54.020 --> 00:20:58.160
And we also have the information
not Q, that it is not raining.

00:20:58.160 --> 00:21:01.430
That this sentence Q, it is
raining, happens to be false.

00:21:01.430 --> 00:21:04.130
And those are the three
sentences that we have access to.

00:21:04.130 --> 00:21:08.680
P and not Q implies R, P and not Q.

00:21:08.680 --> 00:21:12.280
Using that information, we should
be able to draw some inferences.

00:21:12.280 --> 00:21:18.410
P and not Q is only true if
both P and not Q are true.

00:21:18.410 --> 00:21:20.510
Well, all right, we know that P is true.

00:21:20.510 --> 00:21:22.520
And we know that not Q is true.

00:21:22.520 --> 00:21:24.910
So we know that this
whole expression is true.

00:21:24.910 --> 00:21:29.240
And the definition of implication is if
this whole thing on the left is true,

00:21:29.240 --> 00:21:31.400
then this thing on the
right must also be true.

00:21:31.400 --> 00:21:35.870
So if we know that P and not Q is
true, then R must be true as well.

00:21:35.870 --> 00:21:38.470
So the inference we should be
able to draw from all of this

00:21:38.470 --> 00:21:42.490
is that R is true, and we know
that Harry will go for a run,

00:21:42.490 --> 00:21:46.330
by taking this knowledge inside of our
knowledge base and being able to reason

00:21:46.330 --> 00:21:48.160
based on that idea.

00:21:48.160 --> 00:21:51.550
And so this ultimately, is the
beginning of what we might consider

00:21:51.550 --> 00:21:53.800
to be some sort of inference algorithm.

00:21:53.800 --> 00:21:57.820
Some process that we can use to
try and figure out whether or not

00:21:57.820 --> 00:21:59.380
we can draw some conclusion.

00:21:59.380 --> 00:22:02.380
And ultimately, what these inference
algorithms are going to answer

00:22:02.380 --> 00:22:05.260
is the central question
about entailment.

00:22:05.260 --> 00:22:07.090
Given some query about
the world, something

00:22:07.090 --> 00:22:10.450
we're wondering about the world,
and we'll call that query alpha,

00:22:10.450 --> 00:22:13.450
the question we want to ask,
using these inference algorithms,

00:22:13.450 --> 00:22:19.100
is does it KB, our knowledge
base, entail alpha?

00:22:19.100 --> 00:22:20.980
In other words, using
only the information

00:22:20.980 --> 00:22:24.520
we know inside of our knowledge base,
the knowledge that we have access to,

00:22:24.520 --> 00:22:28.540
can we conclude that this
sentence alpha is true?

00:22:28.540 --> 00:22:31.190
And that's ultimately
what we would like to do.

00:22:31.190 --> 00:22:32.480
So how can we do that?

00:22:32.480 --> 00:22:36.130
How can we go about writing an algorithm
that can look at this knowledge base

00:22:36.130 --> 00:22:40.060
and figure out whether or not
this query alpha is actually true?

00:22:40.060 --> 00:22:43.330
Well, it turns out there are a couple
of different algorithms for doing so.

00:22:43.330 --> 00:22:47.470
And one of the simplest, perhaps,
is known as model checking.

00:22:47.470 --> 00:22:49.960
Now remember, that a model
is just some assignment

00:22:49.960 --> 00:22:53.470
of all of the propositional symbols
inside of our language to a truth

00:22:53.470 --> 00:22:55.490
value, true or false.

00:22:55.490 --> 00:22:57.713
And you can think of a
model as a possible world.

00:22:57.713 --> 00:23:00.130
That there are many possible
worlds where different things

00:23:00.130 --> 00:23:01.430
might be true or false.

00:23:01.430 --> 00:23:03.260
And we can enumerate all of them.

00:23:03.260 --> 00:23:06.920
And the model checking
algorithm does exactly that.

00:23:06.920 --> 00:23:08.950
So what does our model
tracking algorithm do?

00:23:08.950 --> 00:23:11.530
Well, if we wanted to
determine if our knowledge

00:23:11.530 --> 00:23:14.470
base entails some query
alpha, then we are

00:23:14.470 --> 00:23:17.390
going to enumerate all possible models.

00:23:17.390 --> 00:23:21.030
In other words, consider all
possible values of true and false

00:23:21.030 --> 00:23:21.820
for our variables.

00:23:21.820 --> 00:23:25.640
All possible states in
which our world can be in.

00:23:25.640 --> 00:23:30.040
And if in every model where
our knowledge base is true,

00:23:30.040 --> 00:23:34.777
alpha is also true, then we know that
the knowledge base entails alpha.

00:23:34.777 --> 00:23:36.610
So let's take a closer
look at that sentence

00:23:36.610 --> 00:23:38.527
and try and figure out
what it actually means.

00:23:38.527 --> 00:23:42.430
If we know that in every model, in
other words, in every possible world,

00:23:42.430 --> 00:23:45.820
no matter what assignment of true
and false to variables you give,

00:23:45.820 --> 00:23:48.580
if we know that whenever
our knowledge is true--

00:23:48.580 --> 00:23:50.560
what we know to be true is true--

00:23:50.560 --> 00:23:53.680
that this query alpha is also true.

00:23:53.680 --> 00:23:57.250
Well, then it stands to reason that
as long as our knowledge base is true,

00:23:57.250 --> 00:24:00.152
then alpha must also be true.

00:24:00.152 --> 00:24:02.860
And so this is going to form the
foundation of our model checking

00:24:02.860 --> 00:24:03.550
algorithm.

00:24:03.550 --> 00:24:06.010
We're going to enumerate
all of the possible worlds,

00:24:06.010 --> 00:24:10.000
and ask ourselves, whenever the
knowledge base is true, is alpha true?

00:24:10.000 --> 00:24:13.630
And if that's the case, then
we know alpha to be true.

00:24:13.630 --> 00:24:15.820
And otherwise, there is no entailment.

00:24:15.820 --> 00:24:19.477
Our knowledge base
does not entail alpha.

00:24:19.477 --> 00:24:21.310
All right, so this is
a little bit abstract.

00:24:21.310 --> 00:24:25.260
But let's take a look at an example to
try and put real propositional symbols

00:24:25.260 --> 00:24:26.560
to this idea.

00:24:26.560 --> 00:24:28.740
So again, we'll work
with the same example.

00:24:28.740 --> 00:24:30.150
P is it is a Tuesday.

00:24:30.150 --> 00:24:31.470
Q is it is raining.

00:24:31.470 --> 00:24:33.510
R is Harry will go for a run.

00:24:33.510 --> 00:24:36.270
Our knowledge base contains
these pieces of information.

00:24:36.270 --> 00:24:40.710
P and not Q implies R. We
also know P, it is a Tuesday.

00:24:40.710 --> 00:24:43.140
And not Q, it is not raining.

00:24:43.140 --> 00:24:46.650
And our query, our alpha in this
case, the thing we want to ask

00:24:46.650 --> 00:24:49.860
is R. We want to know, is it guaranteed?

00:24:49.860 --> 00:24:53.530
Is it entailed that
Harry will go for a run.

00:24:53.530 --> 00:24:56.760
So the first step is to enumerate
all of the possible models.

00:24:56.760 --> 00:24:59.400
We have three propositional
symbols here, P, Q,

00:24:59.400 --> 00:25:04.110
and R, which means we have 2 to the
third power, or 8 possible models.

00:25:04.110 --> 00:25:04.980
All false.

00:25:04.980 --> 00:25:06.010
False, false, true.

00:25:06.010 --> 00:25:07.080
False, true, false.

00:25:07.080 --> 00:25:08.310
False, true, true.

00:25:08.310 --> 00:25:08.970
Et cetera.

00:25:08.970 --> 00:25:13.800
Eight possible ways you could assign
true and false to all of these models.

00:25:13.800 --> 00:25:18.210
And we might ask in each one of
them, is the knowledge base true?

00:25:18.210 --> 00:25:20.130
Here are the set of things that we know.

00:25:20.130 --> 00:25:24.420
In which of these worlds could this
knowledge base possibly apply to?

00:25:24.420 --> 00:25:27.340
In which world is this
knowledge base true?

00:25:27.340 --> 00:25:29.400
Well, in the knowledge
base, for example, we

00:25:29.400 --> 00:25:32.680
know P. Like, we know it is a Tuesday.

00:25:32.680 --> 00:25:37.260
Which means we know that these four--
first four rows-- where P is false,

00:25:37.260 --> 00:25:40.512
none of those are going to
be true, are going to work

00:25:40.512 --> 00:25:41.970
for this particular knowledge base.

00:25:41.970 --> 00:25:45.120
Our knowledge base is
not true in those worlds.

00:25:45.120 --> 00:25:50.490
Likewise, we also know not Q.
We know that it is not raining.

00:25:50.490 --> 00:25:54.690
So any of these models where Q is
true, like these two and these two

00:25:54.690 --> 00:25:59.640
here, those aren't going to work either
because we know that Q is not true.

00:25:59.640 --> 00:26:03.030
And finally, we also
know that P and not Q

00:26:03.030 --> 00:26:06.620
implies R. Which means
that when P is true--

00:26:06.620 --> 00:26:07.920
where P is true here--

00:26:07.920 --> 00:26:08.970
and Q is false--

00:26:08.970 --> 00:26:10.710
Q is false in these two--

00:26:10.710 --> 00:26:13.110
then R must be true.

00:26:13.110 --> 00:26:18.810
And if ever P is true, Q is
false, but R is also false,

00:26:18.810 --> 00:26:22.050
well, that doesn't satisfy
this implication here.

00:26:22.050 --> 00:26:26.260
That implication does not hold
true under those situations.

00:26:26.260 --> 00:26:28.380
So we could say that
for our knowledge base,

00:26:28.380 --> 00:26:32.280
we can conclude under which of these
possible worlds is our knowledge base

00:26:32.280 --> 00:26:36.180
true, and under which of the possible
worlds is our knowledge base false.

00:26:36.180 --> 00:26:39.510
And it turns out there is
only one possible world where

00:26:39.510 --> 00:26:41.310
our knowledge base is actually true.

00:26:41.310 --> 00:26:43.560
In some cases, there might
be multiple possible worlds

00:26:43.560 --> 00:26:44.935
where the knowledge base is true.

00:26:44.935 --> 00:26:47.625
But in this case it just so
happens that there's only one.

00:26:47.625 --> 00:26:50.100
One possible world where
we can definitively

00:26:50.100 --> 00:26:52.650
say something about our knowledge base.

00:26:52.650 --> 00:26:55.180
And in this case, we
would look at the query.

00:26:55.180 --> 00:26:57.750
The query of R. Is R true?

00:26:57.750 --> 00:26:59.040
R is true.

00:26:59.040 --> 00:27:03.110
And so as a result, we
can draw that conclusion.

00:27:03.110 --> 00:27:05.400
And so this is this
idea of model checking.

00:27:05.400 --> 00:27:08.880
Enumerate all the possible models,
and look in those possible models

00:27:08.880 --> 00:27:12.300
to see whether or not if
our knowledge base is true,

00:27:12.300 --> 00:27:15.658
is the query in question true as well.

00:27:15.658 --> 00:27:17.700
So let's now take a look
at how we might actually

00:27:17.700 --> 00:27:20.640
go about writing this in a
programming language like Python.

00:27:20.640 --> 00:27:22.560
Take a look at some
actual code that would

00:27:22.560 --> 00:27:24.810
encode this notion of
propositional symbols,

00:27:24.810 --> 00:27:29.070
and logic, and these connectives, like
and, and or, and not an implication,

00:27:29.070 --> 00:27:32.560
and so forth, and see what that
code might actually look like.

00:27:32.560 --> 00:27:35.097
So I've written in
advance a logic library.

00:27:35.097 --> 00:27:37.680
It's more detailed than we need
to worry about entirely today.

00:27:37.680 --> 00:27:40.350
But the important thing
is that we have one class

00:27:40.350 --> 00:27:45.010
for every type of logical symbol,
or connective, that we might have.

00:27:45.010 --> 00:27:47.490
So we just have one class
for logical symbols,

00:27:47.490 --> 00:27:51.030
for example, where every symbol
is going to represent and store

00:27:51.030 --> 00:27:53.670
some name for that particular symbol.

00:27:53.670 --> 00:27:57.240
And we also have a class for
not, that takes an operand.

00:27:57.240 --> 00:28:00.630
So we might say not one symbol
to say something is not true,

00:28:00.630 --> 00:28:02.520
or some other sentence is not true.

00:28:02.520 --> 00:28:06.450
We have one for and, one
for or, so on and so forth.

00:28:06.450 --> 00:28:08.170
And I'll just demonstrate
how this works.

00:28:08.170 --> 00:28:11.740
And you can take a look at
the actual logic.py later on.

00:28:11.740 --> 00:28:15.140
But go ahead and call
this file, Harry.py.

00:28:15.140 --> 00:28:19.380
We're going to store information
about this world of Harry Potter,

00:28:19.380 --> 00:28:20.520
for example.

00:28:20.520 --> 00:28:23.430
So I'll go ahead and import
from my logic module.

00:28:23.430 --> 00:28:24.930
I'll import everything.

00:28:24.930 --> 00:28:29.790
And in this library, in order to create
a symbol, you use capital S symbol.

00:28:29.790 --> 00:28:35.110
And I'll create a symbol for rain
to mean it is raining, for example.

00:28:35.110 --> 00:28:38.340
And I'll create a symbol
for Hagrid to mean

00:28:38.340 --> 00:28:41.150
Harry visited Hagrid is what
the symbol is going to mean.

00:28:41.150 --> 00:28:43.230
So this symbol means it is raining.

00:28:43.230 --> 00:28:46.230
This symbol means Harry visited Hagrid.

00:28:46.230 --> 00:28:49.830
And I'll add another
symbol called Dumbledore

00:28:49.830 --> 00:28:54.030
for Harry visited Dumbledore.

00:28:54.030 --> 00:28:56.700
Now I'd like to save these symbols
so that I can use them later,

00:28:56.700 --> 00:28:58.463
as I do some logical analysis.

00:28:58.463 --> 00:29:01.130
So I'll go ahead and save each
one of them inside of a variable.

00:29:01.130 --> 00:29:04.440
So, like, rain, Hagrid,
and Dumbledore, that you

00:29:04.440 --> 00:29:06.870
could call the variables anything.

00:29:06.870 --> 00:29:08.670
And now that I have
these logical symbols,

00:29:08.670 --> 00:29:12.160
I can use logical connectives
to combine them together.

00:29:12.160 --> 00:29:19.030
So for example, if I have a
sentence like, and rain and Hagrid,

00:29:19.030 --> 00:29:19.790
for example--

00:29:19.790 --> 00:29:22.870
which is not necessarily true,
but just for demonstration--

00:29:22.870 --> 00:29:26.420
I can now try and print
out sentence.formula,

00:29:26.420 --> 00:29:29.740
which is a function I wrote that takes
a sentence and propositional logic

00:29:29.740 --> 00:29:31.870
and just prints it out so
that we, the programmers,

00:29:31.870 --> 00:29:35.230
can now see this in order to get an
understanding for how it actually

00:29:35.230 --> 00:29:36.290
works.

00:29:36.290 --> 00:29:40.570
So if I run Python
Harry.py, what we'll see

00:29:40.570 --> 00:29:44.350
is this sentence and propositional
logic, rain and Hagrid.

00:29:44.350 --> 00:29:46.780
This is the logical
representation of what

00:29:46.780 --> 00:29:49.180
we have here in our
Python program of saying

00:29:49.180 --> 00:29:52.360
and, whose arguments
are rain and Hagrid.

00:29:52.360 --> 00:29:56.130
So we're saying rain and
Hagrid by encoding that idea.

00:29:56.130 --> 00:29:59.010
And this is quite common in
Python object-oriented programming

00:29:59.010 --> 00:30:01.100
where you have a number
of different classes,

00:30:01.100 --> 00:30:04.270
and you pass arguments into
them in order to create a new

00:30:04.270 --> 00:30:08.110
and object, for example, in
order to represent this idea.

00:30:08.110 --> 00:30:11.800
But now what I'd like to do is
somehow encode the knowledge

00:30:11.800 --> 00:30:13.930
that I have about the
world, in order to solve

00:30:13.930 --> 00:30:15.790
that problem from the
beginning of class,

00:30:15.790 --> 00:30:18.700
where we talked about trying to
figure out who Harry visited,

00:30:18.700 --> 00:30:21.550
and trying to figure out if it's
raining or if it's not raining.

00:30:21.550 --> 00:30:23.830
And so what knowledge do I have?

00:30:23.830 --> 00:30:26.990
I'll go ahead and create a
new variable called knowledge.

00:30:26.990 --> 00:30:27.830
And what do I know?

00:30:27.830 --> 00:30:29.663
Well, I know the very
first sentence that we

00:30:29.663 --> 00:30:33.370
talked about was the idea that
if it is not raining, then

00:30:33.370 --> 00:30:35.060
Harry will visit Hagrid.

00:30:35.060 --> 00:30:35.560
All right.

00:30:35.560 --> 00:30:38.020
How do I encode the idea
that it is not raining?

00:30:38.020 --> 00:30:40.920
Well, I can use not and
then the rain symbol.

00:30:40.920 --> 00:30:43.510
So here's me saying
that it is not raining.

00:30:43.510 --> 00:30:49.300
And now the implication is that if it is
not raining, then Harry visited Hagrid.

00:30:49.300 --> 00:30:52.000
So I'll wrap this
inside of an implication

00:30:52.000 --> 00:30:56.530
to say, if it is not raining, this
first argument to the implication,

00:30:56.530 --> 00:31:00.930
well, then Harry visited Hagrid.

00:31:00.930 --> 00:31:04.680
So I'm saying implication, the
premise is that it's not raining.

00:31:04.680 --> 00:31:08.270
And if it is not raining,
then Harry visited Hagrid.

00:31:08.270 --> 00:31:11.940
And I can print out knowledge.formula
to see the logical formula

00:31:11.940 --> 00:31:13.990
equivalent of that same idea.

00:31:13.990 --> 00:31:17.760
So I run Python of Harry.py,
and this is the logical formula

00:31:17.760 --> 00:31:20.370
that we see as a result, which
is a text-based version of what

00:31:20.370 --> 00:31:21.600
we were looking at before.

00:31:21.600 --> 00:31:27.540
That if it is not raining, then that
implies that Harry visited Hagrid.

00:31:27.540 --> 00:31:31.000
But there was additional information
that we had access to as well.

00:31:31.000 --> 00:31:34.050
In this case, we had access
to the fact that Harry

00:31:34.050 --> 00:31:37.320
visited either Hagrid or Dumbledore.

00:31:37.320 --> 00:31:38.478
So how do I encode that?

00:31:38.478 --> 00:31:40.270
Well, this means that
in my knowledge, I've

00:31:40.270 --> 00:31:42.720
really got multiple pieces
of knowledge going on.

00:31:42.720 --> 00:31:45.750
I know one thing, and another
thing, and another thing.

00:31:45.750 --> 00:31:49.475
So I'll go ahead and wrap all of
my knowledge inside of an and.

00:31:49.475 --> 00:31:51.850
And I'll move things on a new
line just for good measure.

00:31:51.850 --> 00:31:53.400
But I know multiple things.

00:31:53.400 --> 00:31:57.010
So I'm saying knowledge is an and
of multiple different sentences.

00:31:57.010 --> 00:32:00.190
I know multiple different
sentences to be true.

00:32:00.190 --> 00:32:03.570
One such sentence that I know
to be true is this implication

00:32:03.570 --> 00:32:06.900
that if it is not raining,
then Harry visited Hagrid.

00:32:06.900 --> 00:32:12.960
Another such sentence that I know
to be true is or Hagrid Dumbledore.

00:32:12.960 --> 00:32:16.710
In other words, so Hagrid
or Dumbledore is true,

00:32:16.710 --> 00:32:20.580
because I know that Harry
visited Hagrid or Dumbledore.

00:32:20.580 --> 00:32:22.080
But I know more than that, actually.

00:32:22.080 --> 00:32:24.720
That initial sentence from
before said that Harry visited

00:32:24.720 --> 00:32:27.730
Hagrid or Dumbledore, but not both.

00:32:27.730 --> 00:32:30.870
So now I want a sentence that'll
encode the idea that Harry didn't

00:32:30.870 --> 00:32:34.140
visit both Hagrid and Dumbledore.

00:32:34.140 --> 00:32:37.440
Well, the notion of Harry
visiting Hagrid and Dumbledore

00:32:37.440 --> 00:32:39.000
would be represented like this.

00:32:39.000 --> 00:32:42.720
And of Hagrid and Dumbledore.

00:32:42.720 --> 00:32:46.290
And if that is not true, I want
to say not that, then I'll just

00:32:46.290 --> 00:32:50.310
wrap this whole thing inside of a not.

00:32:50.310 --> 00:32:54.510
So now these three lines, line 8
says that if it is not raining, then

00:32:54.510 --> 00:32:56.040
Harry visited Hagrid.

00:32:56.040 --> 00:33:00.060
Line 9 says Harry visited
Hagrid or Dumbledore.

00:33:00.060 --> 00:33:05.280
And line 10 says Harry didn't
visit both Hagrid and Dumbledore.

00:33:05.280 --> 00:33:09.510
That it is not true that both the
Hagrid symbol and the Dumbledore symbol

00:33:09.510 --> 00:33:10.330
are true.

00:33:10.330 --> 00:33:12.570
Only one of them can be true.

00:33:12.570 --> 00:33:15.690
And finally, the last piece
of information that I knew

00:33:15.690 --> 00:33:19.620
was the fact that Harry
visited Dumbledore.

00:33:19.620 --> 00:33:22.440
So these now are the pieces
of knowledge that I know.

00:33:22.440 --> 00:33:25.730
One sentence, and another
sentence, and another, and another.

00:33:25.730 --> 00:33:28.920
And I can print out what I know, just
to see it a little bit more visually.

00:33:28.920 --> 00:33:32.970
And here now is a logical
representation of the information

00:33:32.970 --> 00:33:35.670
that my computer is now
internally representing

00:33:35.670 --> 00:33:38.070
using these various
different Python objects.

00:33:38.070 --> 00:33:41.460
And again, take a look at logic.py if
you want to take a look at how exactly

00:33:41.460 --> 00:33:42.420
it's implementing this.

00:33:42.420 --> 00:33:45.040
But no need to worry too much
about all of the details there.

00:33:45.040 --> 00:33:49.140
We're here saying that if it is not
raining, then Harry visited Hagrid.

00:33:49.140 --> 00:33:52.230
We're saying that Hagrid
or Dumbledore is true.

00:33:52.230 --> 00:33:56.910
And we're saying it is not the case
that Hagrid and Dumbledore is true.

00:33:56.910 --> 00:33:58.470
That they're not both true.

00:33:58.470 --> 00:34:01.720
And we also know that
Dumbledore is true.

00:34:01.720 --> 00:34:05.550
So this long, logical sentence
represents our knowledge base.

00:34:05.550 --> 00:34:07.670
It is the thing that we know.

00:34:07.670 --> 00:34:12.090
And now what we like to do is we like
to use model checking to ask a query.

00:34:12.090 --> 00:34:14.639
To ask a question like,
based on this information,

00:34:14.639 --> 00:34:16.525
do I know whether or not it's raining?

00:34:16.525 --> 00:34:18.900
And we, as humans, we're able
to logic our way through it

00:34:18.900 --> 00:34:22.108
and figure out that, all right, based
on these sentences we can conclude this

00:34:22.108 --> 00:34:24.750
and that to figure out that
yes, it must have been raining.

00:34:24.750 --> 00:34:28.090
But now we'd like for the
computer to do that as well.

00:34:28.090 --> 00:34:30.480
So let's take a look at the
model checking algorithm that

00:34:30.480 --> 00:34:32.760
is going to follow that same
pattern that we drew out

00:34:32.760 --> 00:34:34.763
in pseudocode a moment ago.

00:34:34.763 --> 00:34:36.555
So I've defined a
function here in logic.py

00:34:36.555 --> 00:34:40.199
that you can take a look
at called model check.

00:34:40.199 --> 00:34:43.770
Model check takes two arguments,
the knowledge that I already know

00:34:43.770 --> 00:34:45.330
and the query.

00:34:45.330 --> 00:34:47.730
And the idea is, in order
to do model checking,

00:34:47.730 --> 00:34:50.440
I need to enumerate all
of the possible models.

00:34:50.440 --> 00:34:53.580
And for each of the possible
models, I need to ask myself,

00:34:53.580 --> 00:34:57.110
is the knowledge base true,
and is the query true?

00:34:57.110 --> 00:34:58.860
So the first thing I
need to do is somehow

00:34:58.860 --> 00:35:01.050
enumerate all of the possible models.

00:35:01.050 --> 00:35:03.750
Meaning for all possible
symbols that exist,

00:35:03.750 --> 00:35:06.750
I need to assign true and
false to each one of them

00:35:06.750 --> 00:35:09.312
and see whether or not it's still true.

00:35:09.312 --> 00:35:11.820
And so here is the way
we're going to do that.

00:35:11.820 --> 00:35:13.067
We're going to start--

00:35:13.067 --> 00:35:15.150
so I've defined another
helper function internally

00:35:15.150 --> 00:35:16.690
that we'll get to in just a moment.

00:35:16.690 --> 00:35:20.100
But this function starts by
getting all of the symbols,

00:35:20.100 --> 00:35:23.008
in both the knowledge and
the query, by figuring out

00:35:23.008 --> 00:35:24.300
what symbols am I dealing with?

00:35:24.300 --> 00:35:26.070
In this case, the
symbols I'm dealing with

00:35:26.070 --> 00:35:28.410
are rain, and Hagrid, and Dumbledore.

00:35:28.410 --> 00:35:30.870
But there might be other symbols,
depending on the problem.

00:35:30.870 --> 00:35:33.960
And we'll take a look soon at
some examples of situations

00:35:33.960 --> 00:35:37.170
where ultimately, we're going to
need some additional symbols in order

00:35:37.170 --> 00:35:39.000
to represent the problem.

00:35:39.000 --> 00:35:42.510
And then we're going to run
this check all function, which

00:35:42.510 --> 00:35:46.260
is a helper function that's basically
going to recursively call itself,

00:35:46.260 --> 00:35:51.180
checking every possible configuration
of propositional symbols.

00:35:51.180 --> 00:35:56.560
So we start out by looking at this
check all function, and what do we do?

00:35:56.560 --> 00:36:01.350
So if not symbols means if we
finish assigning all of the symbols.

00:36:01.350 --> 00:36:03.120
We've assigned every symbol of value.

00:36:03.120 --> 00:36:07.580
So far we haven't done that, but
if we ever do, then we check.

00:36:07.580 --> 00:36:09.697
In this model, is the knowledge true?

00:36:09.697 --> 00:36:11.030
That's what this line is saying.

00:36:11.030 --> 00:36:14.300
If we evaluate the knowledge,
propositional logic formula,

00:36:14.300 --> 00:36:18.590
using the models assignment of
truth values, is the knowledge true?

00:36:18.590 --> 00:36:23.780
If the knowledge is true, then we should
return true, only if the query is true.

00:36:23.780 --> 00:36:27.590
Because if the knowledge is true, we
want the query to be true as well,

00:36:27.590 --> 00:36:29.750
in order for there to be entailment.

00:36:29.750 --> 00:36:32.150
Otherwise, we don't know
that there-- otherwise, there

00:36:32.150 --> 00:36:33.350
won't be an entailment.

00:36:33.350 --> 00:36:37.280
If there's ever a situation where
what we know in our knowledge is true,

00:36:37.280 --> 00:36:40.565
but the query, the thing we're
asking, happens to be false.

00:36:40.565 --> 00:36:42.440
So this line here is
checking that same idea.

00:36:42.440 --> 00:36:48.320
That in all worlds where the knowledge
is true, the query must also be true.

00:36:48.320 --> 00:36:52.010
Otherwise, we can just return true,
because if the knowledge isn't true,

00:36:52.010 --> 00:36:52.913
then we don't care.

00:36:52.913 --> 00:36:54.830
This is equivalent to
when we were enumerating

00:36:54.830 --> 00:36:56.540
this table from a moment ago.

00:36:56.540 --> 00:36:59.540
In all situations where the
knowledge base wasn't true--

00:36:59.540 --> 00:37:01.190
all of these seven rows here--

00:37:01.190 --> 00:37:04.460
we didn't care whether or not
our query was true or not.

00:37:04.460 --> 00:37:07.370
We only care to check
whether the query is true

00:37:07.370 --> 00:37:09.800
when the knowledge
base is actually true,

00:37:09.800 --> 00:37:13.130
which was just this green
highlighted row right there.

00:37:13.130 --> 00:37:16.850
So that logic is encoded
using that statement there.

00:37:16.850 --> 00:37:19.490
And otherwise, if we haven't
assigned symbols yet,

00:37:19.490 --> 00:37:22.490
which we haven't seen anything
yet, then the first thing we do

00:37:22.490 --> 00:37:24.920
is pop one of the symbols.

00:37:24.920 --> 00:37:27.800
I make a copy of the symbols first,
just to save an existing copy.

00:37:27.800 --> 00:37:30.500
But I pop one symbol off
of the remaining symbols,

00:37:30.500 --> 00:37:33.380
so that I just pick
one symbol at random.

00:37:33.380 --> 00:37:37.970
And I create one copy of the
model where that symbol is true,

00:37:37.970 --> 00:37:42.350
and I create a second copy of the
model where that symbol is false.

00:37:42.350 --> 00:37:44.240
So I now have two copies of the model.

00:37:44.240 --> 00:37:47.480
One where the symbol is true, and
one where the symbol is false.

00:37:47.480 --> 00:37:50.330
And I need to make sure
that this entailment holds

00:37:50.330 --> 00:37:52.190
in both of those models.

00:37:52.190 --> 00:37:56.480
So I recursively check all on the
model where the statement is true,

00:37:56.480 --> 00:38:01.283
and check all on the model
where the statement is false.

00:38:01.283 --> 00:38:03.200
So again, you can take
a look at that function

00:38:03.200 --> 00:38:06.443
to try to get a sense for how
exactly this logic is working.

00:38:06.443 --> 00:38:09.110
But in effect, what it's doing
is recursively calling this check

00:38:09.110 --> 00:38:11.330
all function again and again and again.

00:38:11.330 --> 00:38:14.090
And on every level of the
recursion we're saying,

00:38:14.090 --> 00:38:17.600
let's pick a new symbol that
we haven't yet assigned.

00:38:17.600 --> 00:38:18.830
Assign it to true.

00:38:18.830 --> 00:38:20.430
And assign it to false.

00:38:20.430 --> 00:38:23.690
And then check to make sure that
the entailment holds in both cases.

00:38:23.690 --> 00:38:26.480
Because ultimately, I need to
check every possible world.

00:38:26.480 --> 00:38:28.700
I need to take every
combination of symbols

00:38:28.700 --> 00:38:31.820
and try every combination
of true and false

00:38:31.820 --> 00:38:36.040
in order to figure out whether the
entailment relation actually holds.

00:38:36.040 --> 00:38:38.730
So that function we've written for you.

00:38:38.730 --> 00:38:42.560
But in order to use that function
inside of Harry.py, what I'll write

00:38:42.560 --> 00:38:43.850
is something like this.

00:38:43.850 --> 00:38:47.600
I would like to model check,
based on the knowledge,

00:38:47.600 --> 00:38:50.570
and then I provide, as a second
argument, what the query is.

00:38:50.570 --> 00:38:52.430
What the thing I want to ask is.

00:38:52.430 --> 00:38:56.170
And what I want to ask in
this case is, is it raining?

00:38:56.170 --> 00:38:58.460
So model check, again,
takes two arguments.

00:38:58.460 --> 00:39:01.090
The first argument is the
information that I know.

00:39:01.090 --> 00:39:01.780
This knowledge.

00:39:01.780 --> 00:39:06.250
Which in this case, is this information
that was given to me at the beginning.

00:39:06.250 --> 00:39:11.110
And the second argument, rain, is
encoding the idea of the query.

00:39:11.110 --> 00:39:12.040
What am I asking?

00:39:12.040 --> 00:39:14.410
I would like to ask,
based on this knowledge,

00:39:14.410 --> 00:39:17.460
do I know for sure that it is raining?

00:39:17.460 --> 00:39:21.590
And I can try and print
out the result of that.

00:39:21.590 --> 00:39:24.930
And when I run this program,
I see that the answer is true.

00:39:24.930 --> 00:39:29.080
That based on this information, I can
conclusively say that it is raining.

00:39:29.080 --> 00:39:31.090
Because using this model
checking algorithm,

00:39:31.090 --> 00:39:35.230
we were able to check that in every
world where this knowledge is true,

00:39:35.230 --> 00:39:36.010
it is raining.

00:39:36.010 --> 00:39:39.550
In other words, there's no world
where this knowledge is true

00:39:39.550 --> 00:39:41.000
and it is not raining.

00:39:41.000 --> 00:39:45.500
So you can conclude that
it is, in fact, raining.

00:39:45.500 --> 00:39:47.950
And this sort of logic
can be applied to a number

00:39:47.950 --> 00:39:49.450
of different types of problems.

00:39:49.450 --> 00:39:53.170
That if confronted with a problem
where some sort of logical deduction

00:39:53.170 --> 00:39:55.330
can be used in order
to try to solve it, you

00:39:55.330 --> 00:39:58.150
might try thinking about
what propositional symbols

00:39:58.150 --> 00:40:00.760
you might need in order to
represent that information.

00:40:00.760 --> 00:40:03.220
And what statements
and propositional logic

00:40:03.220 --> 00:40:07.710
you might use in order to encode
that information which you know.

00:40:07.710 --> 00:40:10.030
And this process of
trying to take a problem

00:40:10.030 --> 00:40:12.730
and figure out what propositional
symbols to use in order

00:40:12.730 --> 00:40:15.850
to encode that idea, or how
to represent it logically

00:40:15.850 --> 00:40:17.950
is known as knowledge engineering.

00:40:17.950 --> 00:40:20.830
That software engineers and AI
engineers will take a problem

00:40:20.830 --> 00:40:23.980
and try and figure out how to
distill it down into knowledge

00:40:23.980 --> 00:40:26.847
that is representable by a computer.

00:40:26.847 --> 00:40:29.680
And if we can take any general
purpose problem, some problem that we

00:40:29.680 --> 00:40:32.700
find in the human world,
and turn it into a problem

00:40:32.700 --> 00:40:35.110
that computer's know how
to solve, as by using

00:40:35.110 --> 00:40:37.610
any number of different
variables, well, then, we

00:40:37.610 --> 00:40:39.610
can take a computer that
is able to do something

00:40:39.610 --> 00:40:42.250
like model checking or some
other inference algorithm,

00:40:42.250 --> 00:40:46.250
and actually figure out
how to solve that problem.

00:40:46.250 --> 00:40:49.598
So now we'll take a look at two or
three examples of knowledge engineering

00:40:49.598 --> 00:40:50.140
and practice.

00:40:50.140 --> 00:40:54.460
Of taking some problem and figuring
out how we can apply logical symbols

00:40:54.460 --> 00:40:58.300
and use logical formulas to
be able to encode that idea.

00:40:58.300 --> 00:41:01.270
And we'll start with a very popular
board game in the US and the UK,

00:41:01.270 --> 00:41:02.270
known as Clue.

00:41:02.270 --> 00:41:05.170
Now, in the game of Clue, there's
a number of different factors

00:41:05.170 --> 00:41:06.140
that are going on.

00:41:06.140 --> 00:41:08.680
But the basic premise of the game
if you've never played it before,

00:41:08.680 --> 00:41:10.680
is that there are a number
of different people--

00:41:10.680 --> 00:41:13.420
for now we'll just use three,
Colonel Mustard, Professor Plum,

00:41:13.420 --> 00:41:14.330
and Miss Scarlet.

00:41:14.330 --> 00:41:17.080
There are a number of different
rooms, like a ballroom, a kitchen,

00:41:17.080 --> 00:41:17.870
and a library.

00:41:17.870 --> 00:41:20.620
And there are a number of different
weapons-- a knife, a revolver,

00:41:20.620 --> 00:41:21.700
and a wrench.

00:41:21.700 --> 00:41:26.140
And three of these-- one person,
one room, and one weapon--

00:41:26.140 --> 00:41:29.500
is the solution to the mystery--

00:41:29.500 --> 00:41:32.788
the murderer and what room they were
in, and what weapon they happen to use.

00:41:32.788 --> 00:41:35.830
And what happens at the beginning of
the game is that all these cards are

00:41:35.830 --> 00:41:38.740
randomly shuffled together, and
three of them-- one person, one room,

00:41:38.740 --> 00:41:39.670
and one weapon--

00:41:39.670 --> 00:41:42.100
are placed into a sealed
envelope that we don't know.

00:41:42.100 --> 00:41:45.940
And we would like to figure out, using
some sort of logical process, what's

00:41:45.940 --> 00:41:46.870
inside the envelope.

00:41:46.870 --> 00:41:49.840
Which person, which
room, and which weapon.

00:41:49.840 --> 00:41:54.340
And we do so by looking at some,
but not all, of these cards here.

00:41:54.340 --> 00:41:59.198
By looking at these cards to try and
figure out what might be going on.

00:41:59.198 --> 00:42:01.240
And so this is a very
popular game, but let's now

00:42:01.240 --> 00:42:04.120
try and formalize it and see
if we could train a computer

00:42:04.120 --> 00:42:08.410
to be able to play this game by
reasoning through it logically.

00:42:08.410 --> 00:42:10.540
So in order to do this
we'll begin by thinking

00:42:10.540 --> 00:42:13.780
about what propositional symbols
we're ultimately going to need.

00:42:13.780 --> 00:42:16.240
Remember again, that
propositional symbols are just

00:42:16.240 --> 00:42:21.950
some symbol, some variable, that can
be either true or false in the world.

00:42:21.950 --> 00:42:24.340
And so in this case, the
propositional symbols

00:42:24.340 --> 00:42:29.290
are really just going to correspond
to each of the possible things that

00:42:29.290 --> 00:42:30.730
could be inside the envelope.

00:42:30.730 --> 00:42:33.740
Mustard is a propositional
symbol, that in this case

00:42:33.740 --> 00:42:37.010
will just be true, if Colonel
Mustard is inside the envelope,

00:42:37.010 --> 00:42:38.200
if he is the murderer.

00:42:38.200 --> 00:42:39.460
And false otherwise.

00:42:39.460 --> 00:42:42.790
And likewise, for Plum for Professor
Plum, and Scarlet for Miss Scarlet,

00:42:42.790 --> 00:42:45.880
and likewise for each of the
rooms, and for each of the weapons.

00:42:45.880 --> 00:42:50.450
We have one propositional
symbol for each of these ideas.

00:42:50.450 --> 00:42:52.870
Then using those
propositional symbols we

00:42:52.870 --> 00:42:56.620
can begin to create logical
sentences, create knowledge

00:42:56.620 --> 00:42:58.640
that we know about the world.

00:42:58.640 --> 00:43:01.810
So for example, we know that
someone is the murderer.

00:43:01.810 --> 00:43:04.840
That one of the three people
is, in fact, the murderer.

00:43:04.840 --> 00:43:06.220
And how would we encode that?

00:43:06.220 --> 00:43:08.590
Well, we don't know for
sure who the murderer is,

00:43:08.590 --> 00:43:13.730
but we know it is one person, or the
second person, or the third person.

00:43:13.730 --> 00:43:18.040
So I could say something like
this: Mustard, or Plum, or Scarlet.

00:43:18.040 --> 00:43:21.573
And this piece of knowledge encodes
that one of these three people

00:43:21.573 --> 00:43:22.240
is the murderer.

00:43:22.240 --> 00:43:26.980
We don't know which, but one of
these three things must be true.

00:43:26.980 --> 00:43:28.700
What other information do we know?

00:43:28.700 --> 00:43:30.893
Well, we know that, for
example, one of the rooms

00:43:30.893 --> 00:43:32.560
must have been the room in the envelope.

00:43:32.560 --> 00:43:36.460
That the crime was committed either
in the ballroom, or the kitchen,

00:43:36.460 --> 00:43:37.363
or the library.

00:43:37.363 --> 00:43:39.280
Again, right now we don't
know which, but this

00:43:39.280 --> 00:43:42.640
is knowledge we know at the outset--
knowledge that one of these three

00:43:42.640 --> 00:43:44.417
must be inside the envelope.

00:43:44.417 --> 00:43:46.750
And likewise we can say the
same thing about the weapon.

00:43:46.750 --> 00:43:49.750
That it was either the knife,
or the revolver, or the wrench.

00:43:49.750 --> 00:43:52.780
That one of those weapons must
have been the weapon of choice,

00:43:52.780 --> 00:43:55.950
and therefore, the
weapon in the envelope.

00:43:55.950 --> 00:43:57.960
And then as the game
progresses, the game play

00:43:57.960 --> 00:44:00.120
works by people get
various different cards.

00:44:00.120 --> 00:44:03.200
And using those cards, you
can deduce information.

00:44:03.200 --> 00:44:05.380
That if someone gives
you a card, for example,

00:44:05.380 --> 00:44:08.490
I have the Professor
Plum card in my hand,

00:44:08.490 --> 00:44:12.240
then I know the Professor Plum
card can't be inside the envelope.

00:44:12.240 --> 00:44:15.570
I know that Professor
Plum is not the criminal.

00:44:15.570 --> 00:44:19.320
So I know a piece of information,
like not Plum, for example.

00:44:19.320 --> 00:44:22.710
I know that Professor
Plum has to be false.

00:44:22.710 --> 00:44:25.650
This propositional symbol is not true.

00:44:25.650 --> 00:44:29.040
And sometimes I might not know for
sure that a particular card is not

00:44:29.040 --> 00:44:29.672
in the middle.

00:44:29.672 --> 00:44:31.380
But sometimes, someone
will make a guess,

00:44:31.380 --> 00:44:34.510
and I'll know that one of three
possibilities is not true.

00:44:34.510 --> 00:44:37.890
Like someone will guess Colonel Mustard
in the library with the revolver,

00:44:37.890 --> 00:44:39.370
or something to that effect.

00:44:39.370 --> 00:44:42.360
And in that case, a card might
be revealed that I don't see.

00:44:42.360 --> 00:44:47.340
But if it is a card, and it is either
Colonel Mustard, or the revolver,

00:44:47.340 --> 00:44:51.002
or the library, then I know
that at least one of them

00:44:51.002 --> 00:44:51.960
can't be in the middle.

00:44:51.960 --> 00:44:57.600
So I know something like, it is either
not Mustard, or it is not the library,

00:44:57.600 --> 00:44:59.670
or it is not the revolver.

00:44:59.670 --> 00:45:03.000
Now maybe multiple of these are not
true, but I know that at least one

00:45:03.000 --> 00:45:08.330
of Mustard, library and revolver
must, in fact, be false.

00:45:08.330 --> 00:45:13.080
And so this now is a propositional logic
representation of this game of Clue.

00:45:13.080 --> 00:45:16.560
A way of encoding the knowledge
that we know inside this game using

00:45:16.560 --> 00:45:19.380
propositional logic that a
computer algorithm, something

00:45:19.380 --> 00:45:21.600
like model checking that
we saw a moment ago,

00:45:21.600 --> 00:45:24.280
can actually look at and understand.

00:45:24.280 --> 00:45:28.200
So let's now take a look at some code
to see how this algorithm might actually

00:45:28.200 --> 00:45:31.020
work in practice.

00:45:31.020 --> 00:45:31.520
All right.

00:45:31.520 --> 00:45:33.905
So I'm now going to open
up a file called clue.py,

00:45:33.905 --> 00:45:35.272
which I've started already.

00:45:35.272 --> 00:45:37.730
And what we'll see here is I've
defined a couple of things.

00:45:37.730 --> 00:45:39.680
I've defined some symbols initially.

00:45:39.680 --> 00:45:42.980
Notice I have a symbol for Colonel
Mustard, a symbol for Professor Plum,

00:45:42.980 --> 00:45:45.290
a symbol for Miss Scarlet,
all of which I put inside

00:45:45.290 --> 00:45:46.910
of this list of characters.

00:45:46.910 --> 00:45:48.710
I have a symbol for
ballroom, and kitchen,

00:45:48.710 --> 00:45:50.950
and library inside of a list of rooms.

00:45:50.950 --> 00:45:53.720
And then I have symbols for
knife, and revolver, and wrench.

00:45:53.720 --> 00:45:55.070
These are my weapons.

00:45:55.070 --> 00:45:58.070
And so all of these characters
and rooms and weapons altogether,

00:45:58.070 --> 00:46:00.140
those are my symbols.

00:46:00.140 --> 00:46:03.600
And now I also have this
check knowledge function.

00:46:03.600 --> 00:46:07.070
And what the check knowledge function
does is it takes my knowledge,

00:46:07.070 --> 00:46:11.600
and it's going to try and draw
conclusions about what I know.

00:46:11.600 --> 00:46:16.100
So for example, we'll loop over all of
the possible symbols and we'll check.

00:46:16.100 --> 00:46:17.750
Do I know that that symbol is true?

00:46:17.750 --> 00:46:20.750
And a symbol is going to be something
like Professor Plum, or the knife,

00:46:20.750 --> 00:46:21.780
or the library.

00:46:21.780 --> 00:46:23.820
And if I know that it
is true, in other words,

00:46:23.820 --> 00:46:26.660
I know that it must be
the card in the envelope,

00:46:26.660 --> 00:46:29.180
then I'm going to print
out, using a function called

00:46:29.180 --> 00:46:30.980
C print, which prints things in color.

00:46:30.980 --> 00:46:34.063
I'm going to print out the word yes,
and I'm going to print that in green,

00:46:34.063 --> 00:46:36.520
just to make it very clear to us.

00:46:36.520 --> 00:46:39.450
And if we're not sure
that the symbol is true,

00:46:39.450 --> 00:46:42.930
maybe I can check to see if I'm
sure that the symbol is not true.

00:46:42.930 --> 00:46:46.830
Like, if I know for sure that it
is not Professor Plum, for example.

00:46:46.830 --> 00:46:49.110
And I do that by running
model check again.

00:46:49.110 --> 00:46:52.690
This time checking if my
knowledge is not the symbol.

00:46:52.690 --> 00:46:56.460
If I know for sure that
the symbol is not true.

00:46:56.460 --> 00:46:59.430
And if I don't know for sure
that the symbol is not true,

00:46:59.430 --> 00:47:03.140
because I say elif not model
check, meaning I'm not sure

00:47:03.140 --> 00:47:04.980
that the symbol is
false, well, then I'll

00:47:04.980 --> 00:47:07.350
go ahead and print out
maybe next to the symbol.

00:47:07.350 --> 00:47:09.060
Because maybe the symbol is true.

00:47:09.060 --> 00:47:10.140
Maybe it's not.

00:47:10.140 --> 00:47:12.180
I don't actually know.

00:47:12.180 --> 00:47:14.550
So what knowledge do I actually have?

00:47:14.550 --> 00:47:16.650
Well, let's try and
represent my knowledge now.

00:47:16.650 --> 00:47:20.730
So my knowledge is, I know a couple
of things so I'll put them in an and.

00:47:20.730 --> 00:47:24.570
And I know that one of the three
people must be the criminal.

00:47:24.570 --> 00:47:28.117
So I know or Mustard, Plum, Scarlet.

00:47:28.117 --> 00:47:31.200
This is my way of encoding that it is
either Colonel Mustard, or Professor

00:47:31.200 --> 00:47:32.940
Plum, or Miss Scarlet.

00:47:32.940 --> 00:47:35.310
I know that it must have
happened in one of the rooms.

00:47:35.310 --> 00:47:40.320
So I know or ballroom,
kitchen, library, for example.

00:47:40.320 --> 00:47:43.080
And I know that one of the weapons
must have been used as well.

00:47:43.080 --> 00:47:47.610
So I know or knife, revolver, wrench.

00:47:47.610 --> 00:47:49.380
So that might be my initial knowledge.

00:47:49.380 --> 00:47:51.400
That I know that it must
have been one of the people.

00:47:51.400 --> 00:47:53.275
I know it must have been
in one of the rooms.

00:47:53.275 --> 00:47:55.993
And I know that it must have
been one of the weapons.

00:47:55.993 --> 00:47:58.410
And I can see what that knowledge
looks like as a formula,

00:47:58.410 --> 00:48:01.100
by printing out knowledge.formula.

00:48:01.100 --> 00:48:03.240
So I'll run Python clue.py.

00:48:03.240 --> 00:48:06.720
And here now is the information
that I know in logical format.

00:48:06.720 --> 00:48:10.080
I know that it is Colonel Mustard,
or Professor Plum, or Miss Scarlet.

00:48:10.080 --> 00:48:13.020
And I know that it is the ballroom,
the kitchen, or the library.

00:48:13.020 --> 00:48:16.020
And I know that it is the knife,
the revolver, or the wrench.

00:48:16.020 --> 00:48:18.160
But I don't know much more than that.

00:48:18.160 --> 00:48:20.520
I can't really draw
any firm conclusions.

00:48:20.520 --> 00:48:23.620
And in fact, we can see
that if I try and do--

00:48:23.620 --> 00:48:27.962
let me go ahead and run my knowledge
check function on my knowledge.

00:48:27.962 --> 00:48:29.670
Now let's check is
this function that I--

00:48:29.670 --> 00:48:32.170
or check knowledge rather.

00:48:32.170 --> 00:48:35.530
Is this function that I just wrote
that looks over all of the symbols

00:48:35.530 --> 00:48:40.480
and tries to see what conclusions I can
actually draw about any of the symbols.

00:48:40.480 --> 00:48:45.797
So I'll go ahead and run clue.py
and see what it is that I know.

00:48:45.797 --> 00:48:48.130
And it seems that I don't
really know anything for sure.

00:48:48.130 --> 00:48:49.960
I have all three people are maybes.

00:48:49.960 --> 00:48:51.520
All three of the rooms are maybes.

00:48:51.520 --> 00:48:53.140
All three of the weapons are maybes.

00:48:53.140 --> 00:48:56.410
I don't really know anything
for certain just yet.

00:48:56.410 --> 00:48:59.050
But now let me try and add
some additional information

00:48:59.050 --> 00:49:01.690
and see if additional
information, additional knowledge,

00:49:01.690 --> 00:49:04.818
can help us to logically reason
our way through this process.

00:49:04.818 --> 00:49:06.860
And we are just going to
provide the information.

00:49:06.860 --> 00:49:11.020
Our AI is going to take care of
doing the inference and figuring out

00:49:11.020 --> 00:49:13.390
what conclusions it's able to draw.

00:49:13.390 --> 00:49:17.030
So I start with some cards, and
those cards tell me something.

00:49:17.030 --> 00:49:19.900
So if I have the Colonel
Mustard card, for example,

00:49:19.900 --> 00:49:23.770
I know that the Mustard
symbol must be false.

00:49:23.770 --> 00:49:26.800
In other words, Mustard is
not the one in the envelope.

00:49:26.800 --> 00:49:27.970
It's not the criminal.

00:49:27.970 --> 00:49:31.150
So I can say, knowledge
supports something called--

00:49:31.150 --> 00:49:36.010
every and in this library supports .add,
which is a way of adding knowledge,

00:49:36.010 --> 00:49:39.890
or adding an additional logical
sentence to an and clause.

00:49:39.890 --> 00:49:44.590
So I can say,
knowledge.add, not Mustard.

00:49:44.590 --> 00:49:47.200
I happen to know, because
I have the Mustard card,

00:49:47.200 --> 00:49:49.240
that Colonel Mustard is not the suspect.

00:49:49.240 --> 00:49:51.160
And maybe I have a couple
of other cards, too.

00:49:51.160 --> 00:49:53.500
Maybe I also have a
card for the kitchen,

00:49:53.500 --> 00:49:55.060
so I know it's not the kitchen.

00:49:55.060 --> 00:49:58.752
And maybe I have another card that
says that it is not the revolver.

00:49:58.752 --> 00:49:59.710
So I have three cards--

00:49:59.710 --> 00:50:01.750
Colonel Mustard, the
kitchen, and the revolver.

00:50:01.750 --> 00:50:06.190
And I encode that into my AI this way,
by saying it's not Colonel Mustard,

00:50:06.190 --> 00:50:10.630
it's not the kitchen, and it's not the
revolver, and I know those to be true.

00:50:10.630 --> 00:50:14.080
So now when I rerun clue.py,
we'll see that I've been

00:50:14.080 --> 00:50:16.540
able to eliminate some possibilities.

00:50:16.540 --> 00:50:20.410
Before I wasn't sure if it was the
knife, or the revolver, or the wrench.

00:50:20.410 --> 00:50:23.080
Knife was maybe, revolver
was maybe, wrench was maybe.

00:50:23.080 --> 00:50:25.492
Now I'm down to just the
knife and the wrench.

00:50:25.492 --> 00:50:28.450
Between those two, I don't know which
one it is-- they're both maybes--

00:50:28.450 --> 00:50:31.660
but I've been able to eliminate
the revolver, which is one

00:50:31.660 --> 00:50:36.160
that I know to be false because
I have the revolver card.

00:50:36.160 --> 00:50:40.390
And so additional information might be
acquired over the course of this game,

00:50:40.390 --> 00:50:43.120
and we would represent that
just by adding knowledge

00:50:43.120 --> 00:50:47.620
to our knowledge set, or knowledge
base that we've been building here.

00:50:47.620 --> 00:50:50.347
So if, for example, we
additionally got the information

00:50:50.347 --> 00:50:51.430
that someone made a guess.

00:50:51.430 --> 00:50:55.300
Someone guessed, like, Miss Scarlet
in the library with the wrench.

00:50:55.300 --> 00:50:59.380
And we know that that card was revealed,
which means that one of those three

00:50:59.380 --> 00:51:02.620
cards-- either Miss Scarlet,
or the library, or the wrench--

00:51:02.620 --> 00:51:06.800
one of those at minimum, must
not be inside of the envelope.

00:51:06.800 --> 00:51:08.070
So I could add some knowledge.

00:51:08.070 --> 00:51:12.165
Say knowledge.add, and I'm going
to add an or clause, because I

00:51:12.165 --> 00:51:13.790
don't know for sure which one it's not.

00:51:13.790 --> 00:51:16.390
But I know one of them
is not in the envelope.

00:51:16.390 --> 00:51:19.762
So it's either not Scarlet
or it's not the library.

00:51:19.762 --> 00:51:21.220
And or supports multiple arguments.

00:51:21.220 --> 00:51:25.010
I can say it's also or not the wrench.

00:51:25.010 --> 00:51:26.380
So at least one of those--

00:51:26.380 --> 00:51:29.395
Scarlet, library, and wrench-- at
least one of those needs to be false.

00:51:29.395 --> 00:51:30.520
I don't know which, though.

00:51:30.520 --> 00:51:34.930
Maybe it's multiple, maybe it's
just one, but at least one I know

00:51:34.930 --> 00:51:36.640
needs to hold.

00:51:36.640 --> 00:51:39.430
And so now if I rerun
clue.py, I don't actually

00:51:39.430 --> 00:51:41.860
have any additional
information just yet.

00:51:41.860 --> 00:51:43.180
Nothing I can say conclusively.

00:51:43.180 --> 00:51:46.240
I still know that maybe it's Professor
Plum, maybe it's Miss Scarlet.

00:51:46.240 --> 00:51:48.705
I haven't eliminated any options.

00:51:48.705 --> 00:51:50.830
But let's imagine that I
get some more information.

00:51:50.830 --> 00:51:54.650
That someone shows me the
Professor Plum card, for example.

00:51:54.650 --> 00:51:55.600
So I say, all right.

00:51:55.600 --> 00:51:56.740
Let's go back here.

00:51:56.740 --> 00:52:01.323
Knowledge.add, not Plum.

00:52:01.323 --> 00:52:02.740
So I have the Professor Plum card.

00:52:02.740 --> 00:52:04.900
I know that Professor
Plum is not in the middle.

00:52:04.900 --> 00:52:09.350
I rerun clue.py, and right now,
I'm able to draw some conclusions.

00:52:09.350 --> 00:52:11.440
Now I've been able to
eliminate Professor Plum.

00:52:11.440 --> 00:52:14.650
And the only person that could
remaining be is Miss Scarlet.

00:52:14.650 --> 00:52:18.610
So I know, yes, Miss Scarlet,
this variable must be true.

00:52:18.610 --> 00:52:21.910
And I've been able to infer that based
on the information I already had.

00:52:21.910 --> 00:52:24.910
Now, between the ballroom and the
library, and the knife and the wrench,

00:52:24.910 --> 00:52:26.860
for those two, I'm still not sure.

00:52:26.860 --> 00:52:29.470
So let's add one more
piece of information.

00:52:29.470 --> 00:52:32.230
Let's say that I know that
it's not the ballroom.

00:52:32.230 --> 00:52:35.230
Someone has shown me the ballroom
card, so I know it's not the ballroom.

00:52:35.230 --> 00:52:38.480
Which means at this point, I should be
able to conclude that it's the library.

00:52:38.480 --> 00:52:39.310
Let's see.

00:52:39.310 --> 00:52:44.240
I'll say knowledge.add,
not the ballroom.

00:52:44.240 --> 00:52:47.202
And we'll go ahead and run that.

00:52:47.202 --> 00:52:49.410
And it turns out that after
all of this, not only can

00:52:49.410 --> 00:52:51.900
I conclude that I know
that it's the library.

00:52:51.900 --> 00:52:53.825
But I also know that the
weapon was the knife.

00:52:53.825 --> 00:52:56.700
And that might have been an inference
that was a little bit trickier.

00:52:56.700 --> 00:52:58.710
Something I wouldn't have
realized immediately.

00:52:58.710 --> 00:53:01.247
But the AI, via this
model checking algorithm,

00:53:01.247 --> 00:53:02.580
is able to draw that conclusion.

00:53:02.580 --> 00:53:04.410
That we know for sure
that it must be Miss

00:53:04.410 --> 00:53:06.690
Scarlet in the library with the knife.

00:53:06.690 --> 00:53:08.200
And how do we know that?

00:53:08.200 --> 00:53:11.760
Well, we know it from
this or clause up here.

00:53:11.760 --> 00:53:15.810
That we know that it's either not
Scarlet, or it's not the library,

00:53:15.810 --> 00:53:17.730
or it's not the wrench.

00:53:17.730 --> 00:53:20.310
And given that we know
that it is Miss Scarlet,

00:53:20.310 --> 00:53:23.280
and we know that it is the
library, then the only remaining

00:53:23.280 --> 00:53:26.520
option for the weapon is that
it is not the wrench, which

00:53:26.520 --> 00:53:28.620
means that it must be the knife.

00:53:28.620 --> 00:53:31.050
So we, as humans, now can go
back and reason through that,

00:53:31.050 --> 00:53:33.258
even though it might not
have been immediately clear.

00:53:33.258 --> 00:53:37.112
And that's one of the advantages of
using an AI or some sort of algorithm

00:53:37.112 --> 00:53:38.820
in order to do this,
is that the computer

00:53:38.820 --> 00:53:42.000
can exhaust all of these
possibilities and try and figure out

00:53:42.000 --> 00:53:45.010
what the solution actually should be.

00:53:45.010 --> 00:53:47.550
And so for that reason,
it's often helpful to be

00:53:47.550 --> 00:53:49.380
able to represent knowledge in this way.

00:53:49.380 --> 00:53:51.570
Knowledge engineering,
some situation, where

00:53:51.570 --> 00:53:54.870
we can use a computer to be able
to represent knowledge and draw

00:53:54.870 --> 00:53:57.060
conclusions based on that knowledge.

00:53:57.060 --> 00:54:00.390
And anytime we can translate
something into propositional logic

00:54:00.390 --> 00:54:03.690
symbols like this, type
of approach can be useful.

00:54:03.690 --> 00:54:05.820
So you might be familiar
with logic puzzles, where

00:54:05.820 --> 00:54:08.612
you have to puzzle your way through
trying to figure something out.

00:54:08.612 --> 00:54:10.830
This is what a classic logic
puzzle might look like.

00:54:10.830 --> 00:54:13.950
Something like Gildaroy,
Minerva, Pomona, and Horace each

00:54:13.950 --> 00:54:16.740
belong to a different
one of the four houses--

00:54:16.740 --> 00:54:19.410
Gryffindor, Hufflepuff,
Ravenclaw, and Slytherin.

00:54:19.410 --> 00:54:21.750
And then we have some
information, that Gildaroy

00:54:21.750 --> 00:54:23.970
belongs to Gryffindor or Ravenclaw.

00:54:23.970 --> 00:54:26.190
Pomona does not belong in Slytherin.

00:54:26.190 --> 00:54:28.740
And Minerva does belong to Gryffindor.

00:54:28.740 --> 00:54:30.510
We have a couple of
pieces of information.

00:54:30.510 --> 00:54:32.520
And using that
information, we need to be

00:54:32.520 --> 00:54:35.340
able to draw some conclusions
about which person

00:54:35.340 --> 00:54:37.590
should be assigned to which house.

00:54:37.590 --> 00:54:41.910
And again, we can use the exact same
idea to try and implement this notion.

00:54:41.910 --> 00:54:44.018
So we need some propositional symbols.

00:54:44.018 --> 00:54:45.810
And in this case, the
propositional symbols

00:54:45.810 --> 00:54:48.120
are going to get a little
more complex, although, we'll

00:54:48.120 --> 00:54:50.820
see ways to make this a
little bit cleaner later on.

00:54:50.820 --> 00:54:53.670
But we'll need 16 propositional symbols.

00:54:53.670 --> 00:54:56.280
One for each person and house.

00:54:56.280 --> 00:54:58.890
So we need to say-- remember,
every propositional symbol

00:54:58.890 --> 00:55:00.910
is either true or false.

00:55:00.910 --> 00:55:03.600
So Gildaroy Gryffindor
is either true or false.

00:55:03.600 --> 00:55:05.820
Either he's in Gryffindor or he is not.

00:55:05.820 --> 00:55:08.070
Likewise, Gildaroy Hufflepuff
also true or false.

00:55:08.070 --> 00:55:10.230
Either it is true or it's false.

00:55:10.230 --> 00:55:14.055
And that's true for every
combination of person and house

00:55:14.055 --> 00:55:15.180
that we could come up with.

00:55:15.180 --> 00:55:19.200
We have some sort of propositional
symbol for each one of those.

00:55:19.200 --> 00:55:21.510
Using this type of
knowledge, we can then

00:55:21.510 --> 00:55:24.870
begin to think about what
types of logical sentences

00:55:24.870 --> 00:55:26.730
we can say about the puzzle.

00:55:26.730 --> 00:55:28.020
That if we know--

00:55:28.020 --> 00:55:30.363
before even think about the
information we were given,

00:55:30.363 --> 00:55:32.280
we can think about the
premise of the problem.

00:55:32.280 --> 00:55:35.850
That every person is assigned
to a different house.

00:55:35.850 --> 00:55:37.150
So what does that tell us?

00:55:37.150 --> 00:55:38.760
Well, it tells us sentences like this.

00:55:38.760 --> 00:55:44.190
It tells us, like, Pomona Slytherin
implies not Pomona Hufflepuff.

00:55:44.190 --> 00:55:46.530
Something like if
Pomona is in Slytherin,

00:55:46.530 --> 00:55:48.990
then we know that Pomona
is not in Hufflepuff.

00:55:48.990 --> 00:55:52.800
And we know this for all four people
and for all combinations of houses.

00:55:52.800 --> 00:55:55.620
That no matter what you person
you pick, if they're in one house,

00:55:55.620 --> 00:55:57.900
then they're not in some other house.

00:55:57.900 --> 00:56:00.390
So I'll probably have a whole
bunch of knowledge statements

00:56:00.390 --> 00:56:01.560
that are of this four.

00:56:01.560 --> 00:56:03.480
That if we know Pomona's
in Slytherin, then

00:56:03.480 --> 00:56:06.060
we know Pomona is not in Hufflepuff.

00:56:06.060 --> 00:56:10.110
We were also given the information that
each person is in a different house.

00:56:10.110 --> 00:56:12.840
So I also have pieces of knowledge
that look something like this.

00:56:12.840 --> 00:56:17.490
Minerva Ravenclaw implies
not Gildaroy Ravenclaw.

00:56:17.490 --> 00:56:20.880
If they're all in different houses,
then if Minerva is in Ravenclaw,

00:56:20.880 --> 00:56:24.330
then we know that Gildaroy
is not in Ravenclaw as well.

00:56:24.330 --> 00:56:26.310
And I have a whole bunch
of similar sentences

00:56:26.310 --> 00:56:30.600
like this that are expressing that
idea for other people and other houses

00:56:30.600 --> 00:56:31.475
as well.

00:56:31.475 --> 00:56:34.150
And so in addition to
sentences of these form,

00:56:34.150 --> 00:56:36.420
I also have the knowledge
that was given to me.

00:56:36.420 --> 00:56:40.200
Information like, Gildaroy was
in Gryffindor or in Ravenclaw

00:56:40.200 --> 00:56:41.730
that would be represented like this.

00:56:41.730 --> 00:56:44.970
Gildaroy Gryffindor
or Gildaroy Ravenclaw.

00:56:44.970 --> 00:56:47.310
And then using these
sorts of sentences, I

00:56:47.310 --> 00:56:51.077
can begin to draw some
conclusions about the world.

00:56:51.077 --> 00:56:52.410
So let's see an example of this.

00:56:52.410 --> 00:56:55.110
We'll go ahead and actually try
and implement this logic puzzle

00:56:55.110 --> 00:56:57.660
to see if we can figure
out what the answer is.

00:56:57.660 --> 00:57:00.960
I'll go ahead and open up
puzzle.py where I've already

00:57:00.960 --> 00:57:03.150
started to implement this sort of idea.

00:57:03.150 --> 00:57:06.180
I've defined a list of
people and a list of houses.

00:57:06.180 --> 00:57:11.057
And I've, so far, created one symbol
for every person and for every house.

00:57:11.057 --> 00:57:13.890
That's what this double for loop
is doing-- looping over all people,

00:57:13.890 --> 00:57:17.850
looping over all houses, creating
a new symbol for each of them.

00:57:17.850 --> 00:57:20.620
And then I've added some information.

00:57:20.620 --> 00:57:23.640
I know that every person
belongs to a house,

00:57:23.640 --> 00:57:26.880
so I've added the information
for every person--

00:57:26.880 --> 00:57:29.970
that person Gryffindor,
or person Hufflepuff,

00:57:29.970 --> 00:57:32.580
or person Ravenclaw,
or person Slytherin.

00:57:32.580 --> 00:57:35.130
That one of those four
things must be true.

00:57:35.130 --> 00:57:37.530
Every person belongs to a house.

00:57:37.530 --> 00:57:39.180
What other information do I know?

00:57:39.180 --> 00:57:42.390
I also know that only
one house per person.

00:57:42.390 --> 00:57:45.990
So no person belongs to multiple houses.

00:57:45.990 --> 00:57:47.113
So how does this work?

00:57:47.113 --> 00:57:49.030
Well, this is going to
be true for all people.

00:57:49.030 --> 00:57:51.390
So I'll loop over every person.

00:57:51.390 --> 00:57:55.380
And then I need to loop over
all different pairs of houses.

00:57:55.380 --> 00:57:59.130
The idea is I want to encode the idea
that if Minerva is in Gryffindor,

00:57:59.130 --> 00:58:01.770
then Minerva can't be in Ravenclaw.

00:58:01.770 --> 00:58:04.050
So I'll loop over all houses, h1.

00:58:04.050 --> 00:58:06.870
And I'll loop over all houses again, h2.

00:58:06.870 --> 00:58:10.500
And as long as they're
different, h1 not equal to H2,

00:58:10.500 --> 00:58:13.500
then I'll add to my knowledge
base this piece of information.

00:58:13.500 --> 00:58:18.600
That implication, in other words,
an if/then, if the person is in h1,

00:58:18.600 --> 00:58:22.860
then I know that they
are not in house h2.

00:58:22.860 --> 00:58:25.170
So these lines here
are encoding the notion

00:58:25.170 --> 00:58:28.050
that for every person, if
they belong to house one, then

00:58:28.050 --> 00:58:30.273
they are not in house two.

00:58:30.273 --> 00:58:32.190
And the other piece of
logic we need to encode

00:58:32.190 --> 00:58:35.290
is the idea that every house
can only have one person.

00:58:35.290 --> 00:58:38.370
In other words, if Pomona is
Hufflepuff, then nobody else

00:58:38.370 --> 00:58:40.260
is allowed to be in Hufflepuff either.

00:58:40.260 --> 00:58:42.260
And that's the same logic
but sort of backwards.

00:58:42.260 --> 00:58:47.040
I loop over all of the houses, and loop
over all different pairs of people.

00:58:47.040 --> 00:58:49.890
So I loop over people once,
loop over people again.

00:58:49.890 --> 00:58:54.390
And only do this when the people
are different, p1 not equal to p2.

00:58:54.390 --> 00:58:59.250
And I add the knowledge that
if, as given by the implication,

00:58:59.250 --> 00:59:02.640
if person one belongs
to the house, then it

00:59:02.640 --> 00:59:08.247
is not the case that person
two belongs to the same house.

00:59:08.247 --> 00:59:10.080
So here I'm just encoding
the knowledge that

00:59:10.080 --> 00:59:12.150
represents the problems constraints.

00:59:12.150 --> 00:59:14.040
I know that everyone's
in a different house.

00:59:14.040 --> 00:59:17.070
I know that any person can
only belong to one house.

00:59:17.070 --> 00:59:21.750
And I can now take my knowledge and
try and print out the information

00:59:21.750 --> 00:59:22.890
that I happen to know.

00:59:22.890 --> 00:59:26.400
So I'll go ahead and print
out knowledge.formula,

00:59:26.400 --> 00:59:27.525
just to see this in action.

00:59:27.525 --> 00:59:29.608
And I'll go ahead and skip
this for now, but we'll

00:59:29.608 --> 00:59:31.240
come back to this in a second.

00:59:31.240 --> 00:59:36.150
Let's print out the knowledge that
I know by running Python puzzle.py.

00:59:36.150 --> 00:59:38.070
It's a lot of information,
a lot that I have

00:59:38.070 --> 00:59:41.320
to scroll through, because there's
16 different variables all going on.

00:59:41.320 --> 00:59:43.620
But the basic idea if we
scroll up to the very top

00:59:43.620 --> 00:59:45.330
is I see my initial information.

00:59:45.330 --> 00:59:48.870
Gildaroy is either in Gryffindor,
or Gildaroy is and Hufflepuff,

00:59:48.870 --> 00:59:52.820
or Gildaroy is and Ravenclaw,
or Gildaroy is in Slytherin.

00:59:52.820 --> 00:59:55.210
And then way more information as well.

00:59:55.210 --> 00:59:56.280
So this is quite messy.

00:59:56.280 --> 00:59:58.037
More than we really
want to be looking at.

00:59:58.037 --> 01:00:00.870
And soon, too, we'll see ways of
representing this a little bit more

01:00:00.870 --> 01:00:02.460
nicely using logic.

01:00:02.460 --> 01:00:05.820
But for now, we can just say these are
the variables that we're dealing with.

01:00:05.820 --> 01:00:09.830
And now we'd like to
add some information.

01:00:09.830 --> 01:00:13.840
So the information we're going to
add is Gildaroy is in Gryffindor

01:00:13.840 --> 01:00:14.950
or he is in Ravenclaw.

01:00:14.950 --> 01:00:16.970
So that knowledge was given to us.

01:00:16.970 --> 01:00:20.020
So I'll go ahead and
say knowledge.add, and I

01:00:20.020 --> 01:00:30.680
know that either or Gildaroy
Gryffindor or Gildaroy Ravenclaw.

01:00:30.680 --> 01:00:33.660
One of those two things must be true.

01:00:33.660 --> 01:00:36.460
I also know that Pomona
was not in Slytherin.

01:00:36.460 --> 01:00:39.800
So I can say knowledge.add,
not this symbol.

01:00:39.800 --> 01:00:43.010
Not the Pomona Slytherin symbol.

01:00:43.010 --> 01:00:46.970
And then I can add the knowledge that
Minerva is in Gryffindor by adding

01:00:46.970 --> 01:00:51.060
the symbol Minerva Gryffindor.

01:00:51.060 --> 01:00:53.490
So those are the pieces
of knowledge that I know.

01:00:53.490 --> 01:00:57.210
And this loop here at the bottom
just loops over all of my symbols,

01:00:57.210 --> 01:01:01.410
checks to see if the knowledge entails
that symbol by calling this model check

01:01:01.410 --> 01:01:02.840
function again.

01:01:02.840 --> 01:01:07.790
And if it does, if we know the symbol
is true, we print out the symbol.

01:01:07.790 --> 01:01:11.300
So now I can run Python
puzzle.py, and Python

01:01:11.300 --> 01:01:13.190
is going to solve this puzzle for me.

01:01:13.190 --> 01:01:15.800
We're able to conclude that
Gildaroy belongs to Ravenclaw,

01:01:15.800 --> 01:01:18.320
Pomona belongs to Hufflepuff,
Minerva to Gryffindor,

01:01:18.320 --> 01:01:22.430
and Horace to Slytherin just by encoding
this knowledge inside the computer--

01:01:22.430 --> 01:01:24.680
although, it was quite
tedious to do in this case--

01:01:24.680 --> 01:01:29.280
and as a result, we were able to get
the conclusion from that as well.

01:01:29.280 --> 01:01:32.660
And you can imagine this being applied
to many sorts of different deductive

01:01:32.660 --> 01:01:33.320
situations.

01:01:33.320 --> 01:01:35.450
So not only these situations
where we're trying

01:01:35.450 --> 01:01:38.052
to deal with Harry Potter
characters in this puzzle.

01:01:38.052 --> 01:01:40.010
But if you've ever played
games like Mastermind

01:01:40.010 --> 01:01:43.340
where you're trying to figure out
which order different colors go in

01:01:43.340 --> 01:01:46.700
and trying to make predictions about
it, I could tell you, for example.

01:01:46.700 --> 01:01:49.610
Let's play a simplified version
of Mastermind where there are four

01:01:49.610 --> 01:01:52.070
colors-- red, blue, green, and yellow--

01:01:52.070 --> 01:01:55.350
and they're in some order, but
I'm not telling you what order.

01:01:55.350 --> 01:01:57.350
You just have to make a
guess, and I'll tell you

01:01:57.350 --> 01:01:59.690
of red, blue, green, and
yellow, how many of the four

01:01:59.690 --> 01:02:01.520
you got in the right position.

01:02:01.520 --> 01:02:03.620
So a simplified version of this game.

01:02:03.620 --> 01:02:06.210
You might make a guess, like
red, blue, green, yellow.

01:02:06.210 --> 01:02:09.650
And I would tell you something
like, two of those four

01:02:09.650 --> 01:02:12.447
are in the correct position,
but the other two are not.

01:02:12.447 --> 01:02:15.530
Then you could reasonably make a guess
and say, all right, let's try this.

01:02:15.530 --> 01:02:17.270
Blue, red, green, yellow.

01:02:17.270 --> 01:02:19.100
Try switching two of them around.

01:02:19.100 --> 01:02:22.190
And this time maybe I tell you,
you know what, none of those

01:02:22.190 --> 01:02:23.780
are in the correct position.

01:02:23.780 --> 01:02:26.090
And the question then
is, all right, what is

01:02:26.090 --> 01:02:28.280
the correct order of these four colors?

01:02:28.280 --> 01:02:30.530
And we, as humans, could
begin to reason this through.

01:02:30.530 --> 01:02:34.820
All right, well, if none of these were
correct, but two of these were correct,

01:02:34.820 --> 01:02:37.730
well, it must have been because
I switched the red and the blue.

01:02:37.730 --> 01:02:39.990
Which means red and blue
here must be correct.

01:02:39.990 --> 01:02:42.240
Which means green and yellow
are probably not correct.

01:02:42.240 --> 01:02:44.760
You can begin to do this
sort of deductive reasoning.

01:02:44.760 --> 01:02:48.230
We can also equivalently try and
take this and encode it inside

01:02:48.230 --> 01:02:49.700
of our computer as well.

01:02:49.700 --> 01:02:52.310
And it's going to be very
similar to the logic puzzle

01:02:52.310 --> 01:02:53.678
that we just did a moment ago.

01:02:53.678 --> 01:02:56.720
So I won't spend too much time on this
code because it is fairly similar.

01:02:56.720 --> 01:02:59.210
But again, we have a
whole bunch of colors,

01:02:59.210 --> 01:03:02.880
and four different positions
in which those colors can be.

01:03:02.880 --> 01:03:04.730
And then we have some
additional knowledge.

01:03:04.730 --> 01:03:06.410
And I encode all of that knowledge.

01:03:06.410 --> 01:03:09.360
And you can take a look at
this code on your own time.

01:03:09.360 --> 01:03:12.080
But I just want to demonstrate
that when we run this code,

01:03:12.080 --> 01:03:17.100
run Python mastermind.py
and run and see what we get,

01:03:17.100 --> 01:03:21.170
we ultimately are able to
compute red in the zero position,

01:03:21.170 --> 01:03:23.750
blue in the one position,
yellow in the two position,

01:03:23.750 --> 01:03:28.307
and green in the three position
as the ordering of those symbols.

01:03:28.307 --> 01:03:30.140
Now, ultimately, what
you might have noticed

01:03:30.140 --> 01:03:32.870
is this process was
taking quite a long time.

01:03:32.870 --> 01:03:36.650
And, in fact, model checking is not
a particularly efficient algorithm.

01:03:36.650 --> 01:03:38.630
What I need to do in
order to model check

01:03:38.630 --> 01:03:41.070
is take all of my possible
different variables

01:03:41.070 --> 01:03:43.790
and enumerate all of the
possibilities that they could be in.

01:03:43.790 --> 01:03:48.320
If I have n variables, I have
2 to the n possible worlds

01:03:48.320 --> 01:03:51.740
that I need to be looking through in
order to perform this model checking

01:03:51.740 --> 01:03:52.370
algorithm.

01:03:52.370 --> 01:03:54.740
And this is probably not
tractable, especially

01:03:54.740 --> 01:03:57.770
as we start to get to much
larger and larger sets of data

01:03:57.770 --> 01:04:00.620
where you have many, many more
variables that are at play.

01:04:00.620 --> 01:04:03.440
Right here we only have a relatively
small number of variables,

01:04:03.440 --> 01:04:05.840
so this sort of approach
can actually work.

01:04:05.840 --> 01:04:08.120
But as the number of
variables increases,

01:04:08.120 --> 01:04:11.540
model checking becomes less and
less good of a way of trying

01:04:11.540 --> 01:04:14.050
to solve these sorts of problems.

01:04:14.050 --> 01:04:16.550
So while it might have been OK
for something like Mastermind

01:04:16.550 --> 01:04:18.842
to conclude that this is,
indeed, the correct sequence,

01:04:18.842 --> 01:04:22.010
where all four are in the correct
position, what we'd like to do

01:04:22.010 --> 01:04:25.910
is come up with some better ways to
be able to make inferences, rather

01:04:25.910 --> 01:04:28.910
than just enumerate all
of the possibilities.

01:04:28.910 --> 01:04:33.290
And to do so, what we'll transition to
next is the idea of inference rules.

01:04:33.290 --> 01:04:37.490
Some sort of rules that we can apply
to take knowledge that already exists

01:04:37.490 --> 01:04:40.310
and translate it into
new forms of knowledge.

01:04:40.310 --> 01:04:42.710
And the general way we'll
structure inference rule

01:04:42.710 --> 01:04:45.140
is by having a horizontal line here.

01:04:45.140 --> 01:04:48.560
Anything above the line is going
to represent a premise, something

01:04:48.560 --> 01:04:50.260
that we know to be true.

01:04:50.260 --> 01:04:52.970
And then anything below the
line will be the conclusion

01:04:52.970 --> 01:04:56.552
that we can arrive at
after we apply the logic,

01:04:56.552 --> 01:04:59.010
or from the inference rule that
we're going to demonstrate.

01:04:59.010 --> 01:05:00.440
So we'll do some of
these inference rules

01:05:00.440 --> 01:05:03.320
by demonstrating them in English
first, but then translating them

01:05:03.320 --> 01:05:05.420
into the world of
propositional logic so you

01:05:05.420 --> 01:05:09.120
can see what those inference
rules actually look like.

01:05:09.120 --> 01:05:11.300
So for example, let's
imagine that I have access

01:05:11.300 --> 01:05:13.040
to two pieces of information.

01:05:13.040 --> 01:05:15.720
I know, for example,
that if it is raining,

01:05:15.720 --> 01:05:18.340
then Harry is inside, for example.

01:05:18.340 --> 01:05:21.167
And let's say I also know it is raining.

01:05:21.167 --> 01:05:23.750
Then most of us could reasonably
then look at this information

01:05:23.750 --> 01:05:28.180
and conclude that, all
right, Harry must be inside.

01:05:28.180 --> 01:05:31.450
This inference rule is
known as modus ponens,

01:05:31.450 --> 01:05:34.210
and it's phrased more
formally in logic as this.

01:05:34.210 --> 01:05:38.620
If we know that alpha implies
beta, in other words, if alpha,

01:05:38.620 --> 01:05:42.410
then beta, and we also
know that alpha is true,

01:05:42.410 --> 01:05:45.950
then we should be able to
conclude that beta is also true.

01:05:45.950 --> 01:05:49.960
We can apply this inference rule to
take these two pieces of information

01:05:49.960 --> 01:05:52.250
and generate this new
piece of information.

01:05:52.250 --> 01:05:55.390
Notice that this is a totally different
approach from the model checking

01:05:55.390 --> 01:05:58.810
approach, where the approach was
look at all of the possible worlds

01:05:58.810 --> 01:06:01.000
and see what's true in
each of these worlds.

01:06:01.000 --> 01:06:03.520
Here, we're not dealing
with any specific world.

01:06:03.520 --> 01:06:05.830
We're just dealing with
the knowledge that we know

01:06:05.830 --> 01:06:08.770
and what conclusions we can
arrive at based on that knowledge.

01:06:08.770 --> 01:06:14.320
That I know that A implies B, and
I know A, and the conclusion is B.

01:06:14.320 --> 01:06:16.950
And this should seem like
a relatively obvious rule.

01:06:16.950 --> 01:06:20.410
But of course, if alpha than
beta, and we know alpha,

01:06:20.410 --> 01:06:23.570
then we should be able to
conclude that beta is also true.

01:06:23.570 --> 01:06:26.867
And that's going to be true for many,
maybe even all of the inference rules

01:06:26.867 --> 01:06:27.950
that we'll take a look at.

01:06:27.950 --> 01:06:29.992
You should be able to look
at them and say, yeah,

01:06:29.992 --> 01:06:31.448
of course that's going to be true.

01:06:31.448 --> 01:06:33.490
But it's putting these
all together, figuring out

01:06:33.490 --> 01:06:35.650
the right combination
of inference rules that

01:06:35.650 --> 01:06:39.970
can be applied that ultimately
is going to allow us to generate

01:06:39.970 --> 01:06:42.730
interesting knowledge inside of our AI.

01:06:42.730 --> 01:06:45.700
So that's modus ponens, this
application of implication.

01:06:45.700 --> 01:06:48.910
That if we know alpha, and we
know that alpha implies beta,

01:06:48.910 --> 01:06:51.508
then we can conclude beta.

01:06:51.508 --> 01:06:53.050
Let's take a look at another example.

01:06:53.050 --> 01:06:54.008
Fairly straightforward.

01:06:54.008 --> 01:06:56.860
Something like Harry is
friends with Ron and Hermione.

01:06:56.860 --> 01:06:59.110
Based on that information,
we can reasonably

01:06:59.110 --> 01:07:01.210
conclude Harry is friends with Hermione.

01:07:01.210 --> 01:07:03.070
That must also be true.

01:07:03.070 --> 01:07:06.190
And this inference rule is
known as and elimination.

01:07:06.190 --> 01:07:10.060
And what and elimination says, is
that if we have a situation where

01:07:10.060 --> 01:07:13.240
alpha and beta are both true--

01:07:13.240 --> 01:07:15.840
I have information alpha and beta--

01:07:15.840 --> 01:07:18.730
well, then just alpha is true.

01:07:18.730 --> 01:07:20.850
Or likewise, just beta is true.

01:07:20.850 --> 01:07:24.100
That if I know that both parts
are true, then one of those parts

01:07:24.100 --> 01:07:25.330
must also be true.

01:07:25.330 --> 01:07:28.660
Again, something obvious from the
point of view of human intuition.

01:07:28.660 --> 01:07:31.480
But a computer needs to be
told this kind of information.

01:07:31.480 --> 01:07:33.280
To be able to apply
the inference rule, we

01:07:33.280 --> 01:07:35.988
need to tell the computer that
this is an inference rule that you

01:07:35.988 --> 01:07:38.320
can apply so the computer
has access to it,

01:07:38.320 --> 01:07:41.350
and is able to use it in
order to translate information

01:07:41.350 --> 01:07:44.165
from one form to another.

01:07:44.165 --> 01:07:46.540
In addition to that, let's
take a look at another example

01:07:46.540 --> 01:07:47.800
of an inference rule.

01:07:47.800 --> 01:07:53.055
Something like, it is not true
that Harry did not pass the test.

01:07:53.055 --> 01:07:55.180
Bit of a tricky sentence
to parse so read it again.

01:07:55.180 --> 01:07:59.320
It is not true, or it is false,
that Harry did not pass the test.

01:07:59.320 --> 01:08:03.130
Well, if it is false that
Harry did not pass the test,

01:08:03.130 --> 01:08:07.270
then the only reasonable conclusion
is that Harry did pass the test.

01:08:07.270 --> 01:08:09.460
And so this, instead of
being and elimination,

01:08:09.460 --> 01:08:11.920
is what we call double
negation elimination.

01:08:11.920 --> 01:08:14.860
That if we have two negatives
inside of our premise, then

01:08:14.860 --> 01:08:16.345
we can just remove them altogether.

01:08:16.345 --> 01:08:17.470
They cancel each other out.

01:08:17.470 --> 01:08:21.760
One turns true to false, and the
other one turns false back into true.

01:08:21.760 --> 01:08:23.649
Phrased a little bit
more formally, we say

01:08:23.649 --> 01:08:29.050
that if the premise is not not alpha,
then the conclusion we can draw

01:08:29.050 --> 01:08:30.130
is just alpha.

01:08:30.130 --> 01:08:32.767
We can say that alpha is true.

01:08:32.767 --> 01:08:34.600
We'll take a look at a
couple more of these.

01:08:34.600 --> 01:08:40.240
If I have it is raining, then Harry
is inside, how do I reframe this?

01:08:40.240 --> 01:08:42.100
Well, this one is a little bit trickier.

01:08:42.100 --> 01:08:45.399
But if I know if it is
raining, then Harry is inside,

01:08:45.399 --> 01:08:48.160
then I conclude one of
two things must be true.

01:08:48.160 --> 01:08:52.404
Either it is not raining,
or Harry is inside.

01:08:52.404 --> 01:08:55.029
Now, this one's trickier, so
let's think about it a little bit.

01:08:55.029 --> 01:08:58.710
This first premise here, if it
is raining, then Harry is inside,

01:08:58.710 --> 01:09:03.520
is saying that if I know that it is
raining, then Harry must be inside.

01:09:03.520 --> 01:09:06.160
So what is the other possible case?

01:09:06.160 --> 01:09:11.109
Well, if Harry is not inside, then
I know that it must not be raining.

01:09:11.109 --> 01:09:13.880
So one of those two
situations must be true.

01:09:13.880 --> 01:09:19.220
Either it's not raining, or it is
raining, in which case Harry is inside.

01:09:19.220 --> 01:09:24.100
So the conclusion I can draw is either
it is not raining, or it is raining,

01:09:24.100 --> 01:09:27.350
so therefore, Harry is inside.

01:09:27.350 --> 01:09:32.350
So this is a way to translate if/then
statements into or statements.

01:09:32.350 --> 01:09:35.220
And this is known as
implication elimination.

01:09:35.220 --> 01:09:37.720
And this is similar to what we
actually did in the beginning

01:09:37.720 --> 01:09:41.560
when we were first looking at those very
first sentences about Harry and Hagrid

01:09:41.560 --> 01:09:42.307
and Dumbledore.

01:09:42.307 --> 01:09:44.140
And phrased a little
bit more formally, this

01:09:44.140 --> 01:09:46.479
says that if I have
the implication alpha

01:09:46.479 --> 01:09:51.970
implies beta, that I can draw the
conclusion that either not alpha

01:09:51.970 --> 01:09:53.470
or beta.

01:09:53.470 --> 01:09:55.190
Because there are only
two possibilities.

01:09:55.190 --> 01:09:58.370
Either alpha is true
or alpha is not true.

01:09:58.370 --> 01:10:01.540
So one of those possibilities
is alpha is not true.

01:10:01.540 --> 01:10:04.660
But if alpha is true, well,
then we can draw the conclusion

01:10:04.660 --> 01:10:05.990
that beta must be true.

01:10:05.990 --> 01:10:12.350
So either alpha is not true, or alpha is
true, in which case beta is also true.

01:10:12.350 --> 01:10:16.060
So this is one way to turn an
implication into just a statement about

01:10:16.060 --> 01:10:16.780
or.

01:10:16.780 --> 01:10:19.450
In addition to eliminating
implications, we can also

01:10:19.450 --> 01:10:21.980
eliminate biconditionals as well.

01:10:21.980 --> 01:10:23.500
So let's take an English example.

01:10:23.500 --> 01:10:27.930
Something like, it is raining
if and only if Harry is inside.

01:10:27.930 --> 01:10:31.280
And this if and only if really
sounds like that biconditional,

01:10:31.280 --> 01:10:35.520
that double arrow sign that we saw in
propositional logic not too long ago.

01:10:35.520 --> 01:10:38.160
And what does this actually mean
if we were to translate this?

01:10:38.160 --> 01:10:42.090
Well, this means that if it is
raining, then Harry is inside.

01:10:42.090 --> 01:10:44.590
And if Harry is inside,
then it is raining.

01:10:44.590 --> 01:10:47.440
The implication goes both ways.

01:10:47.440 --> 01:10:50.280
And this is what we would call
biconditional elimination.

01:10:50.280 --> 01:10:54.237
That I can take a biconditional,
A if and only if B,

01:10:54.237 --> 01:10:56.070
and translate that into
something like this.

01:10:56.070 --> 01:11:02.130
A implies B, and B implies A.
So many of these inference rules

01:11:02.130 --> 01:11:04.710
are taking logic that
uses certain symbols

01:11:04.710 --> 01:11:08.280
and turning them into different
symbols, taking an implication

01:11:08.280 --> 01:11:09.370
and turning it into an or.

01:11:09.370 --> 01:11:12.960
Or taking a biconditional and
turning it into implication.

01:11:12.960 --> 01:11:15.930
And another example of it
would be something like this.

01:11:15.930 --> 01:11:20.420
It is not true that both
Harry and Ron passed the test.

01:11:20.420 --> 01:11:22.170
Well, all right, how
do we translate that?

01:11:22.170 --> 01:11:23.230
What does that mean?

01:11:23.230 --> 01:11:27.120
Well, if it is not true that
both of them passed the test,

01:11:27.120 --> 01:11:31.200
well, then the reasonable conclusion we
might draw is that at least one of them

01:11:31.200 --> 01:11:32.370
didn't pass the test.

01:11:32.370 --> 01:11:35.580
So the conclusion is either
Harry did not pass the test,

01:11:35.580 --> 01:11:38.050
or Ron did not pass the test, or both.

01:11:38.050 --> 01:11:39.540
This is not an exclusive or.

01:11:39.540 --> 01:11:43.980
But if it is true that it is not
true, that both Harry and Ron passed

01:11:43.980 --> 01:11:47.160
the test, well, then either
Harry didn't pass the test

01:11:47.160 --> 01:11:49.580
or Ron didn't pass the test.

01:11:49.580 --> 01:11:52.320
And this type of law is
one of De Morgan's laws.

01:11:52.320 --> 01:11:57.330
Quite famous in logic, where the idea
is that we can turn an and into an or.

01:11:57.330 --> 01:12:00.690
We can take this and, that both
Harry and Ron passed the test,

01:12:00.690 --> 01:12:04.140
and turn it into an or by
moving the nots around.

01:12:04.140 --> 01:12:07.680
So if it is not true that
Harry and Ron passed the test,

01:12:07.680 --> 01:12:10.110
well, then either Harry
did not pass the test,

01:12:10.110 --> 01:12:13.200
or Ron did not pass the test either.

01:12:13.200 --> 01:12:16.590
And the way we frame that more
formally using logic is to say this.

01:12:16.590 --> 01:12:21.690
If it is not true that alpha
and beta, well, then either not

01:12:21.690 --> 01:12:24.598
alpha or not beta.

01:12:24.598 --> 01:12:26.640
The way I like to think
about this is that if you

01:12:26.640 --> 01:12:29.550
have a negation in front
of an and expression,

01:12:29.550 --> 01:12:32.190
you move the negation
inwards, so to speak.

01:12:32.190 --> 01:12:36.210
Moving the negation into each
of these individual sentences,

01:12:36.210 --> 01:12:38.920
and then flip the and into an or.

01:12:38.920 --> 01:12:42.090
So the negation moves inwards,
and the and flips into an or.

01:12:42.090 --> 01:12:47.908
So I go from not A and
B, to not A or not B.

01:12:47.908 --> 01:12:49.950
And there's actually a
reverse of De Morgan's law

01:12:49.950 --> 01:12:52.620
that goes in the other direction
for something like this.

01:12:52.620 --> 01:12:56.550
If I say, it is not true that
Harry or Ron passed the test,

01:12:56.550 --> 01:13:00.450
meaning neither of them passed the test,
well, then the conclusion I can draw

01:13:00.450 --> 01:13:05.440
is that Harry did not pass the
test, and Ron did not pass the test.

01:13:05.440 --> 01:13:08.940
So in this case, instead of turning
an and into an or, we're turning an

01:13:08.940 --> 01:13:10.830
or into an and.

01:13:10.830 --> 01:13:12.030
But the idea is the same.

01:13:12.030 --> 01:13:15.140
And this, again, is another
example of De Morgan's laws.

01:13:15.140 --> 01:13:20.007
And the way that works is that
if I have not A or B this time,

01:13:20.007 --> 01:13:21.340
the same logic's going to apply.

01:13:21.340 --> 01:13:23.700
I'm going to move the
negation inwards, and I'm

01:13:23.700 --> 01:13:26.880
going to flip, this time,
flip the or into an and.

01:13:26.880 --> 01:13:32.730
So if not A or B, meaning it is not
true that A or B, or alpha or beta,

01:13:32.730 --> 01:13:36.990
then I can say not alpha and not beta.

01:13:36.990 --> 01:13:40.630
Moving the negation inwards in
order to make that conclusion.

01:13:40.630 --> 01:13:41.880
So those are De Morgan's laws.

01:13:41.880 --> 01:13:45.005
And a couple of other inference rules
that are worth just taking a look at,

01:13:45.005 --> 01:13:47.680
one is the distributive
law that works this way.

01:13:47.680 --> 01:13:53.910
So if I have alpha and beta or gamma,
well, then much in the same way

01:13:53.910 --> 01:13:56.370
that you can use, in math,
use distributive laws

01:13:56.370 --> 01:13:59.750
to distribute operands, like
addition and multiplication,

01:13:59.750 --> 01:14:01.350
I can do a similar thing here.

01:14:01.350 --> 01:14:05.400
Where I can say if
alpha and beta or gamma,

01:14:05.400 --> 01:14:10.890
then I can say something like,
alpha and beta, or alpha and gamma.

01:14:10.890 --> 01:14:15.407
That I've been able to distribute this
and sign throughout this expression.

01:14:15.407 --> 01:14:17.490
So this is an example of
the distributive property

01:14:17.490 --> 01:14:21.240
or the distributive law, as applied
to logic in much the same way

01:14:21.240 --> 01:14:24.120
that you would distribute like a
multiplication over the addition

01:14:24.120 --> 01:14:26.560
of something, for example.

01:14:26.560 --> 01:14:28.060
This works the other way, too.

01:14:28.060 --> 01:14:32.250
So if, for example, I have
alpha or beta and gamma,

01:14:32.250 --> 01:14:34.590
I can distribute the or
throughout the expression.

01:14:34.590 --> 01:14:38.680
I can say alpha or beta,
and alpha or gamma.

01:14:38.680 --> 01:14:40.800
So the distributive law
works in that way, too.

01:14:40.800 --> 01:14:44.640
And it's helpful if I want to take an
or and move it into the expression.

01:14:44.640 --> 01:14:47.490
And we'll see an example soon of
why it is that we might actually

01:14:47.490 --> 01:14:50.440
care to do something like that.

01:14:50.440 --> 01:14:50.940
All right.

01:14:50.940 --> 01:14:53.920
So now we've seen a lot of
different inference rules.

01:14:53.920 --> 01:14:57.660
And the question now is how can we
use those inference rules to actually

01:14:57.660 --> 01:14:59.040
try and draw some conclusions?

01:14:59.040 --> 01:15:01.440
To actually try and prove
something about entailment,

01:15:01.440 --> 01:15:03.720
proving that given some
initial knowledge base,

01:15:03.720 --> 01:15:08.890
we would like to find some way
to prove that a query is true.

01:15:08.890 --> 01:15:10.830
Well, one way to think
about it is actually

01:15:10.830 --> 01:15:12.900
to think back to what we
talked about last time,

01:15:12.900 --> 01:15:14.790
when we talked about search problems.

01:15:14.790 --> 01:15:17.700
Recall again that search problems
have some sort of initial state.

01:15:17.700 --> 01:15:20.520
They have actions that you can
take from one state to another,

01:15:20.520 --> 01:15:23.610
as defined by a transition model that
tells you how to get from one state

01:15:23.610 --> 01:15:24.640
to another.

01:15:24.640 --> 01:15:27.120
We talked about testing
to see if you had a goal.

01:15:27.120 --> 01:15:31.530
And then some path cost function to see
how many steps did you have to take,

01:15:31.530 --> 01:15:35.340
or how costly was the
solution that you found.

01:15:35.340 --> 01:15:37.380
Now that we have these
inference rules that

01:15:37.380 --> 01:15:41.040
take some set of sentences
and propositional logic

01:15:41.040 --> 01:15:44.700
and get us some new set of
sentences in propositional logic,

01:15:44.700 --> 01:15:49.050
we can actually treat those
sentences, or those sets of sentences,

01:15:49.050 --> 01:15:51.610
as states inside of a search problem.

01:15:51.610 --> 01:15:54.060
So if we want to prove
that some query is true,

01:15:54.060 --> 01:15:56.610
prove that some logical
theorem is true, we

01:15:56.610 --> 01:16:00.150
can treat theorem proving as
a form of a search problem.

01:16:00.150 --> 01:16:03.420
I can say that we begin
in some initial state,

01:16:03.420 --> 01:16:06.330
where that initial state is the
knowledge base that I begin with.

01:16:06.330 --> 01:16:09.900
The set of all of the sentences
that I know to be true.

01:16:09.900 --> 01:16:11.580
What actions are available to me?

01:16:11.580 --> 01:16:13.830
Well, the actions are any
of the inference rules

01:16:13.830 --> 01:16:16.380
that I can apply at any given time.

01:16:16.380 --> 01:16:20.730
The transition model just tells me
after I apply the inference rule,

01:16:20.730 --> 01:16:23.290
here is the new set of all
of the knowledge that I have,

01:16:23.290 --> 01:16:26.568
which will be the old set of knowledge,
plus some additional inference

01:16:26.568 --> 01:16:28.860
that I've been able to draw,
much as in the same way we

01:16:28.860 --> 01:16:31.490
saw what we got when we
applied those inference rules

01:16:31.490 --> 01:16:33.000
and got some sort of conclusion.

01:16:33.000 --> 01:16:35.910
That conclusion gets added
to our knowledge base,

01:16:35.910 --> 01:16:38.550
and our transition
model will encode that.

01:16:38.550 --> 01:16:39.500
What is the goal test?

01:16:39.500 --> 01:16:41.250
Well, our goal test
is, you know, checking

01:16:41.250 --> 01:16:44.790
to see if we have proved the
statement we're trying to prove.

01:16:44.790 --> 01:16:49.170
If the thing we're trying to prove
is inside of our knowledge base.

01:16:49.170 --> 01:16:52.230
And the path cost function, the
thing we're trying to minimize,

01:16:52.230 --> 01:16:55.260
is maybe the number of inference
rules that we needed to use.

01:16:55.260 --> 01:16:59.160
The number of steps, so to
speak, inside of our proof.

01:16:59.160 --> 01:17:02.070
And so here we've been able to
apply the same types of ideas

01:17:02.070 --> 01:17:04.140
that we saw last time
with search problems,

01:17:04.140 --> 01:17:06.840
to something like trying to
prove something about knowledge

01:17:06.840 --> 01:17:11.048
by taking our knowledge and framing
it in terms that we can understand

01:17:11.048 --> 01:17:12.840
as a search problem,
with an initial state,

01:17:12.840 --> 01:17:15.210
with actions, with a transition model.

01:17:15.210 --> 01:17:17.080
So this shows a couple of things.

01:17:17.080 --> 01:17:19.310
One being how versatile
search problems are.

01:17:19.310 --> 01:17:23.130
That they can be the same types of
algorithms that we use to solve a maze,

01:17:23.130 --> 01:17:26.770
or figure out how to get from point A to
point B. Inside of driving directions,

01:17:26.770 --> 01:17:30.390
for example, can also be used
as a theorem proofing method.

01:17:30.390 --> 01:17:32.610
Of taking some sort of
starting knowledge base

01:17:32.610 --> 01:17:36.210
and trying to prove something
about that knowledge.

01:17:36.210 --> 01:17:39.420
So this, yet again, is a second
way, in addition to model checking,

01:17:39.420 --> 01:17:43.000
to try and prove that
certain statements are true.

01:17:43.000 --> 01:17:46.425
But it turns out there's yet another
way that we can try and apply inference,

01:17:46.425 --> 01:17:48.800
and we'll talk about this now,
which is not the only way,

01:17:48.800 --> 01:17:50.700
but certainly one of the most common.

01:17:50.700 --> 01:17:52.850
Which is known as resolution.

01:17:52.850 --> 01:17:55.890
And resolution is based
on another inference rule

01:17:55.890 --> 01:17:57.140
that we'll take a look at now.

01:17:57.140 --> 01:17:59.090
Quite a powerful
inference rule that will

01:17:59.090 --> 01:18:03.110
let us prove anything that can
be proven about a knowledge base.

01:18:03.110 --> 01:18:05.730
And it's based on this basic idea.

01:18:05.730 --> 01:18:09.680
Let's say I know that either
Ron is in the Great Hall,

01:18:09.680 --> 01:18:12.240
or Hermione is in the library.

01:18:12.240 --> 01:18:16.790
And let's say I also know that
Ron is not in the Great Hall.

01:18:16.790 --> 01:18:20.480
Based on those two pieces of
information, what can I conclude?

01:18:20.480 --> 01:18:24.470
Well, I could pretty reasonably conclude
that Hermione must be in the library.

01:18:24.470 --> 01:18:25.560
How do I know that?

01:18:25.560 --> 01:18:29.360
Well, it's because these two
statements, these two, what we'll call,

01:18:29.360 --> 01:18:32.930
complementary literals-- literals
that complement each other,

01:18:32.930 --> 01:18:34.970
they are opposites of each other--

01:18:34.970 --> 01:18:36.920
seem to conflict with each other.

01:18:36.920 --> 01:18:39.800
This sentence tells us that
either Ron is in the Great Hall

01:18:39.800 --> 01:18:41.970
or Hermione is in the library.

01:18:41.970 --> 01:18:44.420
So if we know that Ron
is not in the Great Hall,

01:18:44.420 --> 01:18:49.880
that conflicts with this one, which
means Hermione must be in the library.

01:18:49.880 --> 01:18:54.150
And this we can frame as a more general
rule, known as the unit resolution

01:18:54.150 --> 01:18:54.650
rule.

01:18:54.650 --> 01:19:01.880
A rule that says that if we have P or
Q, and we also know not P, well, then

01:19:01.880 --> 01:19:04.700
from that we can reasonably conclude Q.

01:19:04.700 --> 01:19:08.280
That if P or Q are true, and
we know that P is not true,

01:19:08.280 --> 01:19:12.170
the only possibility is
for Q to then be true.

01:19:12.170 --> 01:19:14.660
And this, it turns out, is
quite a powerful inference rule

01:19:14.660 --> 01:19:17.450
in terms of what it can do,
in part because we can quickly

01:19:17.450 --> 01:19:19.260
start to generalize this rule.

01:19:19.260 --> 01:19:23.360
This Q right here doesn't need to
just be a single propositional symbol.

01:19:23.360 --> 01:19:26.720
It could be multiple, all chained
together in a single clause,

01:19:26.720 --> 01:19:27.690
as we'll call it.

01:19:27.690 --> 01:19:32.750
So if I had something like P or Q1,
or Q2, or Q3, so on and so forth,

01:19:32.750 --> 01:19:36.740
up until Qn, so I had n,
different, other variables,

01:19:36.740 --> 01:19:40.910
and I have not P, well, then what
happens when these two complement

01:19:40.910 --> 01:19:44.990
each other is that these two
clauses resolve, so to speak,

01:19:44.990 --> 01:19:50.570
to produce a new clause that is
just Q1 or Q2, all the way up to Qn.

01:19:50.570 --> 01:19:53.890
And in an or, the order of the arguments
in the or doesn't actually matter.

01:19:53.890 --> 01:19:55.240
The P doesn't need to
be the first thing.

01:19:55.240 --> 01:19:56.532
It could've been in the middle.

01:19:56.532 --> 01:20:00.020
But the idea here is that
if I have P in one clause,

01:20:00.020 --> 01:20:02.060
and not P and the other
clause, well, then

01:20:02.060 --> 01:20:05.090
I know that one of these
remaining things must be true.

01:20:05.090 --> 01:20:08.900
I've resolved them in order
to produce a new clause.

01:20:08.900 --> 01:20:12.870
But it turns out we can generalize
this idea even further, in fact,

01:20:12.870 --> 01:20:16.950
and display even more power that we
can have with this resolution rule.

01:20:16.950 --> 01:20:18.768
So let's take another example.

01:20:18.768 --> 01:20:21.560
Let's say, for instance, that I
know the same piece of information,

01:20:21.560 --> 01:20:25.730
that either Ron is in the Great
Hall or Hermione is in the library.

01:20:25.730 --> 01:20:27.980
And the second piece
of information I know

01:20:27.980 --> 01:20:33.780
is that Ron is not in the Great
Hall or Harry is sleeping.

01:20:33.780 --> 01:20:35.840
So it's not just a single
piece of information.

01:20:35.840 --> 01:20:40.070
I have two different clauses, and
we'll define clauses more precisely

01:20:40.070 --> 01:20:41.760
in just a moment.

01:20:41.760 --> 01:20:42.890
What do I know here?

01:20:42.890 --> 01:20:46.670
Well, again, for any propositional
symbol, like Ron is in the Great Hall,

01:20:46.670 --> 01:20:48.720
there are only two possibilities.

01:20:48.720 --> 01:20:52.820
Either Ron is in the Great Hall,
in which case, based on resolution,

01:20:52.820 --> 01:20:55.220
we know that Harry must be sleeping.

01:20:55.220 --> 01:20:58.670
Or Ron is not in the
Great Hall, in which case

01:20:58.670 --> 01:21:03.590
we know, based on the same rule,
that Hermione must be in the library.

01:21:03.590 --> 01:21:05.600
Based on those two
things in combination,

01:21:05.600 --> 01:21:08.240
I can say, based on these
two premises, that I

01:21:08.240 --> 01:21:14.660
can conclude that either Hermione is
in the library or Harry is sleeping.

01:21:14.660 --> 01:21:17.580
So again, because these two
conflict with each other,

01:21:17.580 --> 01:21:19.975
I know that one of
these two must be true.

01:21:19.975 --> 01:21:22.850
And you can take a closer look and
try and reason through that logic.

01:21:22.850 --> 01:21:26.690
Make sure you convince yourself
that you believe this conclusion.

01:21:26.690 --> 01:21:29.600
Stated more generally, we
can name this resolution rule

01:21:29.600 --> 01:21:32.990
by saying that if we
know P or Q is true,

01:21:32.990 --> 01:21:37.370
and we also know that
not P or R is true,

01:21:37.370 --> 01:21:41.480
we resolve these two clauses
together to get a new clause, Q

01:21:41.480 --> 01:21:45.630
or R. That either Q or R must be true.

01:21:45.630 --> 01:21:48.200
And again, much as in
the last case, Q and R

01:21:48.200 --> 01:21:51.050
don't need to just be single
propositional symbols.

01:21:51.050 --> 01:21:52.460
It could be multiple symbols.

01:21:52.460 --> 01:21:57.020
So if I had a rule that had a P or
Q1 or Q2 or Q3, so on and so forth,

01:21:57.020 --> 01:21:59.990
up until Qn, where n
is just some number.

01:21:59.990 --> 01:22:06.820
And likewise, I had not P or R1 or F2,
so on and so forth, up until Rm, m,

01:22:06.820 --> 01:22:09.620
where m, again, is
just some other number,

01:22:09.620 --> 01:22:13.970
I can resolve these two clauses together
to get one of these must be true.

01:22:13.970 --> 01:22:15.740
Q1 or Q2, up until Qn.

01:22:15.740 --> 01:22:18.980
Or R1 or R2, up until Rm.

01:22:18.980 --> 01:22:23.810
And this is just a generalization
of that same rule we saw before.

01:22:23.810 --> 01:22:27.440
Each of these things here
we're going to call a clause.

01:22:27.440 --> 01:22:32.020
Where a clause is formally defined
as a disjunction of literals.

01:22:32.020 --> 01:22:35.990
Where a disjunction means it's a bunch
of things that are connected with or.

01:22:35.990 --> 01:22:38.390
Disjunction means things
connected with or.

01:22:38.390 --> 01:22:41.410
Conjunction, meanwhile, is
things connected with and.

01:22:41.410 --> 01:22:45.410
And a literal is either a
propositional symbol or the opposite

01:22:45.410 --> 01:22:46.680
of a propositional symbol.

01:22:46.680 --> 01:22:50.420
So it's something like P
or Q, or not P or not Q,

01:22:50.420 --> 01:22:54.620
those are all propositional symbols,
or not of the propositional symbols,

01:22:54.620 --> 01:22:57.003
and we call those literals.

01:22:57.003 --> 01:22:58.670
So a clause is just something like this.

01:22:58.670 --> 01:23:02.240
P or Q or R, for example.

01:23:02.240 --> 01:23:04.730
Meanwhile, what this
gives us an ability to do

01:23:04.730 --> 01:23:08.810
is it gives us an ability to
turn logic, any logical sentence,

01:23:08.810 --> 01:23:12.260
into something called
conjunctive normal form.

01:23:12.260 --> 01:23:15.700
A conjunctive normal form
sentence is a logical sentence

01:23:15.700 --> 01:23:18.530
that is a conjunction of clauses.

01:23:18.530 --> 01:23:23.090
Recall again, conjunction means things
are connected to one another using and.

01:23:23.090 --> 01:23:25.580
And so a conjunction of
clauses means that it

01:23:25.580 --> 01:23:29.680
is an and of individual clauses,
each of which has in it.

01:23:29.680 --> 01:23:30.830
So something like this.

01:23:30.830 --> 01:23:38.000
A or B or C, and D or not E, and
F or G. Everything in parentheses

01:23:38.000 --> 01:23:39.670
is one clause.

01:23:39.670 --> 01:23:43.250
All of the clauses are connected
to each other using an and,

01:23:43.250 --> 01:23:47.400
and everything in the clause
is separated using an or.

01:23:47.400 --> 01:23:50.960
And this is just a standard form that
we can translate a logical sentence

01:23:50.960 --> 01:23:54.740
into that just makes it easy to
work with and easy to manipulate.

01:23:54.740 --> 01:23:57.650
And it turns out that we can
take any sentence in logic

01:23:57.650 --> 01:24:00.440
and turn it into
conjunctive normal form,

01:24:00.440 --> 01:24:04.350
just by applying some inference
rules and transformations to it.

01:24:04.350 --> 01:24:07.470
So we'll take a look at how
we can actually do that.

01:24:07.470 --> 01:24:10.280
So what is the process for
taking a logical formula

01:24:10.280 --> 01:24:14.582
and converting it into injunctive
normal form, otherwise known as CNF?

01:24:14.582 --> 01:24:16.790
Well, the process looks a
little something like this.

01:24:16.790 --> 01:24:19.100
We need to take all of
the symbols that are not

01:24:19.100 --> 01:24:22.350
part of conjunctive normal form-- the
biconditionals, and the implications,

01:24:22.350 --> 01:24:23.310
and so forth.

01:24:23.310 --> 01:24:26.330
And turn them into something
that is more closely

01:24:26.330 --> 01:24:28.440
like conjunctive normal form.

01:24:28.440 --> 01:24:31.040
So the first step will be
to eliminate biconditionals.

01:24:31.040 --> 01:24:33.440
Those if and only if double arrows.

01:24:33.440 --> 01:24:35.420
And we know how to
eliminate biconditionals

01:24:35.420 --> 01:24:38.490
because we saw there was an
inference rule to do just that.

01:24:38.490 --> 01:24:42.710
Anytime I have an expression,
like alpha, if and only if beta,

01:24:42.710 --> 01:24:47.960
I can turn that into alpha implies
beta, and beta implies alpha, based

01:24:47.960 --> 01:24:50.780
on that inference rule we saw before.

01:24:50.780 --> 01:24:53.150
Likewise, in addition to
eliminating biconditionals,

01:24:53.150 --> 01:24:55.160
I can eliminate implications as well.

01:24:55.160 --> 01:24:56.980
The if/then arrows.

01:24:56.980 --> 01:25:00.410
And I can do that using the same
inference rule we saw before, too.

01:25:00.410 --> 01:25:02.900
Taking alpha implies
beta, and turning that

01:25:02.900 --> 01:25:06.920
into not alpha or beta,
because that is logically

01:25:06.920 --> 01:25:10.730
equivalent to this first thing here.

01:25:10.730 --> 01:25:13.550
Then we can move nots inwards,
because we don't want nots

01:25:13.550 --> 01:25:15.090
on the outsides of our expressions.

01:25:15.090 --> 01:25:18.590
Conjunctive normal form requires
that its just clause and clause

01:25:18.590 --> 01:25:20.120
and clause and clause.

01:25:20.120 --> 01:25:23.840
Any nots need to be immediately
next to propositional symbols.

01:25:23.840 --> 01:25:26.840
But we can move those nots
around using De Morgan's laws.

01:25:26.840 --> 01:25:33.290
By taking something like, not A and
B, and turn it into not A or not B,

01:25:33.290 --> 01:25:36.110
for example, using de Morgan's
laws to manipulate that.

01:25:36.110 --> 01:25:38.767
And after that, all we'll be
left with are ands and ors,

01:25:38.767 --> 01:25:40.100
and those are easy to deal with.

01:25:40.100 --> 01:25:44.420
We can use the distributive law to
distribute the ors so that the ors end

01:25:44.420 --> 01:25:47.060
up on the inside of the
expression, so to speak,

01:25:47.060 --> 01:25:49.732
and the ands end up on the outside.

01:25:49.732 --> 01:25:52.190
So this is the general pattern
for how we'll take a formula

01:25:52.190 --> 01:25:54.570
and convert it into
conjunctive normal form.

01:25:54.570 --> 01:25:56.750
And let's now take a
look at an example of how

01:25:56.750 --> 01:25:59.720
we would do this, and explore
then, why it is that we

01:25:59.720 --> 01:26:01.950
would want to do something like this.

01:26:01.950 --> 01:26:03.000
Here's how we can do it.

01:26:03.000 --> 01:26:04.880
Let's take this formula, for example.

01:26:04.880 --> 01:26:08.510
P or Q implies R, and
I'd like to convert this

01:26:08.510 --> 01:26:12.650
into conjunctive normal form,
where it's all ands of clauses,

01:26:12.650 --> 01:26:15.090
and every clause is
a disjunctive clause.

01:26:15.090 --> 01:26:16.695
It's or is together.

01:26:16.695 --> 01:26:18.320
So what's the first thing I need to do?

01:26:18.320 --> 01:26:20.130
Well, this is an implication.

01:26:20.130 --> 01:26:22.460
So let me go ahead and
remove that implication.

01:26:22.460 --> 01:26:27.740
Using the implication inference
rule, I can turn P or Q into--

01:26:27.740 --> 01:26:34.190
P or Q implies R, into not P or
Q or R. So that's the first step.

01:26:34.190 --> 01:26:36.390
I've gotten rid of the implication.

01:26:36.390 --> 01:26:40.370
And next, I can get rid of the not on
the outside of this expression, too.

01:26:40.370 --> 01:26:45.830
I can move the nots inwards so they're
closer to the literals themselves

01:26:45.830 --> 01:26:47.390
by using De Morgan's laws.

01:26:47.390 --> 01:26:51.470
And De Morgan's law says
that not P or Q is equivalent

01:26:51.470 --> 01:26:57.200
to not P and not Q. Again here,
just applying the inference rules

01:26:57.200 --> 01:27:01.400
that we've already seen in order
to translate these statements.

01:27:01.400 --> 01:27:04.460
And now I have two things
that are separated by an

01:27:04.460 --> 01:27:07.500
or, where this thing on
the inside is an and.

01:27:07.500 --> 01:27:10.850
What I'd really like is to move the
or so the ors are on the inside,

01:27:10.850 --> 01:27:14.960
because conjunctive normal form means
I need clause and clause and clause

01:27:14.960 --> 01:27:15.960
and clause.

01:27:15.960 --> 01:27:18.560
And so to do that, I can
use the distributive law.

01:27:18.560 --> 01:27:25.400
If I have not P and not Q or R, I can
distribute the or R to both of these

01:27:25.400 --> 01:27:31.100
to get not P or R, and not Q or
R using the distributive law.

01:27:31.100 --> 01:27:34.820
And this now, here at the bottom,
is in conjunctive normal form.

01:27:34.820 --> 01:27:39.080
It is a conjunction, an
and, of disjunctions,

01:27:39.080 --> 01:27:42.510
of clauses that just
are separated by ors.

01:27:42.510 --> 01:27:46.400
So this process can be used by any
formula to take a logical sentence

01:27:46.400 --> 01:27:49.220
and turn it into this
conjuncture normal form, where

01:27:49.220 --> 01:27:54.022
I have clause and clause and clause
and clause and clause, and so on.

01:27:54.022 --> 01:27:54.980
So why is this helpful?

01:27:54.980 --> 01:27:57.260
Why do we even care about
taking all these sentences

01:27:57.260 --> 01:27:58.940
and converting them into this form?

01:27:58.940 --> 01:28:02.860
It's because once they're in this
form where we have these clauses,

01:28:02.860 --> 01:28:06.850
these clauses are the inputs to the
resolution, inference rule that we

01:28:06.850 --> 01:28:07.660
saw a moment ago.

01:28:07.660 --> 01:28:11.260
That if I have two clauses where
there's something that conflicts,

01:28:11.260 --> 01:28:13.690
or something complementary
between those two clauses,

01:28:13.690 --> 01:28:17.470
I can resolve them to get a new
clause, to draw a new conclusion.

01:28:17.470 --> 01:28:20.530
And we call this process
inference by resolution.

01:28:20.530 --> 01:28:23.920
Using the resolution rule to
draw some sort of inference.

01:28:23.920 --> 01:28:28.020
And it's based on the same idea,
that if I have P or Q, this clause,

01:28:28.020 --> 01:28:32.680
and I have not P or R, that I can
resolve these two clauses together

01:28:32.680 --> 01:28:35.680
to get Q or R as the resulting clause.

01:28:35.680 --> 01:28:39.243
A new piece of information
that I didn't have before.

01:28:39.243 --> 01:28:42.160
Now, a couple of key points that are
worth noting about this before we

01:28:42.160 --> 01:28:43.990
talk about the actual algorithm.

01:28:43.990 --> 01:28:47.850
One thing is that, let's
imagine we have P or Q or S,

01:28:47.850 --> 01:28:52.780
and I also have not P or R or
S. The resolution rule says

01:28:52.780 --> 01:28:55.990
that because this P
conflicts with this not P,

01:28:55.990 --> 01:29:01.052
we would resolve to put everything
else together, to get Q or S or R or S.

01:29:01.052 --> 01:29:05.800
But it turns out that this double S is
redundant-- or S here and or S there.

01:29:05.800 --> 01:29:07.990
It doesn't change the
meaning of the sentence.

01:29:07.990 --> 01:29:10.570
So in resolution, when we
do this resolution process,

01:29:10.570 --> 01:29:13.180
we usually also do a
process known as factoring,

01:29:13.180 --> 01:29:16.850
where we take any duplicate variables
that show up and just eliminate them.

01:29:16.850 --> 01:29:23.170
So Q or S or R or S just becomes Q or R
or S. The S only needs to appear once.

01:29:23.170 --> 01:29:26.290
No need to include it multiple times.

01:29:26.290 --> 01:29:28.420
Now, one final question
worth considering

01:29:28.420 --> 01:29:33.250
is what happens if I try to
resolve P and not P together?

01:29:33.250 --> 01:29:36.760
If I know that P is true, and
I know that not P is true,

01:29:36.760 --> 01:29:39.850
well, resolution says I can merge
these clauses together and look

01:29:39.850 --> 01:29:41.570
at everything else.

01:29:41.570 --> 01:29:43.600
Well, in this case,
there is nothing else.

01:29:43.600 --> 01:29:46.570
So I'm left with what we
might call the empty clause.

01:29:46.570 --> 01:29:48.130
I'm left with nothing.

01:29:48.130 --> 01:29:51.220
And the empty clause is always false.

01:29:51.220 --> 01:29:54.220
The empty clause is equivalent
to just being false.

01:29:54.220 --> 01:29:55.720
And that's pretty reasonable.

01:29:55.720 --> 01:30:01.690
Because it's impossible for both P and
not P to both hold at the same time.

01:30:01.690 --> 01:30:03.910
P is either true or it's not true.

01:30:03.910 --> 01:30:07.250
Which means that if P is
true, then this must be false.

01:30:07.250 --> 01:30:09.410
And if this is true,
then this must be false.

01:30:09.410 --> 01:30:12.170
There's no way for both of
these to hold at the same time.

01:30:12.170 --> 01:30:15.640
So if ever I try and resolve
these two, it's a contradiction,

01:30:15.640 --> 01:30:18.820
and I'll end up getting this empty
clause, where the empty clause

01:30:18.820 --> 01:30:21.730
I can call equivalent to false.

01:30:21.730 --> 01:30:25.750
And this idea that if I resolve
these two contradictory terms I

01:30:25.750 --> 01:30:30.280
get the empty clause, this is the
basis for our inference by resolution

01:30:30.280 --> 01:30:30.937
algorithm.

01:30:30.937 --> 01:30:32.770
Here is how we're going
to perform inference

01:30:32.770 --> 01:30:35.420
by resolution at a very high level.

01:30:35.420 --> 01:30:40.000
We want to prove that our knowledge
base entails some query alpha.

01:30:40.000 --> 01:30:43.300
That based on the knowledge we
have, we can prove conclusively

01:30:43.300 --> 01:30:45.950
that alpha is going to be true.

01:30:45.950 --> 01:30:47.540
How are we going to do that?

01:30:47.540 --> 01:30:49.450
Well, in order to do
that, we're going to try

01:30:49.450 --> 01:30:54.100
to prove that if we know the
knowledge and not alpha, that that

01:30:54.100 --> 01:30:55.760
would be a contradiction.

01:30:55.760 --> 01:30:58.510
And this is a common technique in
computer science more generally.

01:30:58.510 --> 01:31:01.720
This idea of proving
something by contradiction.

01:31:01.720 --> 01:31:04.510
If I want to prove
that something is true,

01:31:04.510 --> 01:31:08.320
I can do so by first
assuming that it is false,

01:31:08.320 --> 01:31:10.450
and showing that it
would be contradictory.

01:31:10.450 --> 01:31:12.770
Showing that it leads
to some contradiction.

01:31:12.770 --> 01:31:16.120
And if the thing I'm trying to
prove, if when I assume it's false

01:31:16.120 --> 01:31:19.090
leads to a contradiction,
then it must be true.

01:31:19.090 --> 01:31:22.745
And that's the logical approach, or the
idea, behind a proof by contradiction.

01:31:22.745 --> 01:31:24.370
And that's what we're going to do here.

01:31:24.370 --> 01:31:27.610
We want to prove that
this query alpha is true,

01:31:27.610 --> 01:31:30.440
so we're going to assume
that it's not true.

01:31:30.440 --> 01:31:32.410
We're going to assume not alpha.

01:31:32.410 --> 01:31:34.960
And we're going to try and
prove that it's a contradiction.

01:31:34.960 --> 01:31:37.240
If we do get a
contradiction, well, then we

01:31:37.240 --> 01:31:40.690
know that our knowledge
entails the query alpha.

01:31:40.690 --> 01:31:43.300
If we don't get a contradiction,
there is no entail.

01:31:43.300 --> 01:31:45.670
This is this idea of a
proof by contradiction

01:31:45.670 --> 01:31:48.280
of assuming the opposite of
what you're trying to prove,

01:31:48.280 --> 01:31:51.940
and if you can demonstrate that that's a
contradiction, then what you're proving

01:31:51.940 --> 01:31:54.043
must be true.

01:31:54.043 --> 01:31:55.960
But more formally, how
do we actually do this?

01:31:55.960 --> 01:32:00.460
How do we check that
knowledge base and not alpha

01:32:00.460 --> 01:32:02.420
is going to lead to a contradiction?

01:32:02.420 --> 01:32:05.620
Well, here is where
resolution comes into play.

01:32:05.620 --> 01:32:09.490
To determine if our knowledge
base entails some query alpha,

01:32:09.490 --> 01:32:13.510
we're going to convert knowledge
base and not alpha to conjunction

01:32:13.510 --> 01:32:14.260
normal form.

01:32:14.260 --> 01:32:18.700
That form where we have a whole bunch
of clauses that are all anded together.

01:32:18.700 --> 01:32:21.080
And when we have these
individual clauses,

01:32:21.080 --> 01:32:25.900
now we can keep checking to
see if we can use resolution

01:32:25.900 --> 01:32:27.940
to produce a new clause.

01:32:27.940 --> 01:32:31.030
We can take any pair
of clauses and check.

01:32:31.030 --> 01:32:34.240
Is there some literal that is
the opposite of each other,

01:32:34.240 --> 01:32:36.430
or complementary to each
other, in both of them?

01:32:36.430 --> 01:32:40.180
For example, I have a P in one
clause, and a not P in another clause.

01:32:40.180 --> 01:32:43.780
Or an R in one clause, and
a not R in another clause.

01:32:43.780 --> 01:32:45.940
If ever I have that
situation, where once I

01:32:45.940 --> 01:32:49.210
convert to conjunctive normal form
and I have a whole bunch of clauses,

01:32:49.210 --> 01:32:54.010
I see two clauses that I can resolve to
produce a new clause, then I'll do so.

01:32:54.010 --> 01:32:55.340
This process occurs in a loop.

01:32:55.340 --> 01:32:58.240
I'm going to keep checking to
see if I can use resolution

01:32:58.240 --> 01:33:01.820
to produce a new clause, and keep using
those new clauses to try to generate

01:33:01.820 --> 01:33:04.820
more new clauses after that.

01:33:04.820 --> 01:33:07.310
Now, it just so may
happen that eventually, we

01:33:07.310 --> 01:33:09.593
may produce the empty clause.

01:33:09.593 --> 01:33:11.260
The clause we were talking about before.

01:33:11.260 --> 01:33:16.010
If I resolve P and not P together,
that produces the empty clause.

01:33:16.010 --> 01:33:18.920
And the empty clause
we know to be false.

01:33:18.920 --> 01:33:21.920
Because we know that there's
no way for both P and not

01:33:21.920 --> 01:33:25.590
P to both simultaneously be true.

01:33:25.590 --> 01:33:29.395
So if ever we produce the empty
clause, then we have a contradiction.

01:33:29.395 --> 01:33:31.520
And if we have a contradiction,
that's exactly what

01:33:31.520 --> 01:33:33.983
we were trying to do in
a proof by contradiction.

01:33:33.983 --> 01:33:36.650
If we have a contradiction, then
we know that our knowledge base

01:33:36.650 --> 01:33:38.690
must entail this query alpha.

01:33:38.690 --> 01:33:41.890
We know that alpha must be true.

01:33:41.890 --> 01:33:44.240
And it turns out-- and we
won't go into the proof here--

01:33:44.240 --> 01:33:48.050
but you can show that, otherwise, if
you don't produce the empty clause,

01:33:48.050 --> 01:33:49.700
then there is no entailment.

01:33:49.700 --> 01:33:52.970
If we run into a situation where
there are no more new clauses to add,

01:33:52.970 --> 01:33:55.280
we've done all the
resolution that we can do,

01:33:55.280 --> 01:33:57.680
and yet we still haven't
produced the empty clause,

01:33:57.680 --> 01:34:00.680
then there is no
entailment in this case.

01:34:00.680 --> 01:34:03.020
And this now is the
resolution algorithm.

01:34:03.020 --> 01:34:04.940
And it's very abstract
looking, especially

01:34:04.940 --> 01:34:07.862
this idea of what does that even
mean to have the empty clause.

01:34:07.862 --> 01:34:09.320
So let's take a look at an example.

01:34:09.320 --> 01:34:13.250
Actually try and prove some
entailment by using this inference

01:34:13.250 --> 01:34:15.720
by resolution process.

01:34:15.720 --> 01:34:16.970
So here's our question.

01:34:16.970 --> 01:34:18.500
We have this knowledge base.

01:34:18.500 --> 01:34:20.240
Here is the knowledge that we know.

01:34:20.240 --> 01:34:27.560
A or B, and not B or C, and not C.
And we want to know if all of this

01:34:27.560 --> 01:34:30.140
entails A.

01:34:30.140 --> 01:34:32.870
So this is our knowledge base
here, this whole log thing.

01:34:32.870 --> 01:34:37.430
And our query alpha is just
this propositional symbol A.

01:34:37.430 --> 01:34:38.510
So what do we do?

01:34:38.510 --> 01:34:40.760
Well, first we want to
prove by contradiction.

01:34:40.760 --> 01:34:43.880
So we want to first
assume that A is false,

01:34:43.880 --> 01:34:46.360
and see if that leads to
some sort of contradiction.

01:34:46.360 --> 01:34:48.110
So here is what we're
going to start with.

01:34:48.110 --> 01:34:52.970
A or B, and not B or C, and not
C. This is our knowledge base.

01:34:52.970 --> 01:34:55.550
And we're going to
assume not A. We're going

01:34:55.550 --> 01:35:01.050
to assume that the thing we're
trying to prove is, in fact, false.

01:35:01.050 --> 01:35:03.800
And so this is now in
conjunctive normal form,

01:35:03.800 --> 01:35:05.690
and I have four different clauses.

01:35:05.690 --> 01:35:12.930
I have A or B. I have not B or C.
I have not C. And I have not A.

01:35:12.930 --> 01:35:17.630
And now, I can begin to just pick two
clauses that I can resolve and apply

01:35:17.630 --> 01:35:20.090
the resolution rule to them.

01:35:20.090 --> 01:35:21.890
And so looking at these
four clauses I see,

01:35:21.890 --> 01:35:25.730
all right, these two clauses
are ones I can resolve.

01:35:25.730 --> 01:35:29.570
I can resolve them because there
are complementary literals that

01:35:29.570 --> 01:35:30.300
show up in them.

01:35:30.300 --> 01:35:32.870
There's a C here, and a not C here.

01:35:32.870 --> 01:35:38.640
So just looking at these two clauses,
if I know that not B or C is true,

01:35:38.640 --> 01:35:41.210
and I know that C is
not true, well, then

01:35:41.210 --> 01:35:45.690
I can resolve these two clauses to say,
all right, not B. That must be true.

01:35:45.690 --> 01:35:49.340
I can generate this new clause
as a new piece of information

01:35:49.340 --> 01:35:51.995
that I now know to be true.

01:35:51.995 --> 01:35:53.870
And all right, now I
can repeat this process.

01:35:53.870 --> 01:35:55.100
Do the process again.

01:35:55.100 --> 01:35:58.460
Can I use resolution again
to get some new conclusion?

01:35:58.460 --> 01:35:59.510
Well, it turns out I can.

01:35:59.510 --> 01:36:03.020
I can use that new clause I just
generated, along with this one here.

01:36:03.020 --> 01:36:04.910
There are complementary literals.

01:36:04.910 --> 01:36:10.580
This B is complementary to, or
conflicts with this not B over here.

01:36:10.580 --> 01:36:16.640
And so if I know that A or B is
true, and I know that B is not true,

01:36:16.640 --> 01:36:19.860
well, then the only remaining
possibility is that A must be true.

01:36:19.860 --> 01:36:23.940
So now we have A. That is a new clause
that I've been able to generate.

01:36:23.940 --> 01:36:25.940
And now I can do this one
more time, and looking

01:36:25.940 --> 01:36:27.530
for two clauses that can be resolved.

01:36:27.530 --> 01:36:29.780
And you might programmatically
do this by just looping

01:36:29.780 --> 01:36:32.600
over all possible pairs
of clauses and checking

01:36:32.600 --> 01:36:34.520
for complementary literals in each.

01:36:34.520 --> 01:36:36.830
And here I can say, all
right, I found two clauses.

01:36:36.830 --> 01:36:40.740
Not A and A that
conflict with each other.

01:36:40.740 --> 01:36:43.070
And when I resolve these
two together, well, this

01:36:43.070 --> 01:36:46.340
is the same as when we were
resolving P and not P from before.

01:36:46.340 --> 01:36:50.060
When I resolve these two clauses
together, I get rid of the As,

01:36:50.060 --> 01:36:52.550
and I'm left with the empty clause.

01:36:52.550 --> 01:36:55.070
And the empty clause we know
to be false, which means we

01:36:55.070 --> 01:36:56.210
have a contradiction.

01:36:56.210 --> 01:36:58.970
Which means we can safely
say, that this whole knowledge

01:36:58.970 --> 01:37:02.420
base does entail A. That
if this sentence is true,

01:37:02.420 --> 01:37:06.480
that we know that A,
for sure, is also true.

01:37:06.480 --> 01:37:09.020
So this now, using
inference by resolution,

01:37:09.020 --> 01:37:12.050
is an entirely different
way to take some statement

01:37:12.050 --> 01:37:14.540
and try and prove that
it is, in fact, true.

01:37:14.540 --> 01:37:16.880
Instead of enumerating
all of the possible worlds

01:37:16.880 --> 01:37:20.150
that we might be in in order to
try to figure out in which case

01:37:20.150 --> 01:37:23.060
is the knowledge base true, and
in which case is our query true.

01:37:23.060 --> 01:37:26.270
Instead we use this
resolution algorithm to say,

01:37:26.270 --> 01:37:29.360
let's keep trying to figure out
what conclusions we can draw

01:37:29.360 --> 01:37:31.450
and see if we reach a contradiction.

01:37:31.450 --> 01:37:33.200
And if we reach a
contradiction, then that

01:37:33.200 --> 01:37:37.310
tells us something about whether our
knowledge actually entails the query

01:37:37.310 --> 01:37:38.110
or not.

01:37:38.110 --> 01:37:40.485
And it turns out there are
many different algorithms that

01:37:40.485 --> 01:37:41.745
can be used for inference.

01:37:41.745 --> 01:37:44.120
What we've just looked at here
are just a couple of them.

01:37:44.120 --> 01:37:48.380
And, in fact, all of this is just
based on one particular type of logic.

01:37:48.380 --> 01:37:52.190
It's based on propositional logic,
where we have these individual symbols

01:37:52.190 --> 01:37:55.610
and we connect them using and,
and or, and not, and implies,

01:37:55.610 --> 01:37:56.930
and biconditionals.

01:37:56.930 --> 01:38:01.170
But propositional logic is not the
only kind of logic that exists.

01:38:01.170 --> 01:38:03.170
And in fact, we see that
there are limitations

01:38:03.170 --> 01:38:05.960
that exist in propositional
logic, especially

01:38:05.960 --> 01:38:10.310
as we saw in examples like
with the Mastermind example,

01:38:10.310 --> 01:38:12.740
or with the example
with the logic puzzle

01:38:12.740 --> 01:38:16.550
where we had different Hogwart's has
people that belong to different houses,

01:38:16.550 --> 01:38:19.370
and we were trying to figure out
who belonged to which houses.

01:38:19.370 --> 01:38:21.530
There were a lot of different
propositional symbols

01:38:21.530 --> 01:38:25.867
that we needed in order to
represent some fairly basic ideas.

01:38:25.867 --> 01:38:27.950
So now as a final topic
that we'll take a look at,

01:38:27.950 --> 01:38:31.040
just before we end class today,
is one final type of logic,

01:38:31.040 --> 01:38:33.200
different from
propositional logic, known

01:38:33.200 --> 01:38:35.330
as first order logic,
which is a little bit more

01:38:35.330 --> 01:38:37.790
powerful than
propositional logic, and is

01:38:37.790 --> 01:38:41.540
going to make it easier for us to
express certain types of ideas.

01:38:41.540 --> 01:38:44.090
In propositional logic, if
we think back to that puzzle

01:38:44.090 --> 01:38:46.280
with the people and
the Hogwart's houses,

01:38:46.280 --> 01:38:48.620
we had a whole bunch of
symbols, and every symbol

01:38:48.620 --> 01:38:50.510
could only be true or false.

01:38:50.510 --> 01:38:53.120
We had a symbol for Minerva
Gryffindor, which was either true

01:38:53.120 --> 01:38:55.580
if Minerva was in Gryffindor,
and false otherwise.

01:38:55.580 --> 01:38:58.310
And likewise, for Minerva
Hufflepuff, and Minerva Ravenclaw,

01:38:58.310 --> 01:39:01.230
and Minerva Slytherin, and so forth.

01:39:01.230 --> 01:39:03.170
But this was starting
to get quite redundant.

01:39:03.170 --> 01:39:05.150
That we wanted some way
to be able to express

01:39:05.150 --> 01:39:07.817
that there's a relationship between
these propositional symbols.

01:39:07.817 --> 01:39:09.725
That Minerva shows up in all of them.

01:39:09.725 --> 01:39:11.600
And also, I would have
liked to have not have

01:39:11.600 --> 01:39:14.270
had so many different
symbols to represent

01:39:14.270 --> 01:39:17.718
what really was a fairly
straightforward problem.

01:39:17.718 --> 01:39:19.760
So first order logic will
give us a different way

01:39:19.760 --> 01:39:21.890
of trying to deal with
this idea by giving us

01:39:21.890 --> 01:39:23.810
two different types of symbols.

01:39:23.810 --> 01:39:27.320
We're going to have constant symbols
that are going to represent objects,

01:39:27.320 --> 01:39:29.150
like people or houses.

01:39:29.150 --> 01:39:31.730
And then predicate
symbols, which you can

01:39:31.730 --> 01:39:35.870
think of as relations or functions,
that take an input and evaluate them to,

01:39:35.870 --> 01:39:37.520
like, true or false, for example.

01:39:37.520 --> 01:39:41.720
That tell us whether or not
some property of some constant,

01:39:41.720 --> 01:39:45.358
or some pair of constants, or
multiple constants, actually holds.

01:39:45.358 --> 01:39:47.400
So we'll see an example
of that in just a moment.

01:39:47.400 --> 01:39:52.302
But for now, in this same problem,
our constant symbols might be objects.

01:39:52.302 --> 01:39:53.510
Things like people or houses.

01:39:53.510 --> 01:39:55.820
So Minerva, Pomona, Horace, Gildaroy.

01:39:55.820 --> 01:39:57.740
Those are all constant symbols.

01:39:57.740 --> 01:39:58.820
As are my four houses--

01:39:58.820 --> 01:40:02.300
Gryffindor, Hufflepuff,
Ravenclaw, and Slytherin.

01:40:02.300 --> 01:40:04.670
Predicates, meanwhile,
these predicate symbols

01:40:04.670 --> 01:40:08.180
are going to be properties
that might hold true or false

01:40:08.180 --> 01:40:10.400
of these individual constants.

01:40:10.400 --> 01:40:14.990
So person might hold true of Minerva,
but it would be false for Gryffindor,

01:40:14.990 --> 01:40:16.610
because Gryffindor is not a person.

01:40:16.610 --> 01:40:19.580
And house is going to
hold true for Ravenclaw,

01:40:19.580 --> 01:40:21.920
but it's not going to hold
true for Horace, for example,

01:40:21.920 --> 01:40:24.110
because Horace is a person.

01:40:24.110 --> 01:40:27.740
And belongs, meanwhile, is going
to be some relation that is

01:40:27.740 --> 01:40:30.560
going to relate people to their houses.

01:40:30.560 --> 01:40:34.760
And it's going to only tell me when
someone belongs to a house or does not.

01:40:34.760 --> 01:40:39.380
So let's take a look at some examples
of what a sentence in first order logic

01:40:39.380 --> 01:40:40.662
might actually look like.

01:40:40.662 --> 01:40:42.620
A sentence might look
like something like this.

01:40:42.620 --> 01:40:46.010
Person Minerva, with
Minerva in parentheses.

01:40:46.010 --> 01:40:50.180
And person being a predicate symbol,
Minerva being a constant symbol.

01:40:50.180 --> 01:40:55.010
This sentence in first order logic
effectively means Minerva is a person,

01:40:55.010 --> 01:40:58.808
or the person property
applies to the Minerva object.

01:40:58.808 --> 01:41:01.100
So if I want to say something
like Minerva is a person,

01:41:01.100 --> 01:41:05.090
here is how I express that
idea using first order logic.

01:41:05.090 --> 01:41:08.000
Meanwhile, I can say something
like house Gryffindor

01:41:08.000 --> 01:41:11.630
to, likewise, express the idea
that Gryffindor is a house.

01:41:11.630 --> 01:41:13.070
I can do that this way.

01:41:13.070 --> 01:41:16.643
And all of the same logical connectives
that we saw in propositional logic,

01:41:16.643 --> 01:41:18.060
those are going to work here, too.

01:41:18.060 --> 01:41:21.050
So and, or, implication,
biconditional, not.

01:41:21.050 --> 01:41:25.220
In fact, I can use not to say
something like, not house Minerva.

01:41:25.220 --> 01:41:29.330
And this sentence in first order
logic means something like Minerva

01:41:29.330 --> 01:41:30.350
is not a house.

01:41:30.350 --> 01:41:35.897
It is not true that the house
property applies to Minerva.

01:41:35.897 --> 01:41:38.480
Meanwhile, in addition to some
of these predicate symbols that

01:41:38.480 --> 01:41:41.210
just take a single argument,
some of our predicate symbols

01:41:41.210 --> 01:41:43.580
are going to express binary relations.

01:41:43.580 --> 01:41:46.500
Relations between two of its arguments.

01:41:46.500 --> 01:41:50.030
So I could say something like,
belongs to, and then two inputs,

01:41:50.030 --> 01:41:53.480
Minerva and Gryffindor
to express the idea

01:41:53.480 --> 01:41:56.200
that Minerva belongs to Gryffindor.

01:41:56.200 --> 01:41:59.210
And so now here's the key difference,
or one of the key differences,

01:41:59.210 --> 01:42:01.220
between this and propositional logic.

01:42:01.220 --> 01:42:04.940
In propositional logic, I needed
one symbol for Minerva Gryffindor,

01:42:04.940 --> 01:42:07.580
and one symbol for Minerva
Hufflepuff, and one symbol

01:42:07.580 --> 01:42:10.670
for all the other people's
Gryffindor and Hufflepuff variables.

01:42:10.670 --> 01:42:14.840
In this case, I just need one
symbol for each of my people,

01:42:14.840 --> 01:42:17.870
and one symbol for each
of my houses, and then I

01:42:17.870 --> 01:42:21.230
can express, as a predicate,
something like, belongs to,

01:42:21.230 --> 01:42:24.980
and say, belongs to Minerva
Gryffindor to express the idea

01:42:24.980 --> 01:42:27.740
that Minerva belongs
to Gryffindor house.

01:42:27.740 --> 01:42:30.080
So already we can see
that first order logic

01:42:30.080 --> 01:42:35.030
is quite expressive in being able to
express these sorts of sentences using

01:42:35.030 --> 01:42:37.430
the existing constant
symbols and predicates that

01:42:37.430 --> 01:42:40.550
already exist, while minimizing
the number of new symbols

01:42:40.550 --> 01:42:41.520
that I need to create.

01:42:41.520 --> 01:42:45.560
I can just use eight symbols
for people, for houses, instead

01:42:45.560 --> 01:42:50.360
of 16 symbols for every
possible combination of each.

01:42:50.360 --> 01:42:53.300
But first order logic gives us
a couple of additional features

01:42:53.300 --> 01:42:56.300
that we can use to express
even more complex ideas.

01:42:56.300 --> 01:43:00.470
And these additional features are
generally known as quantifiers.

01:43:00.470 --> 01:43:03.110
And there are two main
quantifiers in first order logic.

01:43:03.110 --> 01:43:05.930
The first of which is
universal quantification.

01:43:05.930 --> 01:43:09.110
Universal quantification
lets me express an idea,

01:43:09.110 --> 01:43:13.300
like something is going to be
true for all values of a variable.

01:43:13.300 --> 01:43:17.970
Like for all values of x, some
statement is going to hold true.

01:43:17.970 --> 01:43:20.900
So what might a sentence in
universal quantification look like?

01:43:20.900 --> 01:43:25.370
Well, we're going to use this
upside-down A to mean for all.

01:43:25.370 --> 01:43:31.080
So upside-down Ax means for all
values of x, where x is any object,

01:43:31.080 --> 01:43:33.140
this is going to hold true.

01:43:33.140 --> 01:43:41.120
Belongs to x Gryffindor implies
not belongs to x Hufflepuff.

01:43:41.120 --> 01:43:42.470
So let's try and parse this out.

01:43:42.470 --> 01:43:46.790
This means that for all values
of x, If this holds true,

01:43:46.790 --> 01:43:51.200
if x belongs to Gryffindor,
then this does not hold true.

01:43:51.200 --> 01:43:54.500
X does not belong to Hufflepuff.

01:43:54.500 --> 01:43:56.930
So translated into
English, this sentence

01:43:56.930 --> 01:44:01.610
is saying something like, for all
objects x, if x belongs to Gryffindor,

01:44:01.610 --> 01:44:05.090
then x does not belong to
Hufflepuff, for example.

01:44:05.090 --> 01:44:09.530
Or phrased even more simply, anyone
in Gryffindor is not a Hufflepuff.

01:44:09.530 --> 01:44:12.360
A simplified way of
saying the same thing.

01:44:12.360 --> 01:44:15.620
So this universal quantification
lets us express an idea,

01:44:15.620 --> 01:44:20.750
like something is going to hold true
for all values of a particular variable.

01:44:20.750 --> 01:44:23.270
In addition to universal
quantification, though, we also

01:44:23.270 --> 01:44:26.240
have existential quantification.

01:44:26.240 --> 01:44:28.730
Whereas universal quantification
said that something

01:44:28.730 --> 01:44:31.640
is going to be true for
all values of variable,

01:44:31.640 --> 01:44:34.700
existential quantification
says that some expression

01:44:34.700 --> 01:44:37.910
is going to be true for
some value of a variable.

01:44:37.910 --> 01:44:40.980
At least one value of the variable.

01:44:40.980 --> 01:44:43.070
So let's take a look at
a sample sentence using

01:44:43.070 --> 01:44:44.870
existential quantification.

01:44:44.870 --> 01:44:46.890
One such sentence looks like this.

01:44:46.890 --> 01:44:50.760
There exists an x-- this
backwards E stands for exists.

01:44:50.760 --> 01:44:54.980
And here we're saying there
exists an x, such that house x

01:44:54.980 --> 01:44:57.680
and belongs to Minerva x.

01:44:57.680 --> 01:45:01.760
In other words, there exists some
object x, where x is a house,

01:45:01.760 --> 01:45:04.790
and Minerva belongs to x.

01:45:04.790 --> 01:45:07.970
Or phrased a little more succinctly
in English, you're just saying,

01:45:07.970 --> 01:45:09.710
Minerva belongs to a house.

01:45:09.710 --> 01:45:14.600
There's some object that is a house,
and Minerva belongs to a house.

01:45:14.600 --> 01:45:17.600
And combining this universal
and existential quantification,

01:45:17.600 --> 01:45:20.570
we can create far more
sophisticated logical statements

01:45:20.570 --> 01:45:23.630
than we were able to just
using propositional logic.

01:45:23.630 --> 01:45:26.150
I could combine these to
say something like this.

01:45:26.150 --> 01:45:33.170
For all x, person x implies there
exists a y, such that house y

01:45:33.170 --> 01:45:35.525
and belongs to xy.

01:45:35.525 --> 01:45:36.900
So a lot of stuff going on there.

01:45:36.900 --> 01:45:37.910
A lot of symbols.

01:45:37.910 --> 01:45:40.610
Let's try and parse it out and
just understand what it's saying.

01:45:40.610 --> 01:45:47.400
Here we're saying that for all values of
x, if x is a person, then this is true.

01:45:47.400 --> 01:45:49.940
So in other words, I'm
saying for all people,

01:45:49.940 --> 01:45:53.270
and we call that person x, this
statement is going to be true.

01:45:53.270 --> 01:45:55.100
What statement is true of all people?

01:45:55.100 --> 01:46:00.050
Well, there exists a y that is the
house, so there exists some house,

01:46:00.050 --> 01:46:03.050
and x belongs to y.

01:46:03.050 --> 01:46:05.840
In other words I'm saying,
that for all people out there,

01:46:05.840 --> 01:46:11.760
there exists some house, such that x,
the person, belongs to y, the house.

01:46:11.760 --> 01:46:15.830
So say it more succinctly, I'm saying
that every person belongs to a house.

01:46:15.830 --> 01:46:21.470
That for all x, if x is a person, then
there exists a house that x belongs to.

01:46:21.470 --> 01:46:25.030
And so we can now express a lot more
powerful ideas using this idea now

01:46:25.030 --> 01:46:26.030
of first order logic.

01:46:26.030 --> 01:46:28.655
And it turns out there are many
other kinds of logic out there.

01:46:28.655 --> 01:46:31.820
There's second order logic and other
higher order logic, each of which

01:46:31.820 --> 01:46:35.000
allows us to express more
and more complex ideas.

01:46:35.000 --> 01:46:38.630
But all of it, in this case, is really
in pursuit of the same goal, which

01:46:38.630 --> 01:46:40.550
is the representation of knowledge.

01:46:40.550 --> 01:46:44.060
We want our AI agents to be
able to know information,

01:46:44.060 --> 01:46:46.160
to represent that
information, whether that's

01:46:46.160 --> 01:46:49.730
using propositional logic, or first
order logic, or some other logic.

01:46:49.730 --> 01:46:51.680
And then be able to
reason based on that.

01:46:51.680 --> 01:46:53.360
To be able to draw conclusions.

01:46:53.360 --> 01:46:54.230
Make inferences.

01:46:54.230 --> 01:46:57.080
Figure out whether there's some
sort of entailment relationship,

01:46:57.080 --> 01:46:59.780
as by using some sort
of inference algorithm.

01:46:59.780 --> 01:47:02.772
Something like inference by
resolution, or model checking,

01:47:02.772 --> 01:47:04.730
or any number of these
other algorithms that we

01:47:04.730 --> 01:47:07.700
can use in order to take
information that we know

01:47:07.700 --> 01:47:10.280
and translate it to
additional conclusions.

01:47:10.280 --> 01:47:13.040
So all of this has
helped us to create AI

01:47:13.040 --> 01:47:15.980
that is able to represent
information about what it knows

01:47:15.980 --> 01:47:17.860
and what it doesn't know.

01:47:17.860 --> 01:47:19.610
Next time though, we'll
take a look at how

01:47:19.610 --> 01:47:23.150
we can make our AI even more powerful
by not just encoding information

01:47:23.150 --> 01:47:26.690
that we know for sure to be true,
and not to be true, but also,

01:47:26.690 --> 01:47:28.110
to take a look at uncertainty.

01:47:28.110 --> 01:47:31.550
To look at what happens if AI thinks
that something might be probable,

01:47:31.550 --> 01:47:35.810
or maybe not very probable, or
somewhere in between those two extremes,

01:47:35.810 --> 01:47:40.310
all in the pursuit of trying to build
our intelligent systems to be even more

01:47:40.310 --> 01:47:41.180
intelligent.

01:47:41.180 --> 01:47:43.210
We'll see you next time.