Cut-Elimination for Cyclic Proof Systems with Inductively Defined Propositions (Theory and Applications of Proof and Computation)
-
- Kimura, Daisuke
- Toho University
-
- Nakazawa, Koji
- Nagoya University
-
- Saotome, Kenji
- Intelligent Systems Laboratory, SECOM Company Limited
Search this article
Abstract
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.
Journal
-
- RIMS Kokyuroku
-
RIMS Kokyuroku 2228 59-72, 2022-08
京都大学数理解析研究所
- Tweet
Details 詳細情報について
-
- CRID
- 1050858441648061312
-
- NII Book ID
- AN00061013
-
- HANDLE
- 2433/279726
-
- ISSN
- 18802818
-
- Text Lang
- en
-
- Article Type
- departmental bulletin paper
-
- Data Source
-
- IRDB