Algorithmic Correspondence and Canonicity for Distributive Modal Logic, in preparation

Sahlqvist’s theorem [1] identifies a large, syntactically specified class of modal formulas which are canonical and also locally elementary on Kripke frames. Via the well known duality theory linking frames and Boolean algebras with operators (BAO’s), this result can be equivalently reformulated in the purely algebraic setting of canonical extensions. This perspective immediately suggests generalizations of Sahlqvist’s theorem along algebraic lines, e.g., to the cases of distributive [2] or arbitrary lattices with operators. We give a brief overview of Sahlqvist theory for modal logic (with BAO-based semantics) and distributive modal logic (with distributive lattice-based seman-tics) and also discuss the appropriate duality with the relational semantics. We formulate a distributive modal logic analogue of Goranko and Vakarelov’s in-ductive formulas [3]. Next we present the newly developed algorithm ALBA [4] which effectively captures these results via a handful of syntactic transformation rules exploiting the residuation of (dual) operators and some other properties of perfect distributive lattices