5 papers · 1 filter
Refutation calculi for lattice-based logics: from display to tableaux
Andrea De Domenico, Giuseppe Greco, Alessandra Palmigiano +2
Refutation calculi are formal systems developed to derive the invalid formulas of a given logic. While the notion of refutation calculi has played a key role in the development of…
Inception Display Calculi
Andrea De Domenico, Giuseppe Greco, Alessandra Palmigiano
Display calculi were introduced by Nuel Belnap in `Display logic' (1982) as a natural extension of Gentzen's sequent calculi, as a uniform and modular framework capable of encompas…
Modular constructive Lyndon interpolation for nondistributive logics
Andrea De Domenico, Giuseppe Greco, Alessandra Palmigiano +1
We establish the Lyndon interpolation property for basic lattice expansion logics (LE-logics) in arbitrary signatures using display calculi. Our approach is constructive, yielding…
Algorithmic correspondence and analytic rules
Andrea De Domenico, Giuseppe Greco, Alessandra Palmigiano
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…
Non-distributive description logic
Ineke van der Berg, Andrea De Domenico, Giuseppe Greco +3
We define LE-ALC, a generalization of the description logic ALC based on the propositional logic of general (i.e. not necessarily distributive) lattices, and semantically interpret…