Skolemization, Most General Unifiers, First-Order Resolution

1 skolemization , most General Unifiers, First-Order ResolutionTorsten HahmannCSC 384, University of TorontoMarch 07, 2011 SkolemizationConversion of sentences FOL to CNF requires : remove existential quantifiers by introducing newfunction : For each existentially quantified variable introduce a n-placefunction where n is the number of previously appearing case: introducing constants (trivial functions: no previousuniversal quantifier). skolemization - Example 1 IEvery philosopher writes at least one book. x[Philo(x) y[Book(y) Write(x,y)]]IEliminate Implication: x[ Philo(x) y[Book(y) Write(x,y)]]ISkolemize: substituteybyg(x) x[ Philo(x) [Book(g(x)) Write(x,g(x))]] skolemization - Example 1 IEvery philosopher writes at least one book. x[Philo(x) y[Book(y) Write(x,y)]]IEliminate Implication: x[ Philo(x) y[Book(y) Write(x,y)]]ISkolemize: substituteybyg(x) x[ Philo(x) [Book(g(x)) Write(x,g(x))]] skolemization - Example 1 IEvery philosopher writes at least one book. x[Philo(x) y[Book(y) Write(x,y)]]IEliminate Implication: x[ Philo(x) y[Book(y) Write(x,y)]]ISkolemize: substituteybyg(x) x[ Philo(x) [Book(g(x)) Write(x,g(x))]] skolemization - Example 2 IAll students of a philosopher read one of their teacher s books.

2 X y[Philo(x) StudentOf(y,x) z[Book(z) Write(x,z) Read(y,z)]]IEliminate Implication: x y[ Philo(x) StudentOf(y,x) z[Book(z) Write(x,z) Read(y,z)]]ISkolemize: substitutezbyh(x,y) x y[ Philo(x) StudentOf(y,x) [Book(h(x,y)) Write(x,h(x,y)) Read(y,h(x,y))]] skolemization - Example 2 IAll students of a philosopher read one of their teacher s books. x y[Philo(x) StudentOf(y,x) z[Book(z) Write(x,z) Read(y,z)]]IEliminate Implication: x y[ Philo(x) StudentOf(y,x) z[Book(z) Write(x,z) Read(y,z)]]ISkolemize: substitutezbyh(x,y) x y[ Philo(x) StudentOf(y,x) [Book(h(x,y)) Write(x,h(x,y)) Read(y,h(x,y))]] skolemization - Example 2 IAll students of a philosopher read one of their teacher s books. x y[Philo(x) StudentOf(y,x) z[Book(z) Write(x,z) Read(y,z)]]IEliminate Implication: x y[ Philo(x) StudentOf(y,x) z[Book(z) Write(x,z) Read(y,z)]]ISkolemize: substitutezbyh(x,y) x y[ Philo(x) StudentOf(y,x) [Book(h(x,y)) Write(x,h(x,y)) Read(y,h(x,y))]] skolemization - Example 3 IThere exists a philosopher with students.

3 X y[Philo(x) StudentOf(y,x)]ISkolemize: substitutexbyaandybybPhilo(a) StudentOf(b,a) skolemization - Example 3 IThere exists a philosopher with students. x y[Philo(x) StudentOf(y,x)]ISkolemize: substitutexbyaandybybPhilo(a) StudentOf(b,a) most General UnifierLeast specialized unification of two can compute the MGU using the disagreement setDk={e1,e2}: the pair of expressions where two clauses UNTIL no more disagreement found eithere1ore2is a variableVand the other is some term (or avariable)t, then chooseV=tas substitute to obtainSk+1and find disagreement setDk+ unification is not - Example 1 Find the MGU ofp(f(a),g(X)) andp(Y,Y):IS0={p(f(a),g(X)) ;p(Y,Y)}ID0={f(a),Y}I ={Y=f(a)}IS1={p(f(a),g(X)) ;p(f(a),f(a))}ID1={g(X),f(a)}Ino unification possible!MGU - Example 1 Find the MGU ofp(f(a),g(X)) andp(Y,Y):IS0={p(f(a),g(X)) ;p(Y,Y)}ID0={f(a),Y}I ={Y=f(a)}IS1={p(f(a),g(X)) ;p(f(a),f(a))}ID1={g(X),f(a)}Ino unification possible!MGU - Example 1 Find the MGU ofp(f(a),g(X)) andp(Y,Y):IS0={p(f(a),g(X)) ;p(Y,Y)}ID0={f(a),Y}I ={Y=f(a)}IS1={p(f(a),g(X)) ;p(f(a),f(a))}ID1={g(X),f(a)}Ino unification possible!

4 MGU - Example 1 Find the MGU ofp(f(a),g(X)) andp(Y,Y):IS0={p(f(a),g(X)) ;p(Y,Y)}ID0={f(a),Y}I ={Y=f(a)}IS1={p(f(a),g(X)) ;p(f(a),f(a))}ID1={g(X),f(a)}Ino unification possible!MGU - Example 1 Find the MGU ofp(f(a),g(X)) andp(Y,Y):IS0={p(f(a),g(X)) ;p(Y,Y)}ID0={f(a),Y}I ={Y=f(a)}IS1={p(f(a),g(X)) ;p(f(a),f(a))}ID1={g(X),f(a)}Ino unification possible!MGU - Example 2IS0={p(a,X,h(g(Z))) ;p(Z,h(Y),h(Y))}ID0={a,Z}I ={Z=a}IS1={p(a,X,h(g(a))) ;p(a,h(Y),h(Y))}ID1={X,h(Y)}I ={Z=a,X=h(Y)}IS2={p(a,h(Y),h(g(a))) ;p(a,h(Y),h(Y))}ID2={g(a),Y}I ={Z=a,X=h(Y),Y=g(a)}IS3={p(a,h(g(a)),h(g (a))) ;p(a,h(g(a)),h(g(a)))}INo disagreement ={Z=a,X=h(Y),Y=g(a)}is MGUMGU - Example 2IS0={p(a,X,h(g(Z))) ;p(Z,h(Y),h(Y))}ID0={a,Z}I ={Z=a}IS1={p(a,X,h(g(a))) ;p(a,h(Y),h(Y))}ID1={X,h(Y)}I ={Z=a,X=h(Y)}IS2={p(a,h(Y),h(g(a))) ;p(a,h(Y),h(Y))}ID2={g(a),Y}I ={Z=a,X=h(Y),Y=g(a)}IS3={p(a,h(g(a)),h(g (a))) ;p(a,h(g(a)),h(g(a)))}INo disagreement ={Z=a,X=h(Y),Y=g(a)}is MGUMGU - Example 2IS0={p(a,X,h(g(Z))) ;p(Z,h(Y),h(Y))}ID0={a,Z}I ={Z=a}IS1={p(a,X,h(g(a))) ;p(a,h(Y),h(Y))}ID1={X,h(Y)}I ={Z=a,X=h(Y)}IS2={p(a,h(Y),h(g(a))) ;p(a,h(Y),h(Y))}ID2={g(a),Y}I ={Z=a,X=h(Y),Y=g(a)}IS3={p(a,h(g(a)),h(g (a))) ;p(a,h(g(a)),h(g(a)))}INo disagreement ={Z=a,X=h(Y),Y=g(a)}is MGUMGU - Example 2IS0={p(a,X,h(g(Z))) ;p(Z,h(Y),h(Y))}ID0={a,Z}I ={Z=a}IS1={p(a,X,h(g(a))).}

5 P(a,h(Y),h(Y))}ID1={X,h(Y)}I ={Z=a,X=h(Y)}IS2={p(a,h(Y),h(g(a))) ;p(a,h(Y),h(Y))}ID2={g(a),Y}I ={Z=a,X=h(Y),Y=g(a)}IS3={p(a,h(g(a)),h(g (a))) ;p(a,h(g(a)),h(g(a)))}INo disagreement ={Z=a,X=h(Y),Y=g(a)}is MGUMGU - Example 2IS0={p(a,X,h(g(Z))) ;p(Z,h(Y),h(Y))}ID0={a,Z}I ={Z=a}IS1={p(a,X,h(g(a))) ;p(a,h(Y),h(Y))}ID1={X,h(Y)}I ={Z=a,X=h(Y)}IS2={p(a,h(Y),h(g(a))) ;p(a,h(Y),h(Y))}ID2={g(a),Y}I ={Z=a,X=h(Y),Y=g(a)}IS3={p(a,h(g(a)),h(g (a))) ;p(a,h(g(a)),h(g(a)))}INo disagreement ={Z=a,X=h(Y),Y=g(a)}is MGUMGU - Example 2IS0={p(a,X,h(g(Z))) ;p(Z,h(Y),h(Y))}ID0={a,Z}I ={Z=a}IS1={p(a,X,h(g(a))) ;p(a,h(Y),h(Y))}ID1={X,h(Y)}I ={Z=a,X=h(Y)}IS2={p(a,h(Y),h(g(a))) ;p(a,h(Y),h(Y))}ID2={g(a),Y}I ={Z=a,X=h(Y),Y=g(a)}IS3={p(a,h(g(a)),h(g (a))) ;p(a,h(g(a)),h(g(a)))}INo disagreement ={Z=a,X=h(Y),Y=g(a)}is MGUMGU - Example 2IS0={p(a,X,h(g(Z))) ;p(Z,h(Y),h(Y))}ID0={a,Z}I ={Z=a}IS1={p(a,X,h(g(a))) ;p(a,h(Y),h(Y))}ID1={X,h(Y)}I ={Z=a,X=h(Y)}IS2={p(a,h(Y),h(g(a))) ;p(a,h(Y),h(Y))}ID2={g(a),Y}I ={Z=a,X=h(Y),Y=g(a)}IS3={p(a,h(g(a)),h(g (a))) ;p(a,h(g(a)),h(g(a)))}INo disagreement ={Z=a,X=h(Y),Y=g(a)}is MGUMGU - Example 2IS0={p(a,X,h(g(Z))) ;p(Z,h(Y),h(Y))}ID0={a,Z}I ={Z=a}IS1={p(a,X,h(g(a))) ;p(a,h(Y),h(Y))}ID1={X,h(Y)}I ={Z=a,X=h(Y)}IS2={p(a,h(Y),h(g(a))) ;p(a,h(Y),h(Y))}ID2={g(a),Y}I ={Z=a,X=h(Y),Y=g(a)}IS3={p(a,h(g(a)),h(g (a))) ;p(a,h(g(a)),h(g(a)))}INo disagreement ={Z=a,X=h(Y),Y=g(a)}is MGUMGU - Example 2IS0={p(a,X,h(g(Z))) ;p(Z,h(Y),h(Y))}ID0={a,Z}I ={Z=a}IS1={p(a,X,h(g(a))) ;p(a,h(Y),h(Y))}ID1={X,h(Y)}I ={Z=a,X=h(Y)}IS2={p(a,h(Y),h(g(a))) ;p(a,h(Y),h(Y))}ID2={g(a),Y}I ={Z=a,X=h(Y),Y=g(a)}IS3={p(a,h(g(a)),h(g (a))) ;p(a,h(g(a)),h(g(a)))}INo disagreement ={Z=a,X=h(Y),Y=g(a)}is MGUMGU - Example 2IS0={p(a,X,h(g(Z))) ;p(Z,h(Y),h(Y))}ID0={a,Z}I ={Z=a}IS1={p(a,X,h(g(a))) ;p(a,h(Y),h(Y))}ID1={X,h(Y)}I ={Z=a,X=h(Y)}IS2={p(a,h(Y),h(g(a))) ;p(a,h(Y),h(Y))}ID2={g(a),Y}I ={Z=a,X=h(Y),Y=g(a)}IS3={p(a,h(g(a)),h(g (a))).

6 P(a,h(g(a)),h(g(a)))}INo disagreement ={Z=a,X=h(Y),Y=g(a)}is MGUMGU - Example 2IS0={p(a,X,h(g(Z))) ;p(Z,h(Y),h(Y))}ID0={a,Z}I ={Z=a}IS1={p(a,X,h(g(a))) ;p(a,h(Y),h(Y))}ID1={X,h(Y)}I ={Z=a,X=h(Y)}IS2={p(a,h(Y),h(g(a))) ;p(a,h(Y),h(Y))}ID2={g(a),Y}I ={Z=a,X=h(Y),Y=g(a)}IS3={p(a,h(g(a)),h(g (a))) ;p(a,h(g(a)),h(g(a)))}INo disagreement ={Z=a,X=h(Y),Y=g(a)}is MGUMGU - Example 3IS0={p(X,X) ;p(Y,f(Y))}ID0={X,Y}I ={X=Y}IS1={p(Y,Y) ;p(Y,f(Y))}ID1={Y,f(Y)}Ino unification possible!MGU - Example 3IS0={p(X,X) ;p(Y,f(Y))}ID0={X,Y}I ={X=Y}IS1={p(Y,Y) ;p(Y,f(Y))}ID1={Y,f(Y)}Ino unification possible!MGU - Example 3IS0={p(X,X) ;p(Y,f(Y))}ID0={X,Y}I ={X=Y}IS1={p(Y,Y) ;p(Y,f(Y))}ID1={Y,f(Y)}Ino unification possible!MGU - Example 3IS0={p(X,X) ;p(Y,f(Y))}ID0={X,Y}I ={X=Y}IS1={p(Y,Y) ;p(Y,f(Y))}ID1={Y,f(Y)}Ino unification possible!MGU - Example 3IS0={p(X,X) ;p(Y,f(Y))}ID0={X,Y}I ={X=Y}IS1={p(Y,Y) ;p(Y,f(Y))}ID1={Y,f(Y)}Ino unification possible!MGU - Example 3IS0={p(X,X) ;p(Y,f(Y))}ID0={X,Y}I ={X=Y}IS1={p(Y,Y) ;p(Y,f(Y))}ID1={Y,f(Y)}Ino unification possible!

7 Full example problemGiven the following sentences, answer the question What isconnected to the Galbraith building? using Resolution with answerextraction:Connected is a binary symmetric objectXis part of another objectYiff everythingXisconnected to,Yis also connected GB221 is part of Galbraith GB221 is connected to example problem - Representation in FOL(a) Represent these sentences in first order is a binary symmetric objectXis part of another objectYiff everythingXisconnected to,Yis also connected GB221 is part of Galbraith GB221 is connected to example problem - Representation in FOLIC onnected is a symmetric relation.( X,Y)connected(X,Y) connected(Y,X)IAn objectXis part of another objectYiff everythingXisconnected to,Yis also connected to.( X,Y) (part(X,Y) (( Z)connected(Z,X) connected(Z,Y)))IRoom GB221 is part of Galbraith (gb221,galbraith)IRoom GB221 is connected to (gb221,gb221)Full example problem - Representation in FOLIC onnected is a symmetric relation.

8 ( X,Y)connected(X,Y) connected(Y,X)IAn objectXis part of another objectYiff everythingXisconnected to,Yis also connected to.( X,Y) (part(X,Y) (( Z)connected(Z,X) connected(Z,Y)))IRoom GB221 is part of Galbraith (gb221,galbraith)IRoom GB221 is connected to (gb221,gb221)Full example problem - Representation in FOLIC onnected is a symmetric relation.( X,Y)connected(X,Y) connected(Y,X)IAn objectXis part of another objectYiff everythingXisconnected to,Yis also connected to.( X,Y) (part(X,Y) (( Z)connected(Z,X) connected(Z,Y)))IRoom GB221 is part of Galbraith (gb221,galbraith)IRoom GB221 is connected to (gb221,gb221)Full example problem - Representation in FOLIC onnected is a symmetric relation.( X,Y)connected(X,Y) connected(Y,X)IAn objectXis part of another objectYiff everythingXisconnected to,Yis also connected to.( X,Y) (part(X,Y) (( Z)connected(Z,X) connected(Z,Y)))IRoom GB221 is part of Galbraith (gb221,galbraith)IRoom GB221 is connected to (gb221,gb221)Full example problem - CNF Conversion(b) Convert the formulas to clausal form.

9 Indicate any Skolemfunctions or constants used.( X,Y)connected(X,Y) connected(Y,X)( X,Y)part(X,Y) ( Z)connected(Z,X) connected(Z,Y)part(gb221,galbraith)conne cted(gb221,gb221)Full example problem - CNF ConversionI( X,Y)connected(X,Y) connected(Y,X)[ connected(X,Y),connected(Y,X)]I( X,Y)part(X,Y) ( Z)connected(Z,X) connected(Z,Y) : [ part(X,Y), connected(Z,X),connected(Z,Y)] : [part(X,Y),connected(f(X,Y),X)][part(X,Y ), connected(g(X,Y),Y)]Ipart(gb221,galbrait h)[part(gb221,galbraith)]Iconnected(gb22 1,gb221)[connected(gb221,gb221)]Full example problem - CNF ConversionI( X,Y)connected(X,Y) connected(Y,X)[ connected(X,Y),connected(Y,X)]I( X,Y)part(X,Y) ( Z)connected(Z,X) connected(Z,Y) : [ part(X,Y), connected(Z,X),connected(Z,Y)] : [part(X,Y),connected(f(X,Y),X)][part(X,Y ), connected(g(X,Y),Y)]Ipart(gb221,galbrait h)[part(gb221,galbraith)]Iconnected(gb22 1,gb221)[connected(gb221,gb221)]Full example problem - CNF ConversionI( X,Y)connected(X,Y) connected(Y,X)[ connected(X,Y),connected(Y,X)]I( X,Y)part(X,Y) ( Z)connected(Z,X) connected(Z,Y) : [ part(X,Y), connected(Z,X),connected(Z,Y)] : [part(X,Y),connected(f(X,Y),X)][part(X,Y ), connected(g(X,Y),Y)]Ipart(gb221,galbrait h)[part(gb221,galbraith)]Iconnected(gb22 1,gb221)[connected(gb221,gb221)]Full example problem - CNF ConversionI( X,Y)connected(X,Y) connected(Y,X)[ connected(X,Y),connected(Y,X)]I( X,Y)part(X,Y) ( Z)connected(Z,X) connected(Z,Y) : [ part(X,Y), connected(Z,X),connected(Z,Y)].

10 [part(X,Y),connected(f(X,Y),X)][part(X,Y ), connected(g(X,Y),Y)]Ipart(gb221,galbrait h)[part(gb221,galbraith)]Iconnected(gb22 1,gb221)[connected(gb221,gb221)]Full example problem - Goal(c) Convert the negation of the statement What is connected tothe Galbraith building? to clause form (using an answer literal).IFOL: ( X)connected(galbraith,X)Inegate goal!! ( X)connected(galbraith,X)ICNF with answer literal: ( X) connected(galbraith,X)[ connected(galbraith,X),ans(X)]Full example problem - Goal(c) Convert the negation of the statement What is connected tothe Galbraith building? to clause form (using an answer literal).IFOL: ( X)connected(galbraith,X)Inegate goal!! ( X)connected(galbraith,X)ICNF with answer literal: ( X) connected(galbraith,X)[ connected(galbraith,X),ans(X)]Full example problem - Goal(c) Convert the negation of the statement What is connected tothe Galbraith building? to clause form (using an answer literal).IFOL: ( X)connected(galbraith,X)Inegate goal!! ( X)connected(galbraith,X)ICNF with answer literal: ( X) connected(galbraith,X)[ connected(galbraith,X),ans(X)]Full example problem - Resolution (d) Answer the question using Resolution and answer the notation developed in class: every new clause must belabeled by the Resolution step that was used to generate it.