Seminar: September 24, 3:30pm, Room 277

Yuri Gurevich, Microsoft Research

Linear Time Reasoning

Note non-standard day, time and place!

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.