A New Calculus for Intuitionistic Strong Lob Logic: Strong Termination and Cut-Elimination, Formalised

被引：2

作者：

Shillito, Ian ^{[1
]}

van der Giessen, Iris ^{[2
]}

Gore, Rajeev ^{[3
,4
]}

Iemhoff, Rosalie ^{[5
]}

机构：

[1] Australian Natl Univ, Canberra, Australia

[2] Univ Birmingham, Birmingham, England

[3] Vienna Univ Technol, Vienna, Austria

[4] Polish Acad Sci, Warsaw, Poland

[5] Univ Utrecht, Utrecht, Netherlands

来源：

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

基金：

欧盟地平线“2020”;

关键词：

Intuitionistic provability logic; Cut-elimination; Backward proof search; Interactive theorem proving; Proof theory; PROVABILITY LOGIC; SEQUENT CALCULI; MODAL LOGIC;

D O I：

10.1007/978-3-031-43513-3_5

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong Lob logic iSL, an intuitionistic modal logic with a provability interpretation. A novel measure on sequents is used to prove both the termination of the naive backward proof search strategy, and the admissibility of cut in a syntactic and direct way, leading to a straight-forward cut-elimination procedure. All proofs have been formalised in the interactive theorem prover Coq.

引用

页码：73 / 93

页数：21

共 46 条

[1] Uniform Interpolation from Cyclic Proofs: The Case of Modal Mu-Calculus [J].