Polynomial-time checking of generalized Sahlqvist syntactic shape

Krishna B. Manoorkar; Alessandra Palmigiano; Mattia Panettiere

doi:10.1016/j.tcs.2024.114875

Polynomial-time checking of generalized Sahlqvist syntactic shape

Krishna B. Manoorkar, Alessandra Palmigiano, Mattia Panettiere^*

^*Corresponding author for this work

Ethics, Governance and Society

Research output: Contribution to Journal › Article › Academic › peer-review

Abstract

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.

Original language	English
Article number	114875
Pages (from-to)	1-17
Number of pages	17
Journal	Theoretical Computer Science
Volume	1021
Early online date	18 Sept 2024
DOIs	https://doi.org/10.1016/j.tcs.2024.114875
Publication status	E-pub ahead of print - 18 Sept 2024

Bibliographical note

Publisher Copyright:
© 2024 The Author(s)

Keywords

Algorithmic correspondence theory
Inductive formulas
Modal logic
Non-classical logics
Sahlqvist formulas

Access to Document

10.1016/j.tcs.2024.114875

Persistent URL (handle)

Copy link address

Cite this

@article{91fb18715dfd438584d29a614e693b56,

title = "Polynomial-time checking of generalized Sahlqvist syntactic shape",

abstract = "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.",

keywords = "Algorithmic correspondence theory, Inductive formulas, Modal logic, Non-classical logics, Sahlqvist formulas",

author = "Manoorkar, {Krishna B.} and Alessandra Palmigiano and Mattia Panettiere",

note = "Publisher Copyright: {\textcopyright} 2024 The Author(s)",

year = "2024",

month = sep,

day = "18",

doi = "10.1016/j.tcs.2024.114875",

language = "English",

volume = "1021",

pages = "1--17",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier",

}

TY - JOUR

T1 - Polynomial-time checking of generalized Sahlqvist syntactic shape

AU - Manoorkar, Krishna B.

AU - Palmigiano, Alessandra

AU - Panettiere, Mattia

PY - 2024/9/18

Y1 - 2024/9/18

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

SP - 1

EP - 17

JO - Theoretical Computer Science

JF - Theoretical Computer Science

M1 - 114875

ER -

Polynomial-time checking of generalized Sahlqvist syntactic shape

Abstract

Bibliographical note

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this