CODEWITHSUNDEEP
artificial-intelligencelogicdiscrete-mathematics
roccia
roccia

Reputation: 179

Need some hints about Resolution Rule prove

It's a homework. I'm trying to prove that (a v b) ^(~b V c) |= (a V c)

it's a correct resolution rule. And I'm not allowed to use resolution rule to prove it. Get little confusing, don't know what should I do at the first place..

And another problem, teacher let us to prove KB |= a, when KB ^ ~a is unsatisfiable. as far as I know , I may need to build a KB which includes several sentences, then I can prove KB ^ ~a is unsatisfiable. but teacher told to me If I want to derive an example, I have to let it suit for every cases. I want to know is there an universal example to prove that? Do I have to use example?

Hope somebody can give me some hints or useful links.. Thanks..

Upvotes: 2

Views: 1245

Answers (1)

Danica
Danica

Reputation: 28846

You can do it with the rule you describe in the third paragraph:

First, build a knowledge base of everything you know: namely a v b and ~b v c.

Then add the negation of the statement you're trying to prove: ~(a v c). You can rewrite this in CNF and add it to the KB.

Now show that this KB is unsatisfiable. There are two ways you can do this:

  • Just make a truth table. There are eight possible assignments to a, b, c, so it'll have eight rows; you can show that at least one statement in the KB is false for any possible assignment. This isn't an "example", because you're considering all possible cases.

  • Depending on the models you're using, you can make some inference within the KB itself. You'll have some statements that simply assert that a certain variable is true or false; you can then use that fact to simplify other statements in the KB. You'll want to check that you're doing this in a way that's appropriate in your formalism, though.

So, to prove that KB ^ ~a being unsatisfiable implies KB |= a, do a proof by contradiction:

  • You have KB.
  • Assume that, given KB, ~a is satisfiable.
  • But if that's true, then KB ^ ~a is satisfiable -- which you're proving is false, ie KB ^ ~a is unsatisfiable.
  • Therefore our assumption must have been wrong, and so ~a is unsatisfiable given KB.

Now you're pretty much there.

Upvotes: 2

Related Questions