Concurrent Deduction: Classical and Modal

Contents

We provide an informal report of work seeking to introduce concurrency into deduction by exploiting modularity. The work arose in the context of a theorem prover for an applied modal action logic, has led to the re-discovery and generalisation of earlier work by Nelson and Oppen and promises a fibered approach to deduction in multi-modal representations of rationality.