Algorithmic correspondence and analytic rules
Andrea De Domenico, Giuseppe Greco, Alessandra Palmigiano
TL;DR
The paper introduces MASSA, an algorithm that, for classical modal formulas, generates analytic geometric rules for the labelled calculus $G3K$ and corresponding cut-free derivations in the extended calculus. MASSA terminates and is correct for definite analytic inductive inputs, producing the exact first-order correspondents and analytic rule systems; its soundness is established by a close comparison with SCAN, which is shown to be complete for analytic inductive formulas. The work also demonstrates how SCAN can be extended to broader inductive settings and discusses extensions to quantified modal logic. Overall, MASSA provides a uniform, constructive method to bridge modal axioms with first-order frame conditions and corresponding analytic proof systems, with potential for broader applicability and future refinements.
Abstract
We introduce the algorithm MASSA which takes classical modal formulas in input, and, when successful, effectively generates: (a) (analytic) geometric rules of the labelled calculus G3K, and (b) cut-free derivations (of a certain `canonical' shape) of each given input formula in the geometric labelled calculus obtained by adding the rule in output to G3K. We show that MASSA successfully terminates whenever its input formula is a (definite) analytic inductive formula, in which case, the geometric axiom corresponding to the output rule is, modulo logical equivalence, the first-order correspondent of the input formula. In proving the correctness of MASSA, we also show that the algorithm for the elimination of second-order quantifiers SCAN is complete with respect to the class of inductive analytic formulas. Finally, we show how our algorithm can be extended to the class of inductive formulas and to modal logic with quantifiers.