Algorithmic correspondence and analytic rules

TL;DR

This paper presents MASSA, an algorithm that generates geometric rules and cut-free proofs for modal formulas, effectively bridging modal logic and first-order correspondence through an automated, terminating process for inductive formulas.

Contribution

The paper introduces MASSA, an innovative algorithm that automates the generation of geometric rules and proofs for a broad class of modal formulas, extending to quantified modal logic.

Findings

MASSA terminates successfully for definite analytic inductive formulas.

The geometric axioms produced are equivalent to first-order correspondents.

The SCAN algorithm for quantifier elimination is complete for inductive analytic formulas.

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.