|
|
Introduction to Logic
|
Tools for Thought
|
|
In a previous section, we saw how to use resolution in answering true-or-false questions (e.g. Is Art the grandparent of Coe?). In this section, we show how resolution can be used to answer fill-in-the-blank questions as well (e.g. Who is the grandparent of Coe?).
A fill-in-the-blank question is a sentence with free variables specifying the blanks to be filled in. The goal is to find bindings for the free variables such that the database logically entails the sentence obtained by substituting the bindings into the original question.
For example, to ask about Jon's parent, we would write the question p(x,jon). Using the database from the previous section, we see that art is an answer to this question, since the sentence p(art, jon) is logically entailed by the database.
|
An answer literal for a fill-in-the-blank question φ is a sentence goal(ν1, ... , νn), where ν1, ... , νn are the free variables in φ. To answer φ, we form an implication from φ and its answer literal and convert to clausal form.
For example, the literal p(x, jon) is combined with its answer literal goal(x) to form the rule (p(x, jon) ⇒ goal(x)), which leads to the clause {¬p(x, jon),goal(x)}.
|
To get answers, we use resolution as described above, except that we change the termination test. Rather than waiting for the empty clause to be produced, the procedure halts as soon as it derives a clause consisting of only answer literals. The following resolution derivation shows how we compute the answer to Who is Jon's parent?
1. | {f(art, jon)} | Premise |
2. | {f(bob, kim)} | Premise |
3. | {¬f(x, y), p(x, y)} | Premise |
4. | {¬p(x, jon), goal(x)} | Goal |
5. | {¬f(x, jon), goal(x)} | 3, 4 |
6. | {goal(art)} | 1, 5 |
|
If this procedure produces only one answer literal, the terms it contains constitute the only answer to the question. In some cases, the result of a fill-in-the-blank resolution depends on the refutation by which it is produced. In general, several different refutations can result from the same query, leading to multiple answers.
Suppose, for example, that we knew the identities of both the father and mother of Jon and that we asked Who is one of Jon's parents? The following resolution trace shows that we can derive two answers to this question.
1. | {f(art, jon)} | Premise |
2. | {m(ann, jon)} | Premise |
3. | {¬f(x, y), p(x, y)} | Premise |
4. | {¬m(x, y), p(x, y)} | Premise |
5. | {¬p(x, jon), goal(x)} | Goal |
6. | {¬f(x, jon), goal(x)} | 3, 5 |
7. | {goal(art)} | 1, 6 |
8. | {¬m(x, jon), goal(x)} | 4, 5 |
9. | {goal(ann)} | 2, 8 |
|
Unfortunately, we have no way of knowing whether or not the answer statement from a given refutation exhausts the possibilities. We can continue to search for answers until we find enough of them. However, due to the undecidability of logical entailment, we can never know in general whether we have found all the possible answers.
|
Another interesting aspect of fill-in-the-blank resolution is that in some cases the procedure can result in a clause containing more than one answer literal. The significance of this is that no one answer is guaranteed to work, but one of the answers must be correct.
|
The following resolution trace illustrates this fact. The database in this case is a disjunction asserting that either Art or Bob is the father of Jon, but we do not know which man is. The goal is to find a parent of John. After resolving the goal clause with the sentence about fathers and parents, we resolve the result with the database disjunction, obtaining a clause that can be resolved a second time yielding a clause with two answer literals. This answers indicates not two answers but rather uncertainty as to which is the correct answer.
1. | {f(art, jon), f(bob, jon)} | Premise |
2. | {¬f(x, y), p(x, y)} | Premise |
3. | {¬p(x, jon), goal(x)} | Goal |
4. | {¬f(x, jon), goal(x)} | 2, 3 |
5. | {f(art, jon), goal(bob)} | 1, 4 |
6. | {goal(art), goal(bob)} | 5, 4 |
In such situations, we can continue searching in hope of finding a more specific answer. However, given the undecidability of logical entailment, we can never know in general whether we can stop and say that no more specific answer exists.
|
Use the arrow keys to navigate.
Press the escape key to toggle all / one.
|
|