Report

<is web> Completeness of the SLD-Resolution ISWeb - Information Systems & Semantic Web ISWeb - Information Systems & Semantic Web Sergej Sizov MOA meeting [email protected] 1 of 25 Steffen Staab Foundations of Logic Programming [email protected] 1 of 12 <is web> Structure - 1 Preliminaries Definite Programs Semantics Soundness of SLD Resolution Completeness of SLD Resolution Normal Programs Add Negative Information and Finite Failure Soundness of SLDNF Resolution Completeness of SLDNF Resolution ISWeb - Information Systems & Semantic Web ISWeb - Information Systems & Semantic Web Sergej Sizov MOA meeting [email protected] 2 of 25 Steffen Staab Foundations of Logic Programming [email protected] 2 of 12 <is web> MGU Lemma Let P be a definite Program and G a definite goal. Suppose that P{G} has an unrestricted SLD-refutation (1, 2, … are not neccessarily mgu's). Then P{G} has an SLD-refutation of the same length with the mgu's ‘1… ‘n and there exists a substitution , such that 1… n = ‘1… ‘n. Proof (basis) Induction over the length of the unrestricted refutation. n=1: G0=G, G1=□ with input clause C1 and unifier 1. Suppose ‘1 is an mgu of the selected atom in G and the head of the input clause C1. Then 1= ‘1 for some . Furthermore, P{G} has a refutation G0=G, G1=□ with input clause C1 and MGU ‘1. ISWeb - Information Systems & Semantic Web ISWeb - Information Systems & Semantic Web Sergej Sizov MOA meeting [email protected] 3 of 25 Steffen Staab Foundations of Logic Programming [email protected] 3 of 12 <is web> MGU Lemma Let P be a definite Program and G a definite goal. Suppose that P{G} has an unrestricted SLD-refutation (1, 2, … are not neccessarily mgu's). Then P{G} has an SLD-refutation of the same length with the mgu's ‘1… ‘n and there exists a substitution , such that 1… n = ‘1… ‘n. Proof (Inductive step) Hypothesis: result holds for n-1. Suppose P{G} has an unrestricted SLD-refutation G0,G1,…Gn =□ of length n with the input clauses C1… Cn and Unifiers ‘1,2,3…,n such that G1=G‘1. By the inductive hypothesis: P{G‘1} has a refutation G‘1,…,G‘n =□ with mgu's ‘2…‘n such that 2…n= ‘2…‘n for some . Then P{G} has a refutation G0=G, G1,…,Gn =□ with mgu's ‘1…‘n such that 1…n=‘12…n= ‘1…‘n . ISWeb - Information Systems & Semantic Web ISWeb - Information Systems & Semantic Web Sergej Sizov MOA meeting [email protected] 4 of 25 Steffen Staab Foundations of Logic Programming [email protected] 4 of 12 <is web> Lifting Lemma Lemma Let P be a definite program, G a definite goal and a substitution. Suppose P{G} has an SLD-refutation with substitutions 1…n, such that the variables of the input clause are distinct from the variables in and G. Then there exists an SLD-refutation of P{G} of the same length and mgu's ‘1…‘n and a substitution such that 1…n=‘1…‘n. ISWeb - Information Systems & Semantic Web ISWeb - Information Systems & Semantic Web Sergej Sizov MOA meeting [email protected] 5 of 25 Steffen Staab Foundations of Logic Programming [email protected] 5 of 12 <is web> Lifting Lemma Proof Suppose the first input clause for the refutation of P{G} is C1, the first mgu is 1 and G1 is the goal which results from the first step Now 1 is a unifier for the head of C1 and the atom in G which corresponds to the selected atom in G. The result of resolving G and C1 using 1 is exactly G1. We obtain an unrestricted refutation of P{G} – which looks almost like the given refutation of P{G}. Now apply the mgu lemma. ISWeb - Information Systems & Semantic Web ISWeb - Information Systems & Semantic Web Sergej Sizov MOA meeting [email protected] 6 of 25 Steffen Staab Foundations of Logic Programming [email protected] 6 of 12 <is web> Success Set and Least Herbrand Model Theorem The success set of a definite program P is equal to its least Herbrand model. ISWeb - Information Systems & Semantic Web ISWeb - Information Systems & Semantic Web Sergej Sizov MOA meeting [email protected] 7 of 25 Steffen Staab Foundations of Logic Programming [email protected] 7 of 12 <is web> Proof : corollary (slide 24, previous slide set). : Show that the least Herbrand model of P is contained in the success set of P. Show per induction over n, that ATPn implies, that P{A} has a refutation and hence A is in the success set. Basis: ATP1 means that A is a ground instance of a unit clause of P. Thus there exists a refutation. ISWeb - Information Systems & Semantic Web ISWeb - Information Systems & Semantic Web Sergej Sizov MOA meeting [email protected] 8 of 25 Steffen Staab Foundations of Logic Programming [email protected] 8 of 12 <is web> Proof (continued) : Show that the least Herbrand model of P is contained in the success set of P. Show per induction over n, that ATPn implies, that P{A} has a refutation and hence A is in the success set. Inductive step: Hypothesis holds for n-1. Let ATPn. By the definition of TP, there exists a ground instance of a clause BB1,…,Bk such that A=B and {B1,…,Bk} TP(n-1) for some . By the induction hypothesis P{Bi} has a refutation for i=1,…,k. Because each Bi is ground these refutations can be combined into a refutation of P{(B1 …Bk)}. Thus P{A} has an unrestricted refutation and we can apply the mgu lemma to obtain a refutation of P{A}. ISWeb - Information Systems & Semantic Web ISWeb - Information Systems & Semantic Web Sergej Sizov MOA meeting [email protected] 9 of 25 Steffen Staab Foundations of Logic Programming [email protected] 9 of 12 <is web> Completeness - 1 Theorem Let P be a definite program and G be a definite goal. Suppose P{G} is unsatisfiable. Then there exists an SLD-refutation of P{G}. Proof Let G= A1,…,Ak. G is false wrt MP. Hence some ground instance Gist false wrt MP. Thus {A1,…,Ak} MP. Therefore there exists a refutation for each.Ai. Because Ai are ground, they can be combined to an SLD-refutation of G. By the lifting lemma, since there is an unrestricted SLDrefutation, we can also find a restricted SLD-refutation. ISWeb - Information Systems & Semantic Web ISWeb - Information Systems & Semantic Web Sergej Sizov MOA meeting [email protected] 10 of of 25Logic Programming Steffen Staab Foundations [email protected] 10 of 12 <is web> Completeness – 2: Every correct answer an instance of a computed answer Lemma Let P be a definite program and A an atom. Suppose (A) is a logical consequence of P, then there exists an SLD-refutation of P{A} with the identity substitution as the computed answer. Proof introduce new constants for all variables xi in A(={… xi/ai …}). Because of the premise P{A} has a refutation. Because A is ground the corresponding calculated answer is . Since the ai do not appear in P or A, we can keep the xi and obtain the calculated answer . ISWeb - Information Systems & Semantic Web ISWeb - Information Systems & Semantic Web Sergej Sizov MOA meeting [email protected] 11 of of 25Logic Programming Steffen Staab Foundations [email protected] 11 of 12 <is web> Completeness – 2: Every correct answer an instance of a computed answer Theorem Let P be a definite Program and G a definite goal. For every correct answer for P{G} there exists a computed answer for P{G} and a substitution such that and have the same effect on all variables in G. Proof sketch Let G=A1,…,Ak. Since is correct,((A1… Ak)) is a logical consequence. Hence there exists a SLD-refutation for P{ Ai} with as calculated answer. Thus there exists a SLD-refutation for P{(A1… Ak)} with as calculated answer. Let the composed mgu's be 1…n. By the lifting lemma we have: 1…n=‘1…‘n with mgu's ‘1…‘n for the refutation of P{G}. ISWeb - Information For this reason we can specify Systems & Semantic Web ISWeb - Information Systems & Semantic Web Sergej Sizov MOA meeting [email protected] 12 of of 25Logic Programming Steffen Staab Foundations [email protected] 12 of 12