[Colloquium] LOGIC/THEORY SEMINARS TODAY: Yuri Gurevich

[Katie Casey]

DEPARTMENT OF COMPUTER SCIENCE

UNIVERSITY OF CHICAGO

Date: Friday, September 24, 2010
Place: Ryerson 277, 1100 East 58th Street

LECTURE 1:

Time: 1:30

Title:  Do Teach Logic

Abstract:

In the software industry engineers do formal logic day in and day out,
even though they may not realize that. It is ironic and silly that
software engineers spend a lot of time studying calculus that they do
not use, and do not study logic that they do use. This logician,
turned computer scientist, spent last twelve years at Microsoft. I'll
try to illustrate why logic is so relevant and why it is so hard for
software engineers to pick it up.

RECEPTION: 2:30-3:30, Ryerson 255

LECTURE 2:

Date: Friday, September 24, 2010 
Time: 3:30 p.m.
Place: Ryerson 277, 1100 E. 58th Street

----------------------------------------------

Speaker:		Yuri Gurevich

From:		Microsoft Research

Web page:	 http://research.microsoft.com/en-us/um/people/gurevich/  

Title: 		Linear Time Reasoning

Abstract:  	

Software industry is a great application area for mathematical logic. Consider for example a scenario where various principals (governments, government agencies, various institutions, individuals) interact and where trust is in short supply. Each principal computes "his" own knowledge, and the whole system maintains certain properties, e.g. patients' privacy is preserved in a health-related scenario. To facilitate such interactions, we designed and implemented the Distributed Knowledge Authorization Language.

Often local computation should be done very efficiently, ideally in linear time (with a reasonable linearity coefficient). But what, if anything, can you do in linear time? Even the sorting of n items requires n x log(n) time. Consider the derivability problem for a fixed logic: decide whether a given set of hypotheses entails a given formula (the query). A typical proof cannot be even written down in linear time. In this connection, we developed a so-called primal infon logic (loosely based on constructive/intuitionistic principles). The problem of interest to us is Multiple Derivability: given a set of hypotheses and a set of queries, determine which of the queries follow from the hypotheses. It turns out that the multiple derivability problem for primal infon logic is solvable in linear time.

We will attempt to make the talk self-contained.

Bio:

Yuri Gurevich is Principal Researcher at Microsoft. He is also Prof. Emeritus at the University of Michigan, ACM Fellow, Guggenheim Fellow, a member of Academia Europaea, and Dr. Honoris Causa of a Belgian and Russian universities.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20100924/f8fb4b1f/attachment.htm