1
00:00:00,000 --> 00:00:08,718
Let's take a closer look at what it means
for a system of knowledge with a bunch of

2
00:00:08,718 --> 00:00:15,880
rules to be able to answer a query Q using
the process of resolution.

3
00:00:16,220 --> 00:00:23,539
We want to know, in other words, whether,
Given this system of rules, which could

4
00:00:23,539 --> 00:00:31,717
have a lot of facts and a lot of rules,
one can actually infer through logical

5
00:00:31,717 --> 00:00:36,435
entailment, some way of fulfilling this
query.

6
00:00:36,435 --> 00:00:44,404
Now this query might consist of unknown
variables such as X and USA, and the

7
00:00:44,404 --> 00:00:53,766
relationship being, is leader of, so K
implies Q means finding out ways to assign

8
00:00:53,766 --> 00:01:01,617
variables to all the unknowns in this
query, so that it actually turns out to be

9
00:01:01,617 --> 00:01:06,720
true given all the knowledge in your
knowledge base.

10
00:01:08,740 --> 00:01:15,692
So resolution involves, as we have seen
before, both entailment, which is logical

11
00:01:15,692 --> 00:01:20,268
inference.
As well as unification, which is replacing

12
00:01:20,268 --> 00:01:24,140
any variables in the query by actual
values.

13
00:01:25,740 --> 00:01:35,216
Now, remember again that.
A statement like K implies Q is exactly

14
00:01:35,216 --> 00:01:41,680
the same thing as saying that, not K or Q
is true.

15
00:01:42,780 --> 00:01:48,696
We went through this in a little bit of
detail awhile back.

16
00:01:48,696 --> 00:01:55,916
Please convince yourself that whether or
not K is one statement or 100s.

17
00:01:55,916 --> 00:02:04,138
K implies Q is still the same as saying,
that not K that means the negation of all

18
00:02:04,138 --> 00:02:11,760
this statements and the knowledge base.
Or Q, this compound statement is true.

19
00:02:12,140 --> 00:02:18,569
To see that.
If k, is, false, then not k is true.

20
00:02:18,569 --> 00:02:26,799
And if k is true, then not k is false.
And if not k is false, then Q must be

21
00:02:26,799 --> 00:02:38,444
true, in order for this to be true.
The next important step is to see that not

22
00:02:38,444 --> 00:02:47,360
k or q being true is the same thing as k
and not q being false.

23
00:02:47,740 --> 00:02:57,504
Try to convince yourself that negating
compound statement which is the ore of two

24
00:02:57,504 --> 00:03:06,695
statements is the same thing as taking the
end of the negation of both of these

25
00:03:06,695 --> 00:03:13,148
statements.
An easy way to see that is that if check

26
00:03:13,148 --> 00:03:20,612
all possible values of K and Q.
There are four combinations, true, true,

27
00:03:20,612 --> 00:03:29,589
true false, false true, and make sure that
in each case, not K or Q being true is the

28
00:03:29,589 --> 00:03:36,584
same thing as K and not Q being false.
We won't go through that in detail.

29
00:03:36,584 --> 00:03:39,680
I'll leave it to you to work that out
yourself.

30
00:03:40,540 --> 00:03:50,648
Now let us see that in order to prove Q
rather to show that K implies Q all we

31
00:03:50,648 --> 00:03:56,480
need to do is show that K and not Q is
false.

32
00:03:56,800 --> 00:04:02,738
So what do we do?
We augment the set of, rules and knowledge

33
00:04:02,738 --> 00:04:09,180
that we have, with not Q.
That means if we had a statement that.

34
00:04:09,520 --> 00:04:17,647
Is leader of X comma Obama, is my query.
I will augment my knowledge base with the

35
00:04:17,647 --> 00:04:25,520
statement that it is not true is leader of
Xx comma Obama.

36
00:04:26,920 --> 00:04:36,117
The augmented, knowledge base which is,
our original knowledge, and not q, must,

37
00:04:36,117 --> 00:04:42,169
give me a falsehood, if, I was to prove, k
in place q.

38
00:04:42,169 --> 00:04:49,829
So in order to, show this, when needs to
take this augmented knowledge base, and

39
00:04:49,829 --> 00:04:56,714
crank it through some logical resolution
engine which performs both inference and

40
00:04:56,714 --> 00:05:00,912
unification that is assigning values to
variables.

41
00:05:00,912 --> 00:05:05,530
And figure out whether or not it answers
true or false.

42
00:05:05,530 --> 00:05:13,752
If it answers false, that is that K and
not Q results in a falsity, then the

43
00:05:13,752 --> 00:05:20,660
answer to my query is true.
K does imply Q as per this argument

44
00:05:20,660 --> 00:05:26,032
earlier.
Along the way, we would also have figured

45
00:05:26,032 --> 00:05:33,816
out the right values for any missing
variables in Q, and, in the process,

46
00:05:33,816 --> 00:05:40,693
answered our query.
However, if, k implies q, results, in, a

47
00:05:40,693 --> 00:05:48,793
true statement or a satisfiable statement,
then the answer to the query would be no.

48
00:05:48,793 --> 00:05:57,384
Because then k and not q would be true.
Which means that, not K or Q is false, or

49
00:05:57,384 --> 00:06:03,767
K implies Q would be false.
This seems fairly straight forward, all we

50
00:06:03,767 --> 00:06:08,720
need to do is take our query, even if it
contains variables, negate it, and then

51
00:06:08,720 --> 00:06:13,356
state its opposite added to our bunch of
knowledge, crank it through some

52
00:06:13,356 --> 00:06:18,182
mechanical process or resolution and
unification, however difficult that may

53
00:06:18,182 --> 00:06:21,103
be.
And see whether the answer comes out false

54
00:06:21,103 --> 00:06:25,739
or true, and then we have the answer to
our query, along with any variable

55
00:06:25,739 --> 00:06:29,740
assignments which would make sure that we
get the right answer.

56
00:06:31,160 --> 00:06:36,400
The trouble is.
This resolution procedure.

57
00:06:37,200 --> 00:06:42,480
May not actually ever finish.
It may go on forever.

58
00:06:43,340 --> 00:06:48,940
That's actually possible.
In which case we get into some trouble.

59
00:06:49,320 --> 00:06:57,334
Resolution need not always work.
And the meaning of not working is that it

60
00:06:57,334 --> 00:07:02,748
never stops.
This brings us to some very important

61
00:07:02,748 --> 00:07:09,680
understanding of the fundamental limits of
logic and resolution.

62
00:07:10,420 --> 00:07:16,088
First of all resolution may never end and
by never we mean never.

63
00:07:16,088 --> 00:07:22,804
Whatever algorithm might weigh, you may,
you might use to perform a resolution,

64
00:07:22,804 --> 00:07:30,042
it's not an issue that one algorithm is
bad but it may be the case that resolution

65
00:07:30,042 --> 00:07:35,798
could never end and in fact this is the
concept of undecidability.

66
00:07:35,798 --> 00:07:40,770
There are some cases where you have a
bunch of knowledge.

67
00:07:40,770 --> 00:07:48,407
A bunch of rules and facts, and you could
never tell whether or not that combination

68
00:07:48,407 --> 00:07:55,410
of rules and facts is true or false.
In, in other words they are undecidable.

69
00:07:55,410 --> 00:08:00,320
This was actually.
Shown, for the case of predicate logic,

70
00:08:00,320 --> 00:08:06,026
that means the logic that we've been
studying, by a number of people in the

71
00:08:06,026 --> 00:08:10,667
early twentieth century.
Kurt Godel, Alan Turing, of course, who

72
00:08:10,667 --> 00:08:16,448
was the founder of computer science,
Church, and a few others, in a variety of

73
00:08:16,448 --> 00:08:20,707
different ways.
Turing showed it in the most elegant way

74
00:08:20,936 --> 00:08:26,715
for a computer science perspective by
using the concept of a Turing machine.

75
00:08:26,715 --> 00:08:32,799
But that's a subject for theoretical
computer science and we won't go into that

76
00:08:32,799 --> 00:08:38,806
in this course.
The other trouble is that even in

77
00:08:38,806 --> 00:08:45,022
situations where.
The resolution process does come to a

78
00:08:45,022 --> 00:08:53,744
conclusion, it might take a lot of time.
For example, for N facts with N variables,

79
00:08:53,744 --> 00:08:59,381
one might have.
An algorithm which took two to the n, m

80
00:08:59,381 --> 00:09:01,995
time.
That means exponential.

81
00:09:01,995 --> 00:09:09,465
We've seen this before, algorithms which
take, extremely large number of steps,

82
00:09:09,465 --> 00:09:16,934
such as figuring out all the possible
combinations of ones and zeros in a large,

83
00:09:16,934 --> 00:09:21,136
thousand bit vector, takes two to the n
steps.

84
00:09:21,416 --> 00:09:25,260
Similarly.
Logical resolution might take two to the

85
00:09:25,260 --> 00:09:31,224
something number of steps, which makes it
really intractable in practice for a large

86
00:09:31,224 --> 00:09:35,532
number of facts.
It turns out that if you have just

87
00:09:35,532 --> 00:09:42,362
propositions, that means no variables, the
old, the what we just did a few with just

88
00:09:42,362 --> 00:09:45,898
statements like Obama is president of
U.S.A.

89
00:09:45,898 --> 00:09:50,880
Rather than relationships between entities
and other entities.

90
00:09:51,780 --> 00:09:58,398
Such propositions alone.
Is, do, do result in decidable logic.

91
00:09:58,398 --> 00:10:03,984
That means you can't always find the end
to a resolution procedure.

92
00:10:03,984 --> 00:10:10,403
But it still might not be tractable in the
sense that it might take too long.

93
00:10:10,403 --> 00:10:17,800
And that comes up to the whole theory of
computational intractability with the

94
00:10:17,800 --> 00:10:24,819
notion of NP completeness.
And the first such problem to be shown to

95
00:10:24,819 --> 00:10:32,203
be provably difficult, in this sense, was
that of satisfiability, which was nothing

96
00:10:32,203 --> 00:10:39,040
but whether or not a statement of
propositions could actually be satisfied.

97
00:10:40,780 --> 00:10:46,202
The point about covering some of these
important results in logic and its

98
00:10:46,202 --> 00:10:51,697
undecidability and computational
complexity and intractability is not that

99
00:10:51,697 --> 00:10:57,925
they are critical for web intelligence but
just to remind us that if you have a

100
00:10:57,925 --> 00:11:04,080
vision such as semantic web where we would
like to have automated reasoning and web

101
00:11:04,080 --> 00:11:07,937
scale.
Then we will probably come across some of

102
00:11:07,937 --> 00:11:14,284
these issues during certain exercise
because we'll have lots of facts, lots of

103
00:11:14,284 --> 00:11:20,305
rules, we'll be relying on predicate
logic, resolution procedures, which may

104
00:11:20,305 --> 00:11:24,634
not complete, ever.
Only when if they do they may be

105
00:11:24,634 --> 00:11:31,578
interactable in that they could take lots
and lots of time, to be effectively,

106
00:11:31,838 --> 00:11:34,980
undoable.
So what, what, what do we do.

107
00:11:35,420 --> 00:11:42,450
It turns out, fortunately, that.
Some kinds of logic's specifically those

108
00:11:42,450 --> 00:11:49,105
designed for the semantic web languages
such as owl dl, which stands for owl

109
00:11:49,105 --> 00:11:55,760
description logic and owl light which is
even simpler version of this logic.

110
00:11:57,020 --> 00:12:03,961
Essentially are decidable.
That means they will always complete their

111
00:12:03,961 --> 00:12:09,092
resolution process.
Description logics, in all light,

112
00:12:09,092 --> 00:12:16,738
essentially encode the notions of, sex.
So that we can write down, logically, a

113
00:12:16,738 --> 00:12:23,680
statement that a leader means that, that
person that is also a person.

114
00:12:23,921 --> 00:12:30,990
Our faculty member is also an employee or
things like that so essentially statements

115
00:12:30,990 --> 00:12:37,418
about the structure of the world are
encodable in this description logics which

116
00:12:37,418 --> 00:12:42,560
is decidable doesn't suffer from this
problem of undecidability.

117
00:12:42,840 --> 00:12:46,118
In it's worst case, it's still
intractable.

118
00:12:46,118 --> 00:12:52,909
Though in most practical cases, the other
some procedures do complete in reasonable

119
00:12:52,909 --> 00:12:58,892
time.
The other piece that is used is something

120
00:12:58,892 --> 00:13:06,776
called horn logic, which is essentially
rules, such as if there was a person and

121
00:13:06,776 --> 00:13:14,562
the person is born in a country C that
implies that person is citizen of that

122
00:13:14,562 --> 00:13:19,552
country.
A rule like this is called a statement of

123
00:13:19,552 --> 00:13:26,140
horn logic if there is only one conclusion
on the right hand side.

124
00:13:26,500 --> 00:13:32,721
If it was, say, a person that's born in C,
that's a citizen of C, as well as a few

125
00:13:32,721 --> 00:13:36,817
other things, then that's not a horn logic
statement.

126
00:13:36,817 --> 00:13:41,082
Such statements in horn logic.
Are tractable.

127
00:13:41,082 --> 00:13:45,680
They will always complete very fast, but
if they do.

128
00:13:45,680 --> 00:13:50,640
But in some situations, they may actually
go on forever.

129
00:13:51,760 --> 00:13:58,136
There are ways of fixing Horn logic by
with some caveats, which we won't go into

130
00:13:58,136 --> 00:14:02,037
in detail, to make it actually desirable
and tractable.

131
00:14:02,037 --> 00:14:06,590
So, in practice, what one does is for a
semantic web-like system.

132
00:14:06,590 --> 00:14:12,261
One relies on description logics to deal
with the structure of the world.

133
00:14:12,261 --> 00:14:18,710
That we describe what the elements in the
world actually look like, how they relate

134
00:14:18,710 --> 00:14:23,061
to each other.
And then rely on Horn logic to encode the

135
00:14:23,061 --> 00:14:26,635
rules.
The reason one does this is, is that the

136
00:14:26,635 --> 00:14:31,220
structure of the world is likely to be,
reasonably small.

137
00:14:31,408 --> 00:14:35,372
And not necessarily lead to some of the
intractable situations.

138
00:14:35,372 --> 00:14:40,405
Whereas the number of rules one may have
may be extremely large, so one needs to

139
00:14:40,405 --> 00:14:43,300
rely on something which is provably
tractable.

140
00:14:43,900 --> 00:14:51,585
Anyway, we are not gonna cover either the
resolution procedures in detail nor any of

141
00:14:51,585 --> 00:14:55,886
the fundamental limits of logic in this
course.

142
00:14:55,886 --> 00:15:03,297
Because what we'll find very soon is that
normal logical resolution, whether it's

143
00:15:03,297 --> 00:15:10,580
decidable or not, infactable or not.
Is not necessarily the.

144
00:15:11,180 --> 00:15:17,851
Best way to deal with the real world.
And that's one of the reasons why the

145
00:15:17,851 --> 00:15:23,082
semantic web, web vision has sort of
floundered in the past decade.

146
00:15:23,082 --> 00:15:27,940
And the reason is uncertainty.
Regardless of.

147
00:15:28,620 --> 00:15:34,899
The fundamental limits of logic.
The real challenge that logical inferences

148
00:15:34,899 --> 00:15:41,933
faced in trying to deal with large volumes
of facts that could be inferred from the

149
00:15:41,933 --> 00:15:46,203
web, is none of these are necessarily true
or false.

150
00:15:46,203 --> 00:15:52,567
They are true with a certain probability.
And that actually causes much more

151
00:15:52,567 --> 00:15:57,507
fundamental problems than some of these
fundamental limits.

152
00:15:57,507 --> 00:15:58,680
Let's see how.