[ont.events] U of Toronto Computer Science activities, April 24-28

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