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.