All language subtitles for 11-Lecture 1 Segment 11 What can AI do Logic.en

What about that other classic AI stuff?
We talked about theorem proving,

can we prove mathematical theorems.
That stuff is happening too and it's also important.

So, on the logic front for
example we can build amazing theorem provers

compared to when people started
doing this. These provers are used for

more than just proving theorems. For
example, NASA uses these for fault diagnosis.

There are some question
answering systems which are no longer

purely logical, but there is a
component of logical theorem proving. You try to

prove that the statement

that you think answers the question
actually entails the question in the appropriate way.

That's the way that logic and theorem proving
has made its way into very different

domains like natural language processing.
The methods people use are things like

deduction systems. The closest we'll get
to this in this class is constraint satisfaction,

but you'll get a flavor for how this stuff works.

Also it's worth pointing out that
satisfiability solvers have had

huge advances in the past decade and are now
able to do really amazing things.

What's shown here on the right is a proof of something called the Robbin's conjecture.

You probably

haven't heard the Robbin's conjecture
itself, but it was an open algebraic question,

and there is a short, human
interpretable proof

that a theorem prover chugged out that humans have been looking for for a while. This is a case of

you see it, and you're like, yeah, that's right.

That's a case of an open question
being proved by a computer in the way

humans would prove it, in the sense that
the human can interpret the proof.

There's also theorem proving by computers where
the computer does a brute force,

where human doesn't want to check 4.7 billion cases, but the computer does,

and so the computer does it.