Automated Theorem Proving for Assertions in Separation Logic with All Connectives
This paper considers Reynolds’s separation logic with all logical connectives but without arbitrary predicates. This logic is not recursively enumerable but is very useful in practice. We give a sound labelled sequent calculus for this logic. Using numerous examples, we illustrate the subtle deficiencies of several existing proof calculi for separation logic, and show that our rules repair these deficiencies. We extend the calculus with rules for linked lists and binary trees, giving a sound,...[Show more]
|Collections||ANU Research Publications|
|Source:||Beagle - A Hierarchic Superposition Theorem Prover|
|01_Hou_Automated_Theorem_Proving_for_2015.pdf||925.5 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.