FJP

67 %
33 %
Information about FJP
Entertainment

Published on September 18, 2007

Author: Seasham

Source: authorstream.com

Identification in Inductive MetaLogic Programming:  Identification in Inductive MetaLogic Programming Akihiro Yamamoto Hokkaido University, JAPAN yamamoto@meme.hokudai.ac.jp Inverse of Deduction, Anti-Unification, and Inductive MetaLogic Programming:  Inverse of Deduction, Anti-Unification, and Inductive MetaLogic Programming Akihiro Yamamoto Hokkaido University, JAPAN yamamoto@meme.hokudai.ac.jp 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.

Add a comment

Related presentations

Related pages

fjp>media

Wenn du dich für Jugendmedien interessierst oder selbst junger Journalist bist, hast du genau die richtige Webseite gefunden. Denn fjp>media ist der ...
Read more

termine | fjp>media

04. Dezember 2016, 11:00 Uhr bis etwa 13:00 Uhr in Magdeburg. Das Jahr 2016 neigt sich dem Ende zu und somit auch die Wahlperiode des Vorstandes von fjp>media.
Read more

FJP Supply

We offer custom doors, mouldings, stair parts, showers, mirrors and hardware. Call us today for more info!
Read more

FJP | Facebook

J U L I A. manchmal fühlt man sich in gewissen situationen eingeengt und man möchte sich einfach nur zurück ziehen. welche story steckt für euch in ...
Read more

FJP - Fotos & Bilder - Fotograf aus Nürnberg, Deutschland ...

Alle Fotos & Bilder von FJP + kostenlos bei fotocommunity.de anschauen ᐅ Die besten Bilder von FJP ansehen
Read more

Freedom and Justice Party (Egypt) - Wikipedia

The Freedom and Justice Party (FJP) (Arabic: حزب الحرية والعدالة ‎, translit. Ḥizb al-Ḥurriya wa al-’Adala ‎) is an Egyptian ...
Read more

FJP | Facebook

Message this Page, learn about upcoming events and more. If you don't have a Facebook account, you can create one to see more of this Page.
Read more

FJP | Photographer | Sedcards | model-kartei.de

Photographer FJP from 90556 Seukendorf in Germany ... =11.111111640930176pxMein Name ist Florian J. Röder, 28 Jahre, komme aus der wunderschönen Stadt ...
Read more

fjp.mg.gov.br - Página principal

A Fundação João Pinheiro está com inscrições abertas para cinco cursos a distância com início previsto para os meses de outubro e novembro: Gênero ...
Read more

Fjp - We Account For Your Future!

Certified General Accountant speacilizing in corporate accounting and tax planning.
Read more