Let's take a closer look at what it means for a system of knowledge with a bunch of
rules to be able to answer a query Q using the process of resolution.
We want to know, in other words, whether, Given this system of rules, which could
have a lot of facts and a lot of rules, one can actually infer through logical
entailment, some way of fulfilling this query.
Now this query might consist of unknown variables such as X and USA, and the
relationship being, is leader of, so K implies Q means finding out ways to assign
variables to all the unknowns in this query, so that it actually turns out to be
true given all the knowledge in your knowledge base.
So resolution involves, as we have seen before, both entailment, which is logical
inference. As well as unification, which is replacing
any variables in the query by actual values.
Now, remember again that. A statement like K implies Q is exactly
the same thing as saying that, not K or Q is true.
We went through this in a little bit of detail awhile back.
Please convince yourself that whether or not K is one statement or 100s.
K implies Q is still the same as saying, that not K that means the negation of all
this statements and the knowledge base. Or Q, this compound statement is true.
To see that. If k, is, false, then not k is true.
And if k is true, then not k is false. And if not k is false, then Q must be
true, in order for this to be true. The next important step is to see that not
k or q being true is the same thing as k and not q being false.
Try to convince yourself that negating compound statement which is the ore of two
statements is the same thing as taking the end of the negation of both of these
statements. An easy way to see that is that if check
all possible values of K and Q. There are four combinations, true, true,
true false, false true, and make sure that in each case, not K or Q being true is the
same thing as K and not Q being false. We won't go through that in detail.
I'll leave it to you to work that out yourself.
Now let us see that in order to prove Q rather to show that K implies Q all we
need to do is show that K and not Q is false.
So what do we do? We augment the set of, rules and knowledge
that we have, with not Q. That means if we had a statement that.
Is leader of X comma Obama, is my query. I will augment my knowledge base with the
statement that it is not true is leader of Xx comma Obama.
The augmented, knowledge base which is, our original knowledge, and not q, must,
give me a falsehood, if, I was to prove, k in place q.
So in order to, show this, when needs to take this augmented knowledge base, and
crank it through some logical resolution engine which performs both inference and
unification that is assigning values to variables.
And figure out whether or not it answers true or false.
If it answers false, that is that K and not Q results in a falsity, then the
answer to my query is true. K does imply Q as per this argument
earlier. Along the way, we would also have figured
out the right values for any missing variables in Q, and, in the process,
answered our query. However, if, k implies q, results, in, a
true statement or a satisfiable statement, then the answer to the query would be no.
Because then k and not q would be true. Which means that, not K or Q is false, or
K implies Q would be false. This seems fairly straight forward, all we
need to do is take our query, even if it contains variables, negate it, and then
state its opposite added to our bunch of knowledge, crank it through some
mechanical process or resolution and unification, however difficult that may
be. And see whether the answer comes out false
or true, and then we have the answer to our query, along with any variable
assignments which would make sure that we get the right answer.
The trouble is. This resolution procedure.
May not actually ever finish. It may go on forever.
That's actually possible. In which case we get into some trouble.
Resolution need not always work. And the meaning of not working is that it
never stops. This brings us to some very important
understanding of the fundamental limits of logic and resolution.
First of all resolution may never end and by never we mean never.
Whatever algorithm might weigh, you may, you might use to perform a resolution,
it's not an issue that one algorithm is bad but it may be the case that resolution
could never end and in fact this is the concept of undecidability.
There are some cases where you have a bunch of knowledge.
A bunch of rules and facts, and you could never tell whether or not that combination
of rules and facts is true or false. In, in other words they are undecidable.
This was actually. Shown, for the case of predicate logic,
that means the logic that we've been studying, by a number of people in the
early twentieth century. Kurt Godel, Alan Turing, of course, who
was the founder of computer science, Church, and a few others, in a variety of
different ways. Turing showed it in the most elegant way
for a computer science perspective by using the concept of a Turing machine.
But that's a subject for theoretical computer science and we won't go into that
in this course. The other trouble is that even in
situations where. The resolution process does come to a
conclusion, it might take a lot of time. For example, for N facts with N variables,
one might have. An algorithm which took two to the n, m
time. That means exponential.
We've seen this before, algorithms which take, extremely large number of steps,
such as figuring out all the possible combinations of ones and zeros in a large,
thousand bit vector, takes two to the n steps.
Similarly. Logical resolution might take two to the
something number of steps, which makes it really intractable in practice for a large
number of facts. It turns out that if you have just
propositions, that means no variables, the old, the what we just did a few with just
statements like Obama is president of U.S.A.
Rather than relationships between entities and other entities.
Such propositions alone. Is, do, do result in decidable logic.
That means you can't always find the end to a resolution procedure.
But it still might not be tractable in the sense that it might take too long.
And that comes up to the whole theory of computational intractability with the
notion of NP completeness. And the first such problem to be shown to
be provably difficult, in this sense, was that of satisfiability, which was nothing
but whether or not a statement of propositions could actually be satisfied.
The point about covering some of these important results in logic and its
undecidability and computational complexity and intractability is not that
they are critical for web intelligence but just to remind us that if you have a
vision such as semantic web where we would like to have automated reasoning and web
scale. Then we will probably come across some of
these issues during certain exercise because we'll have lots of facts, lots of
rules, we'll be relying on predicate logic, resolution procedures, which may
not complete, ever. Only when if they do they may be
interactable in that they could take lots and lots of time, to be effectively,
undoable. So what, what, what do we do.
It turns out, fortunately, that. Some kinds of logic's specifically those
designed for the semantic web languages such as owl dl, which stands for owl
description logic and owl light which is even simpler version of this logic.
Essentially are decidable. That means they will always complete their
resolution process. Description logics, in all light,
essentially encode the notions of, sex. So that we can write down, logically, a
statement that a leader means that, that person that is also a person.
Our faculty member is also an employee or things like that so essentially statements
about the structure of the world are encodable in this description logics which
is decidable doesn't suffer from this problem of undecidability.
In it's worst case, it's still intractable.
Though in most practical cases, the other some procedures do complete in reasonable
time. The other piece that is used is something
called horn logic, which is essentially rules, such as if there was a person and
the person is born in a country C that implies that person is citizen of that
country. A rule like this is called a statement of
horn logic if there is only one conclusion on the right hand side.
If it was, say, a person that's born in C, that's a citizen of C, as well as a few
other things, then that's not a horn logic statement.
Such statements in horn logic. Are tractable.
They will always complete very fast, but if they do.
But in some situations, they may actually go on forever.
There are ways of fixing Horn logic by with some caveats, which we won't go into
in detail, to make it actually desirable and tractable.
So, in practice, what one does is for a semantic web-like system.
One relies on description logics to deal with the structure of the world.
That we describe what the elements in the world actually look like, how they relate
to each other. And then rely on Horn logic to encode the
rules. The reason one does this is, is that the
structure of the world is likely to be, reasonably small.
And not necessarily lead to some of the intractable situations.
Whereas the number of rules one may have may be extremely large, so one needs to
rely on something which is provably tractable.
Anyway, we are not gonna cover either the resolution procedures in detail nor any of
the fundamental limits of logic in this course.
Because what we'll find very soon is that normal logical resolution, whether it's
decidable or not, infactable or not. Is not necessarily the.
Best way to deal with the real world. And that's one of the reasons why the
semantic web, web vision has sort of floundered in the past decade.
And the reason is uncertainty. Regardless of.
The fundamental limits of logic. The real challenge that logical inferences
faced in trying to deal with large volumes of facts that could be inferred from the
web, is none of these are necessarily true or false.
They are true with a certain probability. And that actually causes much more
fundamental problems than some of these fundamental limits.
Let's see how.