Cut-Elimination for Cyclic Proof Systems with Inductively Defined Propositions (Theory and Applications of Proof and Computation)
この論文をさがす
抄録
Cyclic proof systems are extensions of the sequent-calculus style proof systems for logics with inductively defined predicates. In cyclic proof systems, inductive reasoning is realized as cyclic structures in proof trees. It has been already known that the cut-elimination property does not hold for the cyclic proof systems of some logics such as the first-order predicate logic and the separation logic. In this paper, we consider the cyclic proof systems with inductively defined propositions (that is, nullary predicates), and prove that the cut-elimination holds for the propositional logic, and it does not hold for the bunched logic.
収録刊行物
-
- 数理解析研究所講究録
-
数理解析研究所講究録 2228 59-72, 2022-08
京都大学数理解析研究所
- Tweet
詳細情報 詳細情報について
-
- CRID
- 1050858441648061312
-
- NII書誌ID
- AN00061013
-
- HANDLE
- 2433/279726
-
- ISSN
- 18802818
-
- 本文言語コード
- en
-
- 資料種別
- departmental bulletin paper
-
- データソース種別
-
- IRDB