This is a terrible calculus for agents. Terrible AI calculus. Why? Because it's certainly not

how we do inference as humans, and that's kind of the standard. Remember, Elaine Rich's

definition, AI is doing things that humans can do better right now. By shooting yourself

into a foot with a Hilbert-style calculus, you're not going to do anything better than

a human. So try to do it like a human does. We did that. We called it the calculus of natural

deduction. Different set of rules, different formal language, formal language of propositional

logic, and a couple of rules. We looked into them in detail. You can chain them into proofs,

and it feels like what you're doing when you're trying to convince somebody else that we should

go to AI today and not make a wonderful hike in the snow. And you're going to argue, and

typically all the arguments you're going to do are going to look somewhere like this.

We looked at that in detail and via various forms and so on. Yes. Would somebody relay?

All the way in the last row. Could you tell us how do I formally correctly disprove using

natural deduction? What do you mean by disprove? For example, in our homework, there's some

something like approve or disprove this statement using natural deduction. Yes. Disprove is

typically being done by making a counterexample. Okay? If I want to say, let me see. All women

are black-haired. That's not true, obviously. My disprove would be there. Look, there's

one. Okay? But how do I write this down in natural deduction? Because in natural deduction,

so far it was only assume that this is true, then it follows it. I think you have the brackets

wrong. Proof is natural deduction or disprove? You can try to prove the negation. And that

is also something you can do. And in propositional logic, that actually works. But the disproof

for the refutation for the negation you're going to get, you can actually make into an

example, a counterexample, and vice versa.