Name
Abstract | ||
|---|---|---|
Spatial logics are used to reason locally about disjoint data structures. They consist of standard first-order logic constructs, spatial (structural) connectives and their corresponding adjuncts. Lozes has shown that the adjuncts add no expressive power to a spatial logic for analysing tree structures, a surprising and important result. He also showed that a related logic does not have this adjunct elimination property. His proofs yield little information on the generality of adjunct elimination. We present a new proof of these results based on model-comparison games, and strengthen Lozes’ results. Our proof is directed by the intuition that adjuncts can be eliminated when the corresponding moves are not useful in winning the game. The proof is modular with respect to the operators of the logic, providing a general technique for determining which combinations of operators admit adjunct elimination. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1007/978-3-540-30538-5_18 | FSTTCS |
Keywords | Field | DocType |
adjunct elimination property,adjunct elimination,new proof,corresponding adjunct,standard first-order logic construct,corresponding move,related logic,static ambient logic,disjoint data structure,analysing tree structure,spatial logic,expressive power,tree structure,data structure,first order logic | Data structure,Discrete mathematics,Disjoint sets,Computer science,Hoare logic,Theoretical computer science,First-order logic,Mathematical proof,Adjunct,Operator (computer programming),Artificial intelligence,Ambient calculus | Conference |
Volume | ISSN | ISBN |
3328 | 0302-9743 | 3-540-24058-6 |
Citations | PageRank | References |
7 | 0.55 | 10 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| anuj dawar | 1 | 883 | 77.18 |
| Philippa Gardner | 2 | 314 | 14.45 |
| Giorgio Ghelli | 3 | 1300 | 255.19 |