[ont.events] U of Toronto Computer Science activities, January 26-30

clarke@utcsri.UUCP (Jim Clarke) (01/16/87)

         (SF = Sandford Fleming Building, 10 King's College Road)
              (GB = Galbraith Building, 35 St. George Street)

SUMMARY:
Tuesday, January 27, 11 am, SF1101:  P.W. Dymond
               ``Speeding up computations using parallelism"

Tuesday, January 27, 3 pm, GB120:  Wikto Marek
          ``On the Logic and Combinatorics of Rule-Based Systems"

Thursday, January 29, 3 pm, GB220:  Shai Ben-David
          ``A Knowledge Theory Approach to Distributed Protocols"


COLLOQUIUM, Tuesday, January 27, 11 am, SF1101

                           Professor P.W. Dymond
                           University of Toronto

               ``Speeding up computations using parallelism"

     Parallel machines offer the hope of substantial speedups over the best
performance on sequential machines.  Under what circumstances can this hope
be realized?  Some general schemes for obtaining speedups of sequential
computations will be presented, and recent research aimed at the formula-
tion of the complexity theory of parallel computation will be described.

A.I. SEMINAR, Tuesday, January 27, 3 pm, GB120

                           Professor Wikto Marek
                          University of Kentucky

          ``On the Logic and Combinatorics of Rule-Based Systems"

     We discuss some basic issues of rule-based expert systems, their logic
and the main complexity issues related to the algorithms of deciding the
consistency and completeness of such systems.  In addition, we study the
connections to the theory of non-first normal form relational databases and
find applications of our theory to non-first normal form relations.

SYSTEMS/THEORY SEMINAR, Thursday, January 29, 3 pm, GB220

                         Professor Shai Ben-David
                           University of Toronto

          ``A Knowledge Theory Approach to Distributed Protocols"

     There are two prominent aspects of proofs, the first one, of course,
is that a proof validates a statement.  Yet there might be another aspect:
a proof is a way to convey ideas and to explain why things work.  The
existing proofs for the correctness of distributed protocols have sometimes
either of these properties but never both.  In most cases the protocols are
presented with a hand waiving explanation, on the other hand the methods
available to guarantee correctness are basically correctness checkers.
There is a need for a way to present intuitive proofs in such a form that
can easily be altered to formal proofs if need arises.  Towards this aim we
develop a `knowledge theory' for distributed systems.  We formalize a ver-
sion of model logic that enables reasoning about what a process knows and
how this knowledge is communicated and changed along a run of the system.

     We demonstrate our machinery by producing `better' correctness proofs
for protocols for the critical section problems.
-- 

Jim Clarke -- Dept. of Computer Science, Univ. of Toronto, Canada M5S 1A4
              (416) 978-4058
{allegra,cornell,decvax,linus,utzoo}!utcsri!clarke