Natural deduction is also not what I would want to implement in an agent. Why? Because

it's a positive calculus. You start with the axioms and you kind of go deriving and if you're lucky

you hit the theorem, the question. You want to prove there is food and the best way in logic,

if you want to implement it, is not to prove there is proof from the axioms but to assume

there isn't any proof, there isn't any food and disprove that. Make a refutation of there isn't

any food. That typically even tells you where the food is, namely bananas in the fridge. Okay? And

that's really what we're going to use for actual inference in agents. The important theoretical

result behind that is what we call the unsatisfiability theorem, which basically says A is entailed by a

set of hypothesis or think of them as observations or these kind of things, if and only if the

observations together with the negated theorem is unsatisfiable. That gives us leeway to have a

much more directed version of inference here in our agent. By the way, this theorem is also at the

guts of Prolog. Remember in Prolog we had a program. That's essentially what this H is and then we have

a query, which is basically in the world described by the program, is it true that there is a car? I

think that was one of our examples. What Prolog does is essentially behind the scenes says there's

no car. Munges the whole thing up and searches for a contradiction in a very simple calculus,

which is something we're going to look at. So-called resolution calculus. So we're doing,

Prolog is an inference engine, which is something we could just basically directly use here.

And you've done so, essentially.