CONCURRENT DEDUCTION: CLASSICAL AND MODAL
Jim Cunningham · 1993
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. 1. Background An automated tableau theorem prover was developed for the UK Forest project first order modal action logic in order to demonstrate industrial applications in validating specifictions rather than mathematically interesting theorems. It has been used to prove properties safety-critical specifications for systems of non-trivial size, without being adequate for systems of full industrial scale (see, for example Atkinson and Cunningham 11991]). While the full battery of mechanised deduction methods with sorting, theory unification etc., would undoubtedly have provided further enhancement for this system, there seemed to be an underlying need for a "divide and rule " approach which will reduce deep problems into small shallow parts. Motivated by this we re-explored the salient work of Nelson and Oppen [1979] on co-operating decision processes. As a consequence we were able to discover, in turn, a simple new procedure for co-operating classical tableaux, and on further analysis, a comparable procedure for concurrent action tableau which had previously been elusive. Our interests in mechanising a richer class of multi-modal logics let to the creation of a European Esprit project (Medlar). While we report elsewhere on the work of the Medlar project