Talk 1: On Cut-Elimination in Cyclic-Proof Systems, Talk 2: Entailment Checking Procedure for Symbolic Heaps using a Complete Cyclic Proof System
Speaker 2: Dr Daisuke Kimura, Toho University
Speaker 1 Abstract:
Cyclic-proof systems are logical systems in which the induction is represented as cyclic structure of proof trees. Cyclic-proof systems are suitable for automated proof search, and they have been actively studied for several logics such as the first-order logic, the linear logic, and the separation logic. However, fundamental properties of the cyclic-proof systems are not well-known. In this talk, we discuss on the cut-elimination property for the cyclic-proof systems. In particular, we prove that the cut-elimination theorem does not hold in the cyclic-proof system for the separation logic. We expect that the proof idea will be extended to other logics such as the first-order logic and the logic of bunched implications, that is, we conjecture the cut-elimination does not hold in the cyclic-proof systems for these logics.
Speaker 2 Abstract:
This talk presents an entailment checker for a symbolic-heap system with user-defined inductively defined predicates. The checker is an implementation of the proof-search algorithm in the other paper of our group, which proposes a complete proof system for entailments of the symbolic heap system with a class of general inductive predicates, called cone inductive predicates.
This talk focuses to explain our basic algorithm idea: unfold-match with spatial factorization and split. This algorithm is quite inefficient because of an inference rule, called the split-rule, which splits the separating conjunctions on both sides of an entailment. The split-rule requires to explore all possible branches of the splitting cases in order to achieve completeness. We also discuss some ideas for reducing this inefficiency. Experiments show that the checker works well for some non-trivial and interesting inputs.