Mechanised uniform interpolation for modal logics K, GL, and iSL
arxiv(2024)
摘要
The uniform interpolation property in a given logic can be understood as the
definability of propositional quantifiers. We mechanise the computation of
these quantifiers and prove correctness in the Coq proof assistant for three
modal logics, namely: (1) the modal logic K, for which a pen-and-paper proof
exists; (2) Gödel-Löb logic GL, for which our formalisation clarifies an
important point in an existing, but incomplete, sequent-style proof; and (3)
intuitionistic strong Löb logic iSL, for which this is the first
proof-theoretic construction of uniform interpolants. Our work also yields
verified programs that allow one to compute the propositional quantifiers on
any formula in this logic.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要