clarke@csri.toronto.edu (Jim Clarke) (04/11/89)
ACTIVITIES FOR THE WEEK COMMENCING APRIL 24, 1989 (GB = Galbraith Building, 35 St. George Street) (SF = Sandford Fleming Building, 10 King's College Road) SUMMARY: GRAPHICS SEMINAR - Tues., Apr. 25, 3 p.m. in GB 120 -- F. Javier Lerch "Skilled Financial Planning: The Cost of Translating Ideas into Action" AI SEMINAR - Thurs., Apr. 27, 11 a.m. in SF 1105 -- Charles Elkan "Automated Inductive Reasoning about Logic Programs" THEORY/SYSTEMS SEMINAR - Thurs., Apr. 27, 3 p.m. in GB 244 -- Amotz Bar-Noy "Compact Distributed Data Structures for Adaptive Routing" ---------------------- GRAPHICS SEMINAR - Tuesday, April 25, 3 p.m. in Room GB 120 F. Javier Lerch Carnegie-Mellon University "Skilled Financial Planning: The Cost of Translating Ideas into Action" We use GOMS models to predict error rates and mental times for translating financial concepts into equations in two widely used interface representations. The first of these, common to spreadsheet packages, is characterized by non-mnemonic naming and absolute referencing of variables. The second, common to non- procedural command-driven software, is characterized by mnemonic naming conventions and relative referencing of variables. These predictions were tested in an experiment using experienced financial analysts. Although the interface that allows mnemonic and relative names (called keyword) takes longer overall, it produces seventy-five percent fewer simple errors and requires less mental effort. Given the overall serious cost of errors in financial models, we conclude that interfaces having the keyword representation are far superior. AI SEMINAR - Thursday, April 27, 11 a.m. in Room SF 1105 Charles Elkan Cornell University "Automated Inductive Reasoning about Logic Programs" The aim of my work is to construct a powerful tool for verifying properties of pure logic programs. There are two central research issues. The first is how to invent useful induction hypotheses--ones that allow proofs to go through. The second is how to constrain search during the first-order reasoning required to finish a proof. I shall describe how these issues are resolved in the prototype verifier that I have implemented. Induction hypotheses are obtained by a technique based directly on the semantics of pure logic programs. This method produces hypotheses that can implicitly apply many different well-founded orders. Traditional inductive theorem-provers use heuristics to select an induction hypothesis that embodies one particular well-founded order in advance of the remainder of a proof. Search is limited by a focusing mechanism. After establishing induction hypotheses, the verifier fixes a set of terms of interest and performs forward chaining until all facts true of those terms have been found that are provable without introducing other terms. The verifier has heuristics for choosing focus terms that are likely to be relevant. A useless focus term does not increase the forward chaining search space exorbitantly, so these heuristics need not be perfect to be successful. THEORY/SYSTEMS SEMINAR - Thursday, April 27, 3 p.m. in Room GB 244 Amotz Bar-Noy Stanford University "Compact Distributed Data Structures for Adaptive Routing" In designing a routing scheme for a communication network it is desirable to use as short as possible paths for routing messages, while keeping the routing information stored in the processors' local memory as succinct as possible. The efficiency of a routing scheme is measured in terms of its stretch factor - the maximum ratio between the cost of a route computed by the scheme and that of a cheapest path connecting the same pair of vertices. This paper presents a family of adaptive routing schemes for general networks. The hierarchical schemes HSk (for every fixed k >= 1) guarantee a stretch factor of O((k2)(3k)) and require storing at most O(k(n^3)/(k log n)) bits of routing information per vertex. The new important features of these schemes, which make them appropriate for adaptive use, are +o applicability to arbitrary networks with arbitrary edge costs, +o name-independence, i.e., usage of original (user-selected) routing labels, +o a balanced distribution of the memory, +o an efficient on-line distributed preprocessing algorithm. (Joint work with Baruch Awerbuch, Nathan Linial and David Peleg.) -- Jim Clarke -- Dept. of Computer Science, Univ. of Toronto, Canada M5S 1A4 (416) 978-4058 clarke@csri.toronto.edu or clarke@csri.utoronto.ca or ...!{uunet, pyramid, watmath, ubc-cs}!utai!utcsri!clarke