Tool support for reasoning in display calculi

TL;DR

This paper introduces a versatile tool for reasoning in complex propositional sequent calculi, exemplified by dynamic epistemic logic, with formal proof support and adaptable features for various calculi.

Contribution

It provides a new tool supporting reasoning in large, rule-rich calculi, embedding in Isabelle, and adaptable meta-tools for user-defined calculi.

Findings

Successfully formalized the muddy children puzzle for any number of children.

Implemented display calculus D.EAK within the tool.

Demonstrated the tool's ability to handle calculi with over a hundred rules.

Abstract

We present a tool for reasoning in and about propositional sequent calculi. One aim is to support reasoning in calculi that contain a hundred rules or more, so that even relatively small pen and paper derivations become tedious and error prone. As an example, we implement the display calculus D.EAK of dynamic epistemic logic. Second, we provide embeddings of the calculus in the theorem prover Isabelle for formalising proofs about D.EAK. As a case study we show that the solution of the muddy children puzzle is derivable for any number of muddy children. Third, there is a set of meta-tools, that allows us to adapt the tool for a wide variety of user defined calculi.