## Abstract

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.

Original language | English |
---|---|

Title of host publication | Automated Reasoning with Analytic Tableaux and Related Methods |

Subtitle of host publication | 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings |

Editors | Revantha Ramanayake, Josef Urban |

Publisher | Springer |

Pages | 407-426 |

Number of pages | 20 |

ISBN (Electronic) | 9783031435133 |

ISBN (Print) | 9783031435126 |

DOIs | |

Publication status | Published - 14 Sept 2023 |

Event | 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023 - Prague, Czech Republic Duration: 18 Sept 2023 → 21 Sept 2023 https://tableaux2023.tableaux-ar.org/#:~:text=The%2032nd%20International%20Conference,September%2018%2D21%2C%202023. |

### Publication series

Series | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 14278 LNAI |

ISSN | 0302-9743 |

### Conference

Conference | 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023 |
---|---|

Country/Territory | Czech Republic |

City | Prague |

Period | 18/09/23 → 21/09/23 |

Internet address |