Transcript 4/10

Answer Extraction
To use resolution to answer questions, for example a query
of the form X C(X), we must keep track of the substitutions
made during the refutation process by using an answer
literal:
 we add a literal Ans(X,...., Z) to each clause coming from
the negation of the query, and perform resolution until only
an answer literal is left; the variables X,...,Z are all of those
variables that occur in the clause form of the negation of the
query.
The terms substituted during the proof for the variables in the Ans
literal will then be instances of the existentially quantified variables in
the query.
Resolution System
To answer if KB |= Q:
Convert S = KB U { Q} into S’ = CNF(S) (or
INF(S))
convert each formula of S into clauses
Iteratively apply resolution to the clauses in S’ and
add the results to S’ either until there are no more
resolvents that can be added or until the empty
clause is produced.
Refinement Strategies
The procedure described above is inefficient
because some resolutions need not be performed at
all (are irrelevant).
Refinement strategies disallows certain kinds of
resolutions to take place.
Linear resolution with initial set of support
Important Theorems
 Let S be a set of wffs and S’ the set of clauses
obtained by converting S to CNF (to INF).
 In Propositional Logic S and S’ are equivalent;
but in FOL they are not equivalent in general
 But in both logics we have:
S is unsatisfiable iff S’ is unsatisfiable.
 Therefore, KB |= Q iff S = KB U { Q}is unsat
iff S’ is unsat
Important Theorems
Then we can use resolution to check
if S’ |- False(empty clause)
and if it is
use soundness to infer that S’ is unsat, then S is
unsat then KB entails Q;
else use completeness to infer that S’ is satisfiable,
then S is sat then KB does not entail Q.
SLD Resolution
 Language: Horn clauses in INF
S - Selection Function - selects the atom in the goal clause
to resolve
L- Linear Resolution
D - Definite Clauses
The set of clauses S’ (a set of quasi-definite
clauses):
a set of definite clauses (representing KB), together
with one goal clause (representing  Q).
SLD Resolution
Standard selection function (PROLOG): leftmost atom
Let C1 be a goal clause and C2 a definite clause; if there is
an atom P1 in C1 and an atom P in the head of C2 such that
P1 and P have a mgu , then these two clauses have the
following resolvent:
P1  ...  Pn1 
S1  ...  Sn3  P
--------------------------------------------------------(S1  ...  Sn3  P2...  Pn1)  
Remember that the order of atoms is important!
resolvent - play DO:
body of definite clause then body of the objective clause
PROLOG and AI
www.cs.wisc.edu/~fischer/cs538.s00/prolog/prolog.html
Computational Intelligence: a logical approach
D. Poole, A. Mackworth, R. Goebel
Oxford University Press , 1988
Appendix (477-490) - Intro to Prolog
PROLOG
Cut
Used to prune part of the search-space and to restrict
backtracking.
When called, it succeeds immediately;
when it is retried (backtracked to),
it fails the procedure in which it appears
The cut effectively tells Prolog to freeze all the decisions
made so far in this predicate. That is, if required to
backtrack, it will automatically fail without trying other
alternatives.
PROLOG
Here is the first test case. It has no cut and will be used for
comparison purposes.
data(one).
data(two).
data(three).
cut_test_a(X) :- data(X).
cut_test_a('last clause').
PROLOG
This is the control case, which exhibits the normal
behavior.
?- cut_test_a(X), write(X), nl, fail.
one
two
three
last clause
no
PROLOG
Next, we put a cut at the end of the first clause.
cut_test_b(X) :data(X),
!.
cut_test_b('last clause').
Note that it stops backtracking through both the data/1
subgoal (left), and the cut_test_b parent (above).
?- cut_test_b(X), write(X), nl, fail.
one
no
PROLOG
Next we put a cut in the middle of two subgoals.
cut_test_c(X,Y) :data(X),
!,
data(Y).
cut_test_c('last clause').
Note that the cut inhibits backtracking in the parent
cut_test_c and in the goals to the left of (before) the cut
(first data/1).
PROLOG
The second data/1 to the right of (after) the cut is still free
to backtrack.
?- cut_test_c(X,Y), write(X-Y), nl, fail.
one - one
one - two
one - three
no
alternatives.
SLDNF Resolution
Negation in PROLOG: Negation as (finite) Failure
P if an SLDNF tree starting from
P
finitely fails.
Not
PROLOG
Negation as Failure in Prolog (written as “\+”):
not(G) :- G, ! Fail.
not(G).