2022/08/10 by Amirhossein Akbar Tabatabai, Tabatabai, Amirhossein Akbar, Rosalie Iemhoff +3
Computer Science · #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2208.05202
openalex publication_date 2022/08/10 · openalex created_date 2022/08/12 · openalex updated_date 2026/07/28
In this paper, a proof-theoretic method to prove uniform Lyndon interpolation for non-normal modal and conditional logics is introduced and applied to show that the logics E, M, EN, MN, MC, K, and their conditional versions, CE, CM, CEN, CMN, CMC, CK, in addition to CKID have that property. In particular, it implies that these logics have uniform interpolation. Although for some of them the latter is known, the fact that they have uniform Lyndon interpolation is new. Also, the proof-theoretic proofs of these facts are new, as well as the constructive way to explicitly compute the interpolants that they provide. On the negative side, it is shown that the logics CKCEM and CKCEMID enjoy uniform interpolation but not uniform Lyndon interpolation. Moreover, it is proved that the non-normal modal logics EC and ECN and their conditional versions, CEC and CECN, do not have Craig interpolation, and whence no uniform (Lyndon) interpolation.