Okay, the quiz should have ended.

So let's start.

I hope you can all hear me.

I would like to get back to analytical Tableau.

We talked about Tableau and you had lots of Tableaus in the quiz.

Remember that we are doing refutation proofs, which means we take the formula we want to

show as valid, mark it with false, and then we analyze it in a Tableau, which when it's

saturated and closed, meaning all of the branches end in a contradiction, then we have a proof.

Dual to this, we can actually use Tableaus.

Are there any questions?

Dual to this is using, we can use Tableaus for model generation where we basically want to show with the same calculus that a formula is true or can be made true.

You can see it's marked up here with a true.

We develop it in a Tableau.

We have a Tableau which tries to make the formula true.

And here we have what we call an open branch.

And this open branch, we can just look at the literals and see and read off a satisfying assignment.

So a refutation, a proof of unsatisfiability is all closed, meaning there's no way of making it false.

If we want to use Tableaus for satisfiability, we can actually do so and we can read off the satisfying assignment here.

We looked at the Tableau rules.

We actually also looked at quite a lot of examples and we looked at derivable rules of inference, rules that are essentially macro steps,

but make the proving easier.

But now we have talked about soundness and completeness of calculus.

And this is something I would like to.

I would like to go into a little bit here.

We have a test calculus and we want to say that it's refutation sound.

And then what we need to do is to see whether the inference rules preserve satisfiability.

The idea there is that in a Tableau, as we have it here,

satisfiability means that we can actually give the formula P and Q implies Q and P, the truth value false.

Now, if satisfiability is preserved and I end up in an unsatisfiable, in an obviously unsatisfiable formula,

then the only reason for that can be that the original formula was unsatisfiable or, in other words,

that it's impossible to make P and Q implies Q and P false.

So it must be true. So it must be valid.

So that's the real that's the right property we want to look at.

And so we're defining the formula, a label formula is valid if it basically has the right truth value that's marked in the alpha here.

And the Tableau is satisfiable if there is a satisfiable branch.

And so if we actually convince ourselves that Tableau rules transform form satisfiable Tableaus into satisfiable ones,

then we must have we must have that closed saturated Tableaus are a sign of unsatisfiable

formula, which makes the which makes the conjecture we're trying to prove with the Tableau makes them valid.

You may wonder, it's kind of convoluted with lots of negations, right?

So instead of showing that something is valid, we show that the assumption that something is satisfiable cannot be that the satisfiability of the negation.

But if you think about it, this is exactly what we what we need.

So that's one thing Tableau are sound. They happen to also be complete, but that's much more difficult to show.

And I'm not going to do it here.

What is also the case, which is what is very important, is that Tableaus in propositional logic are they terminate,

which means that after finitely many rule applications, a Tableau becomes saturated.

And so termination proofs are something that is also relatively.

It's a relatively paradigmatic proof.

And so I want to show you an instance of this. We do this.

We basically look at all the rules and.

Whenever you do. Whenever you want to show that something terminates,