FJP

Information about FJP

Published on September 18, 2007

Author: Seasham

Source: authorstream.com

Content

Identification in Inductive MetaLogic Programming:  Identification in Inductive MetaLogic Programming Akihiro Yamamoto Hokkaido University, JAPAN [email protected] Inverse of Deduction, Anti-Unification, and Inductive MetaLogic Programming:  Inverse of Deduction, Anti-Unification, and Inductive MetaLogic Programming Akihiro Yamamoto Hokkaido University, JAPAN [email protected] Motivation:  Motivation 'How can mathematical (deductive) logic be used in formalizing inductive logic?' Why? Justification of inference (generation of Hypotheses) with logic Inference from non-numerical data Use of background theories represented in logical formulae Inverse of Deduction for CNFs:  Inverse of Deduction for CNFs Using CNFs:  Using CNFs CNFs are useful. In propositional logic, the set of all models of a formula can be represented DNF or CNF. In first order case, Herbrand Theorem helps up to lift up the theory of CNF (DNF). CNFs are very popular in CS and AI, and some other mechanisms (e.g. abduction) proposed in AI can be merged into our theory [Yamamoto]. Definition and Example:  Definition and Example B : a CNF as a background theory E : a CNF as a set of examples s.t. B |- E A correct hypothesis of HFP(B, E) is a CNF s.t. B Ù H |- E. B = (Pet ¬ Cat) Ù(Pet ¬ Dog ) Ù(Cuddly ¬ Small, Fluffy, Pet) E = Cuddly ¬ Cat, Fluffy H = Small ¬ Pet Basic strategy for solving HFP:  Basic strategy for solving HFP B Ù H |= E Û H |= Ø (B Ù Ø E ) Note : The negation of a CNF is not always a CNF, but easily transformed into a DNF. Residue Hypothesis [Yamamoto et al]:  Residue Hypothesis [Yamamoto et al] Res(T) : The residue of a CNF T is a CNF obtained by transforming Ø T into CNF and then deleting all tautological clauses from it. B : a clausal theory, E : a clausal theory The residue hypothesis for HFP(B, E) is Res(B Ù Res(E)). Prop. For any correct hypothesis H, H |- Res(B Ù Res (E)) Example 1:  Example 1 B = (Pet ¬ Cat) Ù(Pet ¬ Dog ) Ù(Cuddly ¬ Small, Fluffy) E = Cuddly ¬ Cat, Fluffy H = Small ¬ Pet Res(B Ù Res(E)) = (ØPet Ú Dog Ú Small Ú ØFluffy Ú ØCat Ú Cuddly) Ù (ØPet Ú ØPet Ú Small Ú ØFluffy Ú ØCat Ú Cuddly) = (Small Ú Cuddly Ú Dog ¬ Pet Ù Fluffy Ù Cat ) Ù (Small Ú Cuddly ¬ Pet Ù Fluffy Ù Cat) = (Small Ú Cuddly ¬ Pet Ù Fluffy Ù Cat) Example 2:  Example 2 B = (Pet ¬ Cat) Ù(Black ¬ Dog) Ù(Cuddly ¬ Small Ù Fluffy) E = Cuddly ¬ Cat Ù Fluffy H = Small ¬ Pet Res(B Ù Res(E)) = (ØPet Ú Dog Ú Small Ú ØFluffy Ú ØCat Ú Cuddly) Ù (ØPet Ú ØBlack Ú Small Ú ØFluffy Ú ØCat Ú Cuddly) = (Small Ú Cuddly Ú Dog ¬ Pet Ù Fluffy Ù Cat ) Ù (Small Ú Cuddly ¬ Pet Ù Black Ù Fluffy Ù Cat) Inference rule for CNF:  Inference rule for CNF S : a CNF C : a clause L : a literal S Ù(C Ú L ) Ù (C Ú Ø L ) S Ù C Ù (C Ú L ) Ù (C Ú Ø L ) S Ù C S Ù C Ù (C Ú L ) S Ù C S Inverse of deduction:  Inverse of deduction Res(S) : (Small Ú Cuddly Ú Dog ¬ Pet, Fluffy, Cat) Ù (Small Ú Cuddly ¬ Pet, Black, Fluffy, Cat) H1 : (Cuddly ¬ Pet, Fluffy, Cat) Ù (Small Ú Cuddly ¬ Pet, Black, Fluffy, Cat) H2 : (Cuddly ¬ Pet, Fluffy, Cat) Ù (Cuddly ¬ Pet, Fluffy, Cat) = Cuddly ¬ Pet, Fluffy, Cat Problems in Practice:  Problems in Practice High complexity of computing Residue Hypotheses (#SAT) recovering hidden literals adding any clauses Rule Generation:  Rule Generation E1= fly(swallow) E2= fly(pigeon) E3= Øfly(ostrich) E4= Øfly(emu) B = Øsym-feather(swallow) Ù Øsym-feather(pigeon) Ù sym-feather(ostrich) Ù sym-feather(emu) H = Øsym-feather(x) ® fly(x) Ù sym-feather(x) ® Øfly(x) fly(archaeopteryx) 中華竜鳥,始祖鳥,孔子鳥… Example:  Example B = △x y z º △u v w ® ∠y =∠ v Ù A P = A P Ù ∠ P = 90 E = A B= A C ® ∠ B =∠ C H = x y = u v Ù x z = u w ∠z = 90 Ù ∠w = 90 ® △x y z º △u v w A B C P Residue in Predicate Logic:  Residue in Predicate Logic Herbrand’s Theorem  A conjunction of first order clauses S is unsatisfiable Û there is an unsatisfiable conjunction of clause T consisting of clauses in ground(S) Since Res(B Ù Res(E) is satisfiable, the residue hypotheses of any conjunction T of clauses from ground(Res(B Ù Res(E)) is a correct hypothesis. Example (cont’d):  B’ = △ABP º △ACP ® ∠B=∠C Ù A P = A P Ù ∠P = 90 Res(E) = Ø∠B =∠C Ù AB= AC Res(B’ Ù Res(E)) = AP = AP Ù ∠P=90 Ù AB= AC® △ABP º △ACP x y = u v Ù x z = u w Ù ∠z = 90 Ù ∠w = 90 ® △x y z º △u v w Example (cont’d) Residue Hypothesis:  Residue Hypothesis B : a clausal theory, E : a clausal theory For any clausal theory T consisting of clauses in ground(B Ù Res(E)), Res(T) is called a residue hypothesis for HFP(B, E). ground(S) T Inference rule for CNF:  Inference rule for CNF S : a CNF C : a clause L : a literal q : a substitution S Ù(C Ú L ) Ù (C Ú Ø L ) S Ù C Ù (C Ú L ) Ù (C Ú Ø L ) S Ù C S Ù C S Ù C Ù (C Ú L ) S Ù Cq S Ù C S Problems in Practice:  Problems in Practice High complexity of computing Residue Hypotheses (#SAT) recovering hidden literals adding any clauses selecting a set T consisting of clauses in ground(B Ù Res(E)) ILP Techniques:  ILP Techniques Some ILP techniques are considered as inverse of resolution B Ù H |- E  Û  B Ù Ø E |- Ø H 1. Derive B Ù Res(E) |- K   2. Then H= Res(K) Saturation [Sammut, Riouveiol, Angluin, Cohen, Arimura] The bottom method [Yamamoto 97], Inverse entailment [Muggleton95] Abduction [Poole, Inoue] Inverse Resolution and subsumption:  Inverse Resolution and subsumption Th[Yamamoto and Fronhoefer]. S, T : CNF T Î r (S ) Þ Res(S) Res(T) Subsumption of CNFs S Ù C S Ù C S Ù C Ù (C Ú L ) S Subsumption BY Resolution:  Subsumption BY Resolution B Ù Res(E) = S1 |- S2 |- ・ ・ ・ |- Sn-1 |- Sn Res(S1) = H1 H2 ・ ・ ・ Hn-1 Hn Res(S1) = H1 -| H2 -| ・ ・ ・ -| Hn-1 -| Hn Sk = L1 Ù L2 Ù ... Ù Lm  or Sk = L1 Ú L2 Ú ... Ú Lm Definite Induction:  Definite Induction B = (Pet ¬ Cat) Ù(Black ¬ Dog) Ù(Cuddly ¬ Small Ù Fluffy) E = Cuddly ¬ Cat Ù Fluffy H = Small ¬ Pet Ø E = Cat Ù Fluffy Ù (¬ Cuddly ) For positive literals B Ù Cat Ù Fluffy |- Pet, Cat, Fluffy Skipping and consequence:  Skipping and consequence SOLD = SLD + SOL = SLD + Skip [Inoue 92] Resolution á¬A1, ..., Ai, ..., Am | ¬H1, ..., Hnñ B0¬B1, ..., Bn á(¬A1, ..., B1, ..., Bk, ..., Am)q | ¬(H1, ..., Hn)q ñ Skip á¬A1 ,..., Ai ,..., Am | ¬H1,..., Hnñ á¬A1,..., ,..., Am | ¬H1,..., Hn , Ai ñ Slide26:  á ¬ cuddly | q ñ cuddly ¬ small, fluffy ¬ small, fluffy | q ñ á ¬ fluffy | ¬ smallñ fluffy¬ á q | ¬ smallñ B Ù ( ¬ Cuddly) |- ¬ small Analysis of Anti-Unification:  Analysis of Anti-Unification From HFP to Learning:  From HFP to Learning Given : a set of clauses as examples E1, E2,…, En, … In HFP the set is treated as CNF E1 Ù E2 Ù … Ù En and generate complete set of hypos. In learning one appropriate hypothesis must be chosen according to some criteria Least Generalization Approach:  Least Generalization Approach Generate a hypothesis Hn for En and then compute the least generalization of H1, H2,…, Hn if it exists. Anti-Unification:  Anti-Unification R.J. Popplestone said to G. Plotkin: 'Since unification is useful in automatic deduction, its dual might prove helpful for induction' The dual of unification is now called anti-unification or generalization Ex. The (most specific) anti-unification of p(a, f(a), f(f(a))), p(b, a, f(a)) is p(x, y, f(y)) Anti-unification Algorithm:  Anti-unification Algorithm áp(a, f(a), f(f(a))), p(b, a, f(a)) ñ áp(a, f(a), f(f(a))), p(b, a, f(a)) ñ áp(xa,b, f(a), f(f(a))), P(xa,b, a, f(a)) ñ áp(xa,b, xf(a),a, f(f(a))), P(xa,b, xf(a),a, f(a)) ñ áp(xa,b, xf(a),a, f(f(a))), P(xa,b, xf(a),a, f(a)) ñ áp(xa,b, xf(a),a, f(xf(a),a)), p(xa,b, xf(a),a, f(xf(a),a)) ñ p(x, y, f(y)) The AU case (cont’d):  The AU case (cont’d) Induction algorithm: the anti-unification algorithm p(x, y, z) p(f (x), y, z) p(x, y, f(z)) p(x, y, y) … p(x, y, f(y)) p(x, f(z), f(f(z))) p(b, y, f(y)) p(b, a, f(a)) p(a, f(a), f(f(a))) General Concrete Problems:  Problems The least generalization does not always exist if background theory is given. The least generalization for clauses exists. Finite number of minimally generalizations exist in some cases. Why least generalization? Logical explanation, if possible. Induction Algorithm:  Induction Algorithm M h1, h2, h3, ..., w1, w2, w3, ..., Hypotheses Examples Deductive Logic How is each hypothesis generated from example? How does the sequence of hypotheses acts? Identification in the limit[Gold]:  Identification in the limit[Gold] An algorithm M identifies concepts in a class U in the limit iff $N 'n andgt; N hn = i A class U of concepts can be identifiable iff $M s.t. M identifies concepts in a class U in the limit. M h1, h2, h3, ..., w1, w2, w3, ..., The AU case (cont’d):  The AU case (cont’d) Global criteria for successful inference identification in the limit For any input sequence for every concept L(A), the inference algorithm output a correct axiom A after finite change of hypotheses, and never change it afterwards. [Angluin] [Lassez Maher Marriot] M h1, h2, h3, ..., Aq1, Aq2, Aq3, ..., A Comparison 1:  Comparison 1 Subsumption relation could be interpreted as likelihood. Support set of a Hypothesis:  Support set of a Hypothesis The anti-unification algorithm shows an atomic formula can be represented with a finite set of examples. áp(a, f(a), f(f(a))), p(b, a, f(a)) ñ áp(a, f(a), f(f(a))), p(b, a, f(a)) ñ áp(xa,b, f(a), f(f(a))), P(xa,b, a, f(a)) ñ áp(xa,b, xf(a),a, f(f(a))), P(xa,b, xf(a),a, f(a)) ñ áp(xa,b, xf(a),a, f(f(a))), P(xa,b, xf(a),a, f(a)) ñ áp(x, y, f(y)) Comparison 2:  Comparison 2 Buchberger’s Algorithm can be regarded as learning Computational Algebra:  Computational Algebra Dicson’s Lemma (Hilbert’s Basis Theorem) Every ideal of monomial is finitely generated x m y n z k Þ (m, n, k) Computational Algebra:  Computational Algebra U : the class of ideals of commutative ring R with a unit. Prop[Stephan and Venstov 98]. T is a finite tell-tail of an ideal I iff T is a basis of I . Cor.  U is identifiable from texts. Û R is finitely generated. Û R is noetherian. Inductive MetaLogic Programming:  Inductive MetaLogic Programming Simple representation:  Simple representation Metalogic Programming[Bowen and Kowalski] P |- G Û Pdemo |- demo(P, G) Inductive Metalogic Programming [Hamfelt and Nillson 95] B Ù H |- E Û Pdemo |- demo(B Ù H , E) More precise representation:  More precise representation Metalogic Programming[Bowen and Kowalski] P |- G Û Pdemo |- demo(P, G) G = $ x1…xn A1…Am HFP Phyp Ù Pdemo |- $ x hyp(x) Ù demo(B Ù x, E) Idenitification Phyp Ù Pdemo Ù Ps |= $ x 'y ( hyp(x) Ù (s(y) ® (demo(B Ù x, y))) Learning as semantics:  Learning as semantics PP Ù Pq Ù Pr |= $ x 'y ( p(x) Ù (q(y) ® r(x, y)) P |= $ x 'y F(x, y) PP Ù Pq Ù Pr |- $ x 'y ( p(x) Ù (q(y) ® r(x, y)) P |- $ x 'y F(x, y) Procedural Semantics Examples:  Examples Anti-Unification Pterm Ù Pq Ù P= |= $ x 'y ( term(x) Ù (q(y) ® x = y)) The Least Element Pnat Ù Pq Ù Pless-equal |= $ x 'y ( nat(x) Ù (q(y) ® less-equal(x, y)) Replacing proving with learning:  Replacing proving with learning Robust Logic [Valiant] Rich Prolog (2) [Martin et al] LCM [Nakata and Hayashi] More simple and understandable semantics would be useful for extension of Logic Programming. Conclusion:  Conclusion Hypothesis Finding Problem combines logical aspects of induction and abduction shows their incompleteness is difficult because of the DNF -andgt; CNF transformation Anti-unification has good property of logic, statistics, algebra, and learning Conclusion:  Conclusion Inductive metalogic programming would be an extension of logic programming with the support of identification in the limit.

Related presentations


Other presentations created by Seasham

IBM
18. 09. 2007
0 views

IBM

CHEER LEADING
18. 06. 2007
0 views

CHEER LEADING

kano
18. 09. 2007
0 views

kano

14 ZIMBABWE Country Report
18. 09. 2007
0 views

14 ZIMBABWE Country Report

alphabetuppercase
18. 09. 2007
0 views

alphabetuppercase

Stewart Paulson
18. 09. 2007
0 views

Stewart Paulson

Conf2004 Consultant Smith MAI
18. 09. 2007
0 views

Conf2004 Consultant Smith MAI

03 Pole Mer
18. 09. 2007
0 views

03 Pole Mer

GCC2002 G JavaMPI
18. 09. 2007
0 views

GCC2002 G JavaMPI

Blue Whales
18. 09. 2007
0 views

Blue Whales

RDFIntro
18. 09. 2007
0 views

RDFIntro

All About Whales power point
18. 09. 2007
0 views

All About Whales power point

upload
18. 09. 2007
0 views

upload

vendor meeting 20051207
18. 09. 2007
0 views

vendor meeting 20051207

Complexity
18. 09. 2007
0 views

Complexity

BC 101 revised 2007
18. 09. 2007
0 views

BC 101 revised 2007

ossia
18. 09. 2007
0 views

ossia

palais 06
18. 09. 2007
0 views

palais 06

ibm stockholm
18. 09. 2007
0 views

ibm stockholm

Iron Overload Wells
18. 06. 2007
0 views

Iron Overload Wells

IPC Solutions Praesentation
18. 06. 2007
0 views

IPC Solutions Praesentation

D203 Sauers
18. 06. 2007
0 views

D203 Sauers

Concussion in Sports
18. 06. 2007
0 views

Concussion in Sports

colons
18. 06. 2007
0 views

colons

apostrophe
18. 06. 2007
0 views

apostrophe

istorija
18. 06. 2007
0 views

istorija

Creation of an Ancient Newspaper
15. 06. 2007
0 views

Creation of an Ancient Newspaper

coniferous Trees
15. 06. 2007
0 views

coniferous Trees

communities
15. 06. 2007
0 views

communities

columbus
15. 06. 2007
0 views

columbus

colorful utah
15. 06. 2007
0 views

colorful utah

chicks
15. 06. 2007
0 views

chicks

IR REBULL05
18. 06. 2007
0 views

IR REBULL05

1st Lego League presentation
18. 06. 2007
0 views

1st Lego League presentation

kincaid
18. 09. 2007
0 views

kincaid

introductory
18. 06. 2007
0 views

introductory

DITA Briefing3
18. 09. 2007
0 views

DITA Briefing3

bryllups invitasjon
18. 06. 2007
0 views

bryllups invitasjon