If you want to do better, there is some kind of a standard way of doing things better.

You can do these derived rules of inference, which is essentially macro steps.

We talked at length about this.

It really is an engineering question whether you want to include them.

If your processor is wetware, then you probably do.

If you implement it in a high throughput agent function, you just have to see what works

better.

We looked at examples.

We discussed soundness.

Soundness is easy.

In these kind of test calculi, you always want to show that every rule preserves soundness

because we're interested in unsatisfiability.

We want to conclude that if I have an obvious unsatisfiability, that this is not something

my calculus made up.

If you're not allowed to make up unsatisfiability, you have to preserve satisfiability.

If it's satisfiability before, it must be satisfiability after.

That guarantees that any kind of unsatisfiability you see at the end actually comes from here

and is not made up in between.

That's the soundness argument.

The soundness argument you see here is essentially getting the math right of chaining single

rule soundness into calculus soundness.

Of course, since proofs may be arbitrarily long, that's actually an induction proof.

No surprise there.

We looked at termination.

The agent is very interested in knowing that it can act after a finite time.

They would like to know that it can act after a constant time, constant short time.

That's not something we're going to get.

But we have decidability.

That's the typical thing you want to show.

If you have a calculus, you're interested in termination.

For some logics, you get that.

For propositional logic, you get that.

For first-order logic, you don't.

For any more interesting logic, you don't either.

You're interested in soundness.

If your calculus isn't sound, it will make predictions about the world that are not true.

If you as an agent base your actions on untrue assumptions about the world, your mileage

may vary depending on where the errors in the predictions are and how well you can,

as an agent, deal with errors.

This is something that you're always interested in.

The last thing you're interested in is completeness.

Typically, one is a little bit...

Often one is willing to or has to compromise on completeness.

Completeness is something that's wonderful for doing a PhD thesis.

But in practice, you can get by without completeness often if it's not too glaring in completeness.

As you'll probably have seen in the mock exam, tableaus are very nice for exams.

It's good to understand what you're doing.

It's not good if we ask for a tableau proof of this and that to try and give us something

that isn't resolution proof, but you write it down as a tree.

It's not a good idea for an exam at least.