Algorithmic correspondence and analytic rules

Authors Andrea de Domenico, Giuseppe Greco

Publication date 26 March 2022

Modal logic (including the logic of norms) (03B45) Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05)

arXiv classification

cs.LO math.LO

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.

This page was built for publication: Algorithmic correspondence and analytic rules

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6394783)