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