A Linear Perspective on Cut-Elimination for Non-wellfounded Sequent Calculi with Least and Greatest Fixed-Points

被引：1

作者：

Saurin, Alexis ^{[1
,2
]}

机构：

[1] Univ Paris Cite, CNRS, IRIF, Paris, France

[2] INRIA, Paris, France

来源：

AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2023 | 2023年 / 14278卷

关键词：

LL; mu-calculus; Non-wellfounded proofs; cut elimination; INDUCTION;

D O I：

10.1007/978-3-031-43513-3_12

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

This paper establishes cut-elimination for mu LL infinity, mu LK infinity and mu LJ(infinity), that are non-wellfounded sequent calculi with least and greatest fixed-points, by expanding on prior works by Santocanale and Fortier [20] as well as Baelde et al. [3,4]. The paper studies a fixed-point encoding of LL exponentials in order to deduce those cut-elimination results from that of mu MALL(infinity). Cut-elimination for mu LK infinity and mu LJ(infinity) is obtained by developing appropriate linear decorations for those logics.

引用

页码：203 / 222

页数：20