# Proofs and countermodels in BI's pointer logic

1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The question of defining an usable proof theory and proof-search methods for separation logics naturally arises and therefore our aim is to study this question firstly for BIs pointer logic (PL). For that, we apply the same methodology than for proof search in BI logic, that consists in capturing the semantics of PL through rules with labels and constraints and then defining specific closure conditions for the corresponding tableaux method. We first define a calculus and a method for a fragment of PL with only the points-to relation and prove the correctness of the method and its completeness through the construction of countermodels from an open branch and a dependency graph. These results are extended to equality atomic predicate and to existential quantification in order to cover the PLs formulae. Similar results are proposed for the intuitionistic version of PL that is based on affine BI in which weakening on the multiplicative conjunction holds.
Mots-clés :
Type de document :
Communication dans un congrès
2nd APPSEM II Workshop - APPSEM'04, 2004, Tallinn/Estonia, 2004
Domaine :

https://hal.inria.fr/inria-00100047
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 10:13:41
Dernière modification le : mardi 24 avril 2018 - 13:36:41

### Identifiants

• HAL Id : inria-00100047, version 1

### Citation

Didier Galmiche, Julien Gobillot, Daniel Méry. Proofs and countermodels in BI's pointer logic. 2nd APPSEM II Workshop - APPSEM'04, 2004, Tallinn/Estonia, 2004. 〈inria-00100047〉

### Métriques

Consultations de la notice