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

HANDLE オープンアクセス

この論文をさがす

抄録

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.

収録刊行物

詳細情報 詳細情報について

  • CRID
    1050858441648061312
  • NII書誌ID
    AN00061013
  • HANDLE
    2433/279726
  • ISSN
    18802818
  • 本文言語コード
    en
  • 資料種別
    departmental bulletin paper
  • データソース種別
    • IRDB

問題の指摘

ページトップへ