The thing I would like to very briefly alert you to is you remember that we did tableau

And tableau is essentially, you start with a label it by false and develop the whole thing

into a tree of possibilities and every one of these branches in my tree has to be,

has to contain a contradiction. If you think about that, the branches internally I read as

conjunctions, right, if there's A, B, and C, and D on it I read that as B, C, and B, and C, and D,

whereas the branches are actually act like an or. So what we're actually implementing is something

of the form I have a conjunction of literals on each branch, the others I don't want, the others

are worked off we talked about that, right, and I have a big disjunction over that. So I have something

of that form and that's we know that this always exists it's called the disjunctive normal form and

we're implicitly, we're implicitly computing that in a tableau and we are if you want to think about

it the inference process actually makes the contradictions that are already present in the

original formula A we make them explicit, easy to detect, right, the contradiction is if every

possibility has a contradiction and how can a branch have a contradiction well something and

something and something and something and contradiction well that's contradictory. In a

conjunction you have to make everything true and the contradiction you can never make true. So this

is something you can actually see directly you can write a three-line program that actually looks at

a tableau goes through recursively and looks for looks for contradiction so it's in a way obvious

and that's really all that inference procedures do. We have a property of a formula or a description

of the world that we're interested in and we massage it into a form where that property becomes

obvious and easy to read off. That's how we do it in a tableau and in resolution you remember we

have these sets of clauses and clauses are disjunctions of literals. So sets of clauses

we read as conjunctions and clauses are disjunctions of literals so there we have a conjunction over

disjunction of literals as just the dual form and that also always exists and in resolution we kind

of brought the whole thing into clause set form into conjunctive normal form and then

we use the very simple reasoning that would detect a contradiction in there by

making a resolution proof. Okay until it's really really really clear namely an empty

clause we can never make true and a clause set which is a conjunction that

contains an empty clause because that's conjunctive I have to make

all these clauses true I can never make true. We start off with an AF. We make a

clause set from it and then we start resolution that's not nicely drawn

until we end up in an empty clause. Same thing we start off with something where

the contradiction is there but implicit. We massage it into a form where it's

easy to read off. Same idea. Okay how does that work? For the tableaus as we looked

at we actually make this analysis into a tree. We look for closed tableaus and if

we have a closed tableau that constitutes a proof. We've looked at the

rules and we've looked at a couple of examples and I want to these examples I

only want to remind you again that this here is still propositional logic.

Propositional logic remember was something where we had propositional

variables and or not whatever you want to throw into the mix and the only thing

we're doing here is we're giving fancy names to propositional variables. So it

wouldn't be a problem actually translating into real honest to

goodness according to the slides thing by just making a translation table and

say love Mary Bill goes to P and love John Mary goes to Q and then the formula

goes to P and Q implies Q. Okay so there's nothing fishy going on here. Just

want to remind you that propositional logic is something we can use to talk

about the real world and do inference about the rule real world by extension.

Okay that's tableau that easy.