And that's essentially all I wanted to, no not quite all, I wanted to say about theorem

proving in first-order logic. You can use theorem proving for first-order logic if you restrict it

sufficiently for programming. You can use it to feed it propositions, theorems of mathematics,

like Colonel West is a criminal given the laws, which is a mathematical theorem. Or things like

every idempotent monoid is a billion, which already sounds like great math, right? And if you just

use all the definitions you're going to get a first-order logic formula, which is something

you could probably prove in five minutes or ten. I would be surprised if anybody can do it much

faster. A contemporary theorem prover can prove this in something like 20 milliseconds. Okay? If

it becomes a little bit more difficult mathematically spoken, so where you need something like 20 minutes

or something like this, then the theorem prover will actually not find a solution. And if you're

extremely extremely extremely lucky it will actually find a solution for an interesting

problem. That has happened I think three times so far and that's over 50 years. But that's

essentially what we call deduction, which is reasoning from true facts to true facts. What

we do in math, we have axioms which we believe to be true and then we come up with true facts. That

is not all we want to do as an agent. An agent has to do other things and I want to basically just

give you something to think. So you all know that when it rains the street is wet. So if you know

when it rains and the street is wet and it rains, then you can deduce from that that a street is wet.

Right? Easy. More disponents in this case. We have that in natural deduction and it's essentially,

if you say rains falls wet street and so on, then you then you have deduction here. It has the good

property that it's monotonic, which means things you've deduced once never become false. But there

are other ways of inference that you actually want to also do. Sometimes you want to infer an

explanation for something you see. So you still know if it rains then the street is wet and you

have the observation that the street is wet. Then an inference procedure called abduction says

probably it rained. Okay? So that's something the the an agent needs very often to explain

observations. Here we don't have monotonicity. Right? More information can mean that the that

explanations actually don't work anymore. For instance, I'm looking outside, obviously the

street is wet and I say, ah, probably the rain. Oh no, the sun is shining. But there's this little

boy that kind of had an emergency. Okay? So knowing more about this little boy and the sun and so on

actually invalidates conclusions you have done earlier. That's called abduction. And the last

one we're going to look at in quite a lot of detail in the next semester is called induction,

is actually finding out rules. Right? On Monday the street is wet, it rained. Tuesday it rained,

the street is wet. Wednesday same thing. Okay? And at some point you're going to say, ah,

always when it rains the street is wet. Okay? At which point you can do in deduction and

induction, deduction and abduction as an agent. Okay? So agents need all of those. We've only

talked about deduction. Abduction is relatively simple. You just add cheating. Yeah? So if you

allow yourselves to do deduction with cheating, that gives you explanations and depending on

where you cheat it gives you different explanations. And this here is at the heart of machine learning

which we're going to do next semester.