September 30, 4 pm, AVW2120

How I Learned to Stop Worrying and Love the Box

Matthew Stone
University of Pennsylvania

In building an agent using logic, a basic danger is that to compute a needed conclusion may require an unreasonably large derivation. This talk explores ways this danger can be avoided by using modal logic as a specification language. The results of formalizing intuitions about agents and actions in modal logic can be regarded as providing declarative specifications of search control. When properly designed, these specifications can ensure that needed proofs will be compact, so that proofs are easily discovered and search spaces easily exhausted by automatic methods. As an illustration, we consider describing, in modal logic, the evolving computational state of an agent that can only take limited information into account. Such descriptions specify transparently correct computations, but can yield exponential reductions in the (worst-case) size of proofs by repeatedly using stored computations and by resolving multiple ambiguities modularly in separate parts of a proof.