Preclosure Hyperdoctrines

Completeness of (Higher Order) Spatial Logic for Closure Spaces
Davide Castelnovo






Sala Riunioni, ore 11:30


Marino Miculan


Abstract: We introduce the categorical notion of preclosure hyperdoctrines as an abstract theoretical framework for investigating the logical aspects of preclosure spaces, a generalization of topological spaces covering also the notion of neighbourhood in discrete structures. Using this theory, we provide the first axiomatisation and sound and complete semantics for Spatial Logic for Closure Spaces, a modal logic for the specification and verification on spatial properties over preclosure spaces. Moreover, exploiting general results from categorical logic we introduce a new, higher order, version of SLCS, with a sound and complete semantics. Thus, the theory of preclosure hyperdoctrines is useful in the analysis and definition of new spatial logics for various applications, e.g. CAS, autonomic vehicles, image analysis and description, etc.