Cut-Elimination for Cyclic Proof Systems with Inductively Defined Propositions (Theory and Applications of Proof and Computation)

HANDLE Open Access

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

    京都大学数理解析研究所

Details 詳細情報について

  • CRID
    1050858441648061312
  • NII Book ID
    AN00061013
  • HANDLE
    2433/279726
  • ISSN
    18802818
  • Text Lang
    en
  • Article Type
    departmental bulletin paper
  • Data Source
    • IRDB

Report a problem

Back to top