2023-09-14
The logic of separation logic: Models and proofs
Publication
Publication
Presented at the
32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Models, TABLEAUX 2023 (September 2023), Prague, Czech Republic
The standard semantics of separation logic is restricted to finite heaps. This restriction already gives rise to a logic which does not satisfy compactness, hence it does not allow for an effective, sound and complete axiomatization. In this paper we therefore study both the general model theory and proof theory of the separation logic of finite and infinite heaps over arbitrary (first-order) models. We show that we can express in the resulting logic finiteness of the models and the existence of both countably infinite and uncountable models. We further show that a sound and complete sequent calculus still can be obtained by restricting the second-order quantification over heaps to first-order definable heaps.
| Additional Metadata | |
|---|---|
| doi.org/10.1007/978-3-031-43513-3_22 | |
| Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence | |
| 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Models, TABLEAUX 2023 | |
| Organisation | Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands |
|
de Boer, F., Hiep, H.-D., & de Gouw, S. (2023). The logic of separation logic: Models and proofs. In 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Models, TABLEAUX 2023 (pp. 407–426). doi:10.1007/978-3-031-43513-3_22 |
|
