Incorporating Specialized Algorithms into General Inference ProceduresMotivating ExampleSpeed of EpilogSpeed of SubroutineOverall ApproachExampleProof vs. ComputationUniversal AttachmentsPeano Axioms?Filter SetsFormalizationRule of InferenceUAR Rule of InferenceC-FOLC-FOL SyntaxExamplesC-FOL SemanticsC-FOL InferenceSlide 19Slide 20Algorithm DefinitionsAlgorithm = Logic + ControlA = L + C exampleMotivating L+CUse Logic to Improve EfficiencyUse Control to Improve EfficiencyLogic: Horn ClausesControl: Embedded in Proof ProceduresExample ProblemExample ExecutionData structuresQuicksort With Data StructureA = L + C SummaryIssuesFormulation 1Formulation 2ConclusionsIncorporating Specialized Algorithms into General Inference ProceduresRelational LogicMotivating ExampleSet intersectionBBBBBAAAAABAxBxAxx∈∈∈∈∈∈∈∈∈∈∩∈⇒∈∧∈∀6,5,4,3,25,4,3,2,1).(Speed of EpilogEpilog(in ?x AintB) <= (in ?x A) ^ (in ?x B) (in 1 A) ^ (in 2 A) ^ (in 3 A) ^ (in 4 A) ^ (in 5 A)(in 2 B) ^ (in 3 B) ^ (in 4 B) ^ (in 5 B) ^ (in 6 B)Goal: (in ?x AintB)Epilog takes at O(m*n) steps to find AintBSpeed of SubroutinePseudo-codefunction set_intersect (Set A, Set B){ MarkingDS m; Set AintB; foreach item in A {m.mark(item); } foreach item in B { if (m.marked(item)) AintB.add(item); } return AintB;}set-intersect takes O(m+n) steps to find AintBOverall ApproachIn order to solve problems efficiently, let’s give our theorem prover a set of data structures and hard-coded subroutines. We need to do the following:1. Describe the subroutines/data structures in the language of the theorem prover 2. Recognize when to apply thema.) when able—taken care of by #1b.) when appropriate—Algorithm analysis3. Apply the subroutines/data structuresExample1. <~(in x A), ~(in x B), (in x AintB)> P2. <(in 5 A)> P3. <(in 5 B)> P4. <(in 6 A)> P5. <(in 6 B)> P6. <(in 7 A)> P7. <~(in x AintB), goal(x)> Goal8. Recognize we can use set intersection routine to eliminate ~(in x AintB) by binding x to 5 and 6.9. <goal(5)> 7,?10. <goal(6)> 7,?Proof vs. Computation•Proof: solutions derived from logical deduction. Use model elimination, resolution, etc. to create a proof system.•Computation: solutions derived from the use of data structures and specialized procedures. Use a programming language, a compiler, and a computer to create a computation system.Universal AttachmentsExample arithmetic: {plus(3,4)=7}In general, we either need all addition facts or we need to specify the axioms for addition (Peano). 1. Zero is a number.2. If a is a number, the successor of a is a number.3. zero is not the successor of a number.4. Two numbers of which the successors are equal are themselves equal.5. (induction axiom.) If a set S of numbers contains zero and also the successor of every number in S, then every number is in S.Peano Axioms?•Computers add really fast. Why not use the built in +?•Universal Attachment for plus(x,y)plus(x,y) <+, Aint, Dint>Aint([x,y]) = [num(x), num(y)] (attachment map)Dint(n) = num-1(n) (detachment map)num maps “1” to 1, “2” to 2, “3” to 3, etc.•When we see “plus(3,4)”, we now know to ask the CPU for 3+4.Filter Sets•Not all symbols can be converted to numbers. The domain of plus(x,y) <+, Aint, Dint> is too large.•F = {type(x,integer), type(y,integer)}The above universal attachment only applies if all the constraints in F are satisfied. <plus(x,y), F> <+, Aint, Dint>Aint([x,y]) = [num(x), num(y)] (attachment map)Dint(n) = num-1(n) (detachment map)num maps “1” to 1, “2” to 2, “3” to 3, etc.F = {type(x,integer), type(y,integer)}Formalization>>→<< DApFxxn,,],,...,[1φUniversal Attachment:],,...,[1 nxxφthe attachment pattern ( plus(x,y) )F, the filter set, defined for x1,…,xnp, the attached program of arity mA, (logical ground terms)n(computer terms)mD, (computer terms)(logical expression)Rule of InferenceAttachment for a pattern {p(x)}•{p(x)} Yes•{p(x), q(x)} No({p(x)} might evaluate to false {q(x)})•{p(x), r, t(y)} Yes•{~p(a)} YesAttachment for a pattern {h(x,y)}•{h(x,x), R} No),Attach( is ,][][φδφΘΘppUAR Rule of Inference•Universal Attachment for Resolution (resolution is sound when augmented with UAR, but incomplete)}{]},...,,,...,[{ ],...,,,...,[....Q quantified and simple is ],...,[ .3}{]},...,,,...,[{ ],...,,,...,[....Q quantified and simple is ],...,[ 2.]}[{]]},...,[[{ instance predicateor functiona is ],...,[ 1.1111111111111111Θ¬∪Ψ¬∪ΨΘ∪Ψ∪ΨΘ∪∪CttssCxxzzzQzxxCttssCxxzzzQzxxLCttLCxxnknkkknnknkkknnnφφφφC-FOL1. Computational First Order Logic – Sikka, 19962. Combines a proof system (FOL) and a computational system (C)3. Syntax4. Semantics5. Inference methodC-FOL Syntax•Start with Relational (First-order) Logic•Add a set of procedure names, P, that correspond to the specialized procedures in C•Add a set of data structure names, D, that correspond to the data structures in C•Add a new function symbol apply.•Add tr: (logical ground term) D tr-1: D (logical ground term)•Add maps(x,y): (ground term x D)maps-1(x,y): (D x ground term)Examples))(),(()(. .2""),,(),(. .1xfactorialxfactapplyxnumberxTrueyxapplyyxgreateryx=⇒∀=>⇔∀∀What if x is Mike’sAge?))()))(,((( ))((. .21xfactorialxtrfactapplytrxtrnumberx=⇒∀−C-FOL Semantics•Start with Relational (First-order) semantics•Each member of P corresponds to a specialized procedure in C.•Each member of D corresponds to a data structure in C. •apply(p,t1,…,tn) is a function mapped to the result of applying the procedure in C corresponding to p with the arguments t1,…,tn.•tr maps every ground term in FOL into a data structure in C•maps(x,y)relates a ground term in FOL to a data structure in CC-FOL Inference•Start with resolution and paramodulation•Add C-substitution}},...,),...,,({,...,{})...],...,,...,,([...,...,{1111nrnnntttpapplyttpapplyφφφφφφ←• Theorem: Sound and complete system• Theorem: More powerful (general) than Universal attachmentsExample1. {~p(x,z), ~p(y,z), p(plus(x,y),z)} P2. {p(3,2)} P3. {p(4,2)} P4. {~p(7,2)}Goal5. {plus(x,y) = apply(+,x,y)} SP6. {~p(y,2), p(plus(3, y), 2)} 1,27. {p(plus(3, 4), 2)} 6,38. {p(apply(+, 3, 4), 2)} 7,59. {p(7,2)} 810. {}9,4Overall ApproachIn order to solve problems efficiently, let’s give our theorem prover a set of data structures and hard-coded subroutines. We need to do the following:1.
View Full Document
Unlocking...