1 citations · 1 across the 6 of their papers we have counts for
7 papers · 1 filter
Truth Predicate of Inductive Definitions and Logical Complexity of Infinite-Descent Proofs
Sohei Ito, Makoto Tatsuta
Formal reasoning about inductively defined relations and structures is widely recognized not only for its mathematical interest but also for its importance in computer science, and…
Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic
Sohei Ito, Makoto Tatsuta
Separation logic is successful for software verification of heap-manipulating programs. Numbers are necessary to be added to separation logic for verification of practical software…
Cut elimination for propositional cyclic proof systems with fixed-point operators
Hiromasa Hori, Koji Nakazawa, Makoto Tatsuta
Infinitary and cyclic proof systems are proof systems for logical formulas with fixed-point operators or inductive definitions. A cyclic proof system is a restriction of the corres…
Completeness of Cyclic Proofs for Symbolic Heaps
Makoto Tatsuta, Koji Nakazawa, Daisuke Kimura
Separation logic is successful for software verification in both theory and practice. Decision procedure for symbolic heaps is one of the key issues. This paper proposes a cyclic p…
Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic
Stefano Berardi, Makoto Tatsuta
A cyclic proof system gives us another way of representing inductive definitions and efficient proof search. In 2011 Brotherston and Simpson conjectured the equivalence between the…
Decision Procedure for Entailment of Symbolic Heaps with Arrays
Daisuke Kimura, Makoto Tatsuta
This paper gives a decision procedure for the validity of en- tailment of symbolic heaps in separation logic with Presburger arithmetic and arrays. The correctness of the decision…