Sciweavers

CORR
2004
Springer

On Spatial Conjunction as Second-Order Logic

13 years 3 months ago
On Spatial Conjunction as Second-Order Logic
Abstract. Spatial conjunction is a powerful construct for reasoning about dynamically allocated data structures, as well as concurrent, distributed and mobile computation. While researchers have identified many uses of spatial conjunction, its precise expressive power compared to traditional logical constructs was not previously known. In this paper we establish the expressive power of spatial conjunction. We construct an embedding from first-order logic with spatial conjunction into second-order logic, and more surprisingly, an embedding from full second order logic into first-order logic with spatial conjunction. These embeddings show that the satisfiability of formulas in first-order logic with spatial conjunction is equivalent to the satisfiability of formulas in second-order logic. These results explain the great expressive power of spatial conjunction and can be used to show that adding unrestricted spatial conjunction to a decidable logic leads to an undecidable logic. As one ex...
Viktor Kuncak, Martin C. Rinard
Added 17 Dec 2010
Updated 17 Dec 2010
Type Journal
Year 2004
Where CORR
Authors Viktor Kuncak, Martin C. Rinard
Comments (0)