Inference as Search

Question 1

logical equivalence

Answer 1

alpha and beta are equivalent if they entail each other

Question 2

validity

Answer 2

a sentence alpha is valid if it is true in all possible worlds

Question 3

satisfiable

Answer 3

a sentence alpha is satisfiable if it is true in at least one possible world

Question 4

deduction theorem

Answer 4

for any sentences alpha and beta, beta ⊨ alpha iff (beta -> alpha) is valid

Question 5

refutation

Answer 5

for any sentences alpha and beta, beta ⊨ alpha iff (beta ^ ~alpha) is unsatisfiable

Question 6

resolution inference algorithm

Answer 6

1. choose 2 sentences A V B and ~B V C from the KB
2. add A V C to the KB

Question 7

literal

Answer 7

an atomic sentence, or a negation of an atomic sentence

Question 8

clause

Answer 8

a disjunction of literals

Question 9

conjunctive normal form

Answer 9

a sentence expressed as a conjunction of clauses

Question 10

Steps for converting to CNF

Answer 10

1. eliminate <->
2. eliminate ->
3. move negation inwards, until only literals are negated
4. distribute V over ^

Question 11

ground resolution theorem

Answer 11

if a set of CNF clauses is unsatisfiable, then repeated application of the resolution rule will contain the empty clause