View Full Document


Unformatted text preview:

Proof Sketches Discussion Robert Veroff Computer Science Department University of New Mexico ADAM 2007 June 21 23 2007 1 Hierarchy of Theories Let Ai be an independent set of axioms for theory Ti Say have A1 A2 A3 and assume same inference rules T1 T2 T3 theorems Example lattice hierarchy LT CL OL OML MOL BA Can knowledge about theories T1 and T3 help us prove theorems in theory T2 Two ideas about picking given clauses semantics consider models in T1 proof sketches consider proofs in T3 2 Proof Sketches Consider a derivation as a sequence of clauses C1 C2 Ci Cj Cn where Ci is an extra assumption wrt the target theory derived clause Cj has Ci in its derivation history Cj either is in the target theory or it is not if yes it suffices to find a new derivation of Cj if not it suffices to bridge the gap In either case we ve reduced a large problem to a smaller but still potentially difficult problem 3 Theory of Proof Sketches Is there something interesting going on here or is this just an AR hacker s heuristic that happens to have a great track record Operational view What makes a good theorem Can we presume that there is some regularity and structure to known theories and to the results of interest Probabilistic view Of the space of all available clauses with no other prior information it seems reasonable to focus on clauses that have shown value previously 4 Example http www cs unm edu veroff LOOPS basarab html 5

Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...

Join to view Hierarchy of Theories and access 3M+ class-specific study document.

We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Hierarchy of Theories and access 3M+ class-specific study document.


By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?