1
00:00:00,000 --> 00:00:04,722
Hello. In this video, I'm going to give a
demo of the [inaudible]; a research
2
00:00:04,722 --> 00:00:09,948
project in Stanford University for helping
students learn formal systems in online
3
00:00:09,948 --> 00:00:14,670
classes. The basic idea behind the
[inaudible] is to allow students to work
4
00:00:14,670 --> 00:00:19,833
through formal derivations and to have
their improving technology that will check
5
00:00:19,833 --> 00:00:24,870
that those derivations are correct. So you
can actually learn the details of how
6
00:00:24,870 --> 00:00:29,655
formal reasoning works. So let's take a
look at an example here. So here is a
7
00:00:29,655 --> 00:00:34,727
little exercise in algebra and our goal is
to prove that [inaudible]. Is equal to
8
00:00:34,727 --> 00:00:39,454
eleven, all right? That's what we're
trying to accomplish and where we start is
9
00:00:39,454 --> 00:00:43,999
with the equation two x + -four = x +
seven. So in general, there could be more
10
00:00:43,999 --> 00:00:49,211
than one initial given assumption in this
particular exercise so it's just one and
11
00:00:49,211 --> 00:00:54,121
we wanna start with that equation and we
want to prove that x = eleven. And to get
12
00:00:54,121 --> 00:00:58,605
there, we're allowed to use any of the
rules that are listed here that I'm
13
00:00:58,605 --> 00:01:03,514
circling with the mouse. And these were
also divided into two kinds. There are the
14
00:01:03,514 --> 00:01:08,193
required rules which is this first set
here at the top. And, the required rules
15
00:01:08,193 --> 00:01:12,140
are required. So, whenever we have a step
of [inaudible] that uses one of these
16
00:01:12,140 --> 00:01:16,086
rules, we have to name it explicitly, we
have to show that stuff explicitly. And
17
00:01:16,086 --> 00:01:19,830
then there are some rules that are
considered free. These are the rules we
18
00:01:19,830 --> 00:01:23,625
don't have to show. So for example, we
don't have to show all these steps
19
00:01:23,625 --> 00:01:27,774
involving associatively of addition and
multiplication, presumably our instructors
20
00:01:27,774 --> 00:01:32,074
decide we are already understand that and
we're allowed to skip over those steps and
21
00:01:32,074 --> 00:01:36,122
the system will try to fill them in. So
these rules out here we can show them if
22
00:01:36,122 --> 00:01:40,169
we like, but they're not required. We're
allowed to skip these steps. All right, so
23
00:01:40,169 --> 00:01:45,967
let's begin with. On this and every step
of the derivation is going to have three
24
00:01:45,967 --> 00:01:50,835
parts. It's gonna have a conclusion. So
something that we, we are proving at this
25
00:01:50,835 --> 00:01:55,904
particular stuff and we're gonna have the
justification. So the rule from which that
26
00:01:55,904 --> 00:02:00,612
step follows. And then finally, what
previous facts we're using that we already
27
00:02:00,612 --> 00:02:05,379
knew to be true. All right, So why, what
we started with, what rule we apply to it
28
00:02:05,379 --> 00:02:10,207
and then what we concluded from it? All
right? So, what can we do to make progress
29
00:02:10,207 --> 00:02:15,216
in this example? Well, one thing we could
do is we can add four to both sides of the
30
00:02:15,216 --> 00:02:20,417
equation. Okay. And why is that justified?
What rule are we using? Well, that's the
31
00:02:20,417 --> 00:02:25,873
balance equation using addition rule up
here which says it's okay to add the same
32
00:02:25,873 --> 00:02:31,262
thing both sides of the equation. So, we
would select that rule out of the list of
33
00:02:31,262 --> 00:02:35,987
possible rules. Okay. And then what
assumption are we using? Well, there's
34
00:02:35,987 --> 00:02:41,110
only one thing that we've got at the
moment. That's the initial given that we
35
00:02:41,110 --> 00:02:46,366
would begin with. All right, So here, we
have one step of our derivation. We think
36
00:02:46,366 --> 00:02:51,817
this is right. We click update proof and
the system. Comes back and says indeed,
37
00:02:51,817 --> 00:02:56,734
yes. That was a valid step of the
derivation. So now, let's do another step.
38
00:02:56,734 --> 00:03:01,266
Well actually, let's see what would happen
here if we did this balance equation step
39
00:03:01,266 --> 00:03:05,474
incorrectly. Let's say we didn't add the
same thing to both sides. And so, let's
40
00:03:05,474 --> 00:03:09,682
try that out and what do we get? Oh, we
see, then now it comes back to color red
41
00:03:09,682 --> 00:03:14,052
indicating there's something wrong and
we're not given another step here to fill
42
00:03:14,052 --> 00:03:18,152
in, okay, because there was an incorrect
step. We also see there's this little
43
00:03:18,152 --> 00:03:22,742
question mark icon here. We can click on
that. And it tells us something about what
44
00:03:22,742 --> 00:03:27,593
went wrong and gives us some advice as it
balancing equation. Means you have to add
45
00:03:27,593 --> 00:03:31,626
the same value to each side of the
equation. Okay. So with that advice,
46
00:03:31,626 --> 00:03:36,360
presumably we will be able to figure out
what we did wrong and correct this step.
47
00:03:36,360 --> 00:03:41,798
And get back to a place where we're on
track. Now as you say there's not always
48
00:03:41,798 --> 00:03:47,443
advice available for every incorrect step
but if it is available, you know you can
49
00:03:47,443 --> 00:03:53,259
click on that and get some idea of what it
is you might have done wrong. All right so
50
00:03:53,259 --> 00:03:58,816
now let's go on. Let's take a look at this
and see what we could do. We can try to
51
00:03:58,816 --> 00:04:04,108
simplify the left hand si de here. So,
that's = two x on the left hand side and
52
00:04:04,108 --> 00:04:09,400
the right hand side x + seven + four and
we think we can do this here because you
53
00:04:09,400 --> 00:04:14,625
know? Four + -four are that's just adding
constants and that's one of our free
54
00:04:14,625 --> 00:04:19,388
rules, okay? So we're allowed to add up
constants, you know? At the end and
55
00:04:19,388 --> 00:04:24,680
getting zero there should be something we
can do for free, all right? And that
56
00:04:24,680 --> 00:04:29,825
follows our previous step. Let me select
that and now we can do an update and it
57
00:04:29,825 --> 00:04:34,582
comes back and it says, oh we did
something wrong so it doesn't immediately
58
00:04:34,582 --> 00:04:39,911
follow from the previous step and there's
actually empty here so we can see why and
59
00:04:39,911 --> 00:04:45,302
we see oh, it says [inaudible] identity is
a required rule and so what mistake did we
60
00:04:45,302 --> 00:04:50,250
make? Well, you know it was okay to add
four and -four together and get zero, I'm
61
00:04:50,250 --> 00:04:55,388
not sure of that because that was, that
was just adding and multiplying constants
62
00:04:55,388 --> 00:04:59,765
but then the sub-sequence step when we
said the twox+0 = twox that it was
63
00:04:59,765 --> 00:05:04,188
something. They were actually required to
show in this exercise. So, whenever we use
64
00:05:04,188 --> 00:05:08,472
that identity we have to explicitly say
so, so we can, we can fix that. By saying
65
00:05:08,472 --> 00:05:13,626
that you know this rule actually, this
step actually, this step actually follows
66
00:05:13,626 --> 00:05:19,106
[inaudible] identity from the previous one
and all the other rules that we're using
67
00:05:19,106 --> 00:05:24,195
that stuff for free so we don't have to
name them, alright. So now we can go on.
68
00:05:24,195 --> 00:05:29,153
We can although simplify the left hand
side. We might have clean that up and
69
00:05:29,153 --> 00:05:34,633
that's just free rules so we don't have to
say exactly which rule we're using and I
70
00:05:34,633 --> 00:05:40,123
think I didn't take the update there,
okay. So now, I guess I hit it twice by
71
00:05:40,123 --> 00:05:47,269
accident so let's just get rid of one of
these steps, okay. So now what's the next
72
00:05:47,269 --> 00:05:55,599
step we're going to perform? It looks like
we need to bring x over to the left hand
73
00:05:55,599 --> 00:06:02,360
side. So, we're going to add a -x to both
sides so two x + -x = x + eleven + -x,
74
00:06:02,360 --> 00:06:08,851
okay? And that's again the balance
equation using addition rule and that
75
00:06:08,851 --> 00:06:15,973
follows from our previous step, okay? And,
we can get from that one, all right? And
76
00:06:15,973 --> 00:06:22,397
then we'll update that, t hat works just
fine. Okay? And now we can do some
77
00:06:22,397 --> 00:06:28,423
simplification of the left hand side,
sorry excuse me, on the right hand side
78
00:06:28,423 --> 00:06:35,083
because all of these over be here is just
= eleven, okay? And, and then we're having
79
00:06:35,083 --> 00:06:41,980
to use x + -x = zero and then we're just
adding eleven and zero so we're just count
80
00:06:41,980 --> 00:06:48,439
this...adding up constants so this should
follow from additive inverse From the
81
00:06:48,439 --> 00:06:53,923
previous step. All right, If we update
that yes that worked out fine and now we
82
00:06:53,923 --> 00:06:59,165
just have to work on the left hand side.
We've got two x + -x and in order to get
83
00:06:59,165 --> 00:07:04,801
that into a form where we can simplify it,
we're gonna need to use the Distributive
84
00:07:04,801 --> 00:07:10,469
Rule. We need to pull out the constants
that are in front of the x's. And so, we
85
00:07:10,469 --> 00:07:15,960
can do that. We can say that two + (-one)
x = eleven. And so, we're using
86
00:07:15,960 --> 00:07:22,516
distributivity there but we're also using
the unary negation rule that says, you
87
00:07:22,516 --> 00:07:28,662
know, -x = -one x. But that's a free
rule so we don't have to worry about that.
88
00:07:28,662 --> 00:07:35,372
So the only rule we need to name is the
distributivity rule. And that falls from
89
00:07:35,372 --> 00:07:41,110
the previous step with the deliberation.
We update that, okay. And now we're just
90
00:07:41,110 --> 00:07:47,211
about there so now I think in one step we
can do the simplification. We can subtract
91
00:07:47,211 --> 00:07:52,732
one from two and get one and then we have
onex = eleven. That's multiplicative
92
00:07:52,732 --> 00:07:58,496
identity which is a required rule for this
flicker exercise. Falls with the previous
93
00:07:58,496 --> 00:08:03,068
step like all the other, like all the
previous steps and now we're done. And
94
00:08:03,068 --> 00:08:07,757
then we prove that x = eleven says who
knows we have finished the assignment and
95
00:08:07,757 --> 00:08:11,977
that is the basic idea behind the
[inaudible]. And, while this particular
96
00:08:11,977 --> 00:08:16,901
example was algebra this can be done for
any kind of formal system where you can
97
00:08:16,901 --> 00:08:21,941
present the kinds of exercises you want to
do in the set of rules and the students
98
00:08:21,941 --> 00:08:25,400
are supposed to derive some kind of goal
using those rules.