Maude as a Platform for Designing and Implementing Deep Inference Systems

Deep inference is a proof theoretical methodology that generalizes the traditional notion of inference in the sequent calculus: in contrast to the sequent calculus, the deductive systems with deep inference do not rely on the notion of main connective, and permit the application of the inference rules at any depth inside logical expressions, in a way which resembles the application of term rewriting rules. Deep inference provides a richer combinatoric analysis of proofs for different logics. In particular, construction of exponentially shorter proofs becomes possible. In this paper, aiming at the development of computation as proof search tools, we propose the Maude language as a means for designing and implementing different deep inference deductive systems and proof strategies that work on these systems. We give Maude implementations of deep inference systems together with an implementation that simulates sequent calculus proofs to serve as a benchmark. We demonstrate these ideas on classical logic, and argue that they can be analogously carried to other deep inference systems for other logics, as well as sequent calculus systems.