TY - JOUR
T1 - Polynomial-time checking of generalized Sahlqvist syntactic shape
AU - Manoorkar, Krishna B.
AU - Palmigiano, Alessandra
AU - Panettiere, Mattia
N1 - Publisher Copyright:
© 2024 The Author(s)
PY - 2024/12/21
Y1 - 2024/12/21
N2 - The best known modal logics are axiomatized by Sahlqvist axioms, i.e., axioms of a syntactic shape which guarantees these formulas to have such excellent properties as canonicity and elementarity. Recently, the definition of Sahlqvist formulas has been generalized and extended from formulas in classical modal logic to inequalities (sequents) in a wide family of logics known as LE-logics. We introduce an algorithm which checks if a given inequality is generalized Sahlqvist in polynomial time.
AB - The best known modal logics are axiomatized by Sahlqvist axioms, i.e., axioms of a syntactic shape which guarantees these formulas to have such excellent properties as canonicity and elementarity. Recently, the definition of Sahlqvist formulas has been generalized and extended from formulas in classical modal logic to inequalities (sequents) in a wide family of logics known as LE-logics. We introduce an algorithm which checks if a given inequality is generalized Sahlqvist in polynomial time.
KW - Algorithmic correspondence theory
KW - Inductive formulas
KW - Modal logic
KW - Non-classical logics
KW - Sahlqvist formulas
UR - http://www.scopus.com/inward/record.url?scp=85204366460&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85204366460&partnerID=8YFLogxK
U2 - 10.1016/j.tcs.2024.114875
DO - 10.1016/j.tcs.2024.114875
M3 - Article
AN - SCOPUS:85204366460
SN - 0304-3975
VL - 1021
JO - Theoretical Computer Science
JF - Theoretical Computer Science
M1 - 114875
ER -