Semantic Localization for IoT
373
• logical symbols: (→ , ↔, ¬, ∧, ∨, ∀, ∃,), and
• variables (a countably infinite collection)
• function symbols (e.g. + for a group operation)
• relation symbols (e.g. ≤ for the ordering relation on R)
• the relation symbol = , as the usual “equal sign”
• constant symbols which represent a particular element from the domain (e.g. 0 or
π ).
The arity of function and relation symbols is ≥ 1.
A signature is a particular set of function, relation, and constant symbols. The
language of a signature is the set of well-formed formula expressible using functions,
relations and constants from the signature. A variable v 0 is bound iff it appears in a
subformula (i.e. a syntactically correct part of a formula) following (∀v 0 ) or (∃v 0 ).
Otherwise the variable is free, and may be assigned a value separately. For example:
formula φ with free variables v 0 , v 1 , …, v k may be written as φ(a 0 , a 1 , …, a k ) to
express the assignment of a 0 to v 0 , a 1 to v 1 , and so on.
The sentences of a language are formulas of the language with no unbound
variables. A structure (or model) is a tuple A = =A, I where A is a domain, i.e. a nonempty set, and I is an interpretation function. I maps function, relation, and constant
symbols to functions defined over A, relations defined over A, and elements of A
respectively. A structure A models a sentence S of a language when the interpretation
of the sentence within the structure evaluates to true. This relationship is denoted by
A S and its converse by A A S.
A language with a finite signature may be concisely written for example as, L =
{< , 0, 1}. Similarly, a model’s domain and interpretation for that finite signature
may be informally written as an analogous tuple, e.g. A = = R, < , 0, 1. Here, A is
the structure with domain R which interprets L with the strict ordering relation < ,
and constants 0 and 1.
Putting it all together, we may now formalize the motivating observation from the
beginning of this section that the same formula may be true or false with respect to
different domains. Regarding the example formula ∃n 0 < n < 1 we have A ∃n 0
< n < 1, but for B = = N, < , 0, 1, B B ∃n 0 < n < 1.
2.2 Semantic Localization
We propose using the concepts of model theory to formally describe location in IoT
systems. A spatial ontology can be represented as a structure A = =A, I. For A to be
useful as a model of the space, most likely the elements of A should be places or things
located at places. Similarly, I should provide spatially meaningful interpretations of
relations, functions, and constants. The language for such a structure will then consist
of semantic localization statements.
Defining semantic localization as a model-theoretic language has the advantage
of separating the specification of spatial reasoning from its implementation within a
373
• logical symbols: (→ , ↔, ¬, ∧, ∨, ∀, ∃,), and
• variables (a countably infinite collection)
• function symbols (e.g. + for a group operation)
• relation symbols (e.g. ≤ for the ordering relation on R)
• the relation symbol = , as the usual “equal sign”
• constant symbols which represent a particular element from the domain (e.g. 0 or
π ).
The arity of function and relation symbols is ≥ 1.
A signature is a particular set of function, relation, and constant symbols. The
language of a signature is the set of well-formed formula expressible using functions,
relations and constants from the signature. A variable v 0 is bound iff it appears in a
subformula (i.e. a syntactically correct part of a formula) following (∀v 0 ) or (∃v 0 ).
Otherwise the variable is free, and may be assigned a value separately. For example:
formula φ with free variables v 0 , v 1 , …, v k may be written as φ(a 0 , a 1 , …, a k ) to
express the assignment of a 0 to v 0 , a 1 to v 1 , and so on.
The sentences of a language are formulas of the language with no unbound
variables. A structure (or model) is a tuple A = =A, I where A is a domain, i.e. a nonempty set, and I is an interpretation function. I maps function, relation, and constant
symbols to functions defined over A, relations defined over A, and elements of A
respectively. A structure A models a sentence S of a language when the interpretation
of the sentence within the structure evaluates to true. This relationship is denoted by
A S and its converse by A A S.
A language with a finite signature may be concisely written for example as, L =
{< , 0, 1}. Similarly, a model’s domain and interpretation for that finite signature
may be informally written as an analogous tuple, e.g. A = = R, < , 0, 1. Here, A is
the structure with domain R which interprets L with the strict ordering relation < ,
and constants 0 and 1.
Putting it all together, we may now formalize the motivating observation from the
beginning of this section that the same formula may be true or false with respect to
different domains. Regarding the example formula ∃n 0 < n < 1 we have A ∃n 0
< n < 1, but for B = = N, < , 0, 1, B B ∃n 0 < n < 1.
2.2 Semantic Localization
We propose using the concepts of model theory to formally describe location in IoT
systems. A spatial ontology can be represented as a structure A = =A, I. For A to be
useful as a model of the space, most likely the elements of A should be places or things
located at places. Similarly, I should provide spatially meaningful interpretations of
relations, functions, and constants. The language for such a structure will then consist
of semantic localization statements.
Defining semantic localization as a model-theoretic language has the advantage
of separating the specification of spatial reasoning from its implementation within a