Automatic soundness check of sequent-style (and Hilbert-style) rules
Written on February 5, 2026
I present in this post a tool to check soundness of sequent-style rules (and Hilbert-style, in particular) with respect to a family of (deterministic) logical matrices over the same algebra (i.e., it allows to specify multiple sets of designated values). In order to run the tool, you only need to install Docker. The logical matrix and the rules to be checked are specified in an yaml file. The file is then submitted to the tool by a command-line interface.