14 citations · 37 across the 13 of their papers we have counts for
Showing 2017Show all
3 papers · 1 filter
cs.LO2017
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…
cs.LO2017★ 14 cited
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs
Stefano Berardi, Makoto Tatsuta
A cyclic proof system, called CLKID-omega, gives us another way of representing inductive definitions and efficient proof search. The 2005 paper by Brotherston showed that the prov…
cs.LO2017★ 1 cited
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…