We de ne a new notion of truth for logic programs extended with labelled variables, interpreted in non-Herbrand domains. There, usual terms maintain their Herbrand interpretations, whereas diverse domain-speci c computational models depending on the local situation of the computing device can be expressed via suitably-tailored labelled models. After some introductory examples, we de ne the theoretical model for labelled variables in logic programming (LVLP). Then, we present both the xpoint and the operational semantics, and discuss their correctness and completeness, as well as their equivalence.
To face the challenges of today's pervasive systems { inherently complex,
distributed, situated, and intelligent [
Along this line, in this paper we present a logic programming extension based
on labelled variables [
Most other works in this area { such as [
In nowadays complex and pervasive scenario, where software engineering,
programming languages, and distributed arti cial intelligence meet, logic-based
languages have the potential to play a prominent role both as intelligence providers
and technology integrators [
Along this line, we introduce the notion of label to tag logic variables, and the associated computational model for their elaboration, which proceeds along with the resolution procedure without being strictly subject to the standard LP rules. Generally speaking, labels provide a customisable computational model, which can be charged of the domain-speci c { and possibly not declarative { part of the computation, and bound to the standard LP computation.
Before formally de ning (Section 3) the Labelled Variables model in Logic
Programming (LVLP), we informally discuss some examples to give the avour
of our approach. For instance, in a WordNet-like scenario [
Following our prototype syntax, X^label is a labelled variable denoting a logic variable X labelled with label |where label is a term in the set of admissible labels de ned by the user. In a LVLP clause, the list of the labelled variables precedes the remaining part of the body. Given the following LVLP program: wordnet_fact ([ ` dog ',` domestic dog ',` canis ',` pet ',` mammal ',` vertebrate ']). wordnet_fact ([ ` cat ', ` domestic cat ', `pet ', ` mammal ', ` vertebrate ']). wordnet_fact ([ ` fish ', ` aquatic vertebrates ', ` vertebrate ']). wordnet_fact ([ ` frog ', `toad ', ` anauran ', ` batrachian ']). animal (X) :- X^[ ` pet '], X = ` minnie '. animal (X) :- X^[ ` fish '], X = `nemo '. animal (X) :- X^[ ` cat '], X = ` vmolly '. animal (X) :- X^[ ` dog '], X = ` frida '.
animal (X) :- X^[ ` frog '], X = `cra '. the following query, looking for a pet animal, generates four solutions: ?- X^[ ` pet '], animal (X ). yes . X / ` minnie ' [X^[ ` dog ', ` domestic dog ', ` canis ', `pet ', ` mammal ', ` vertebrate ']] ; yes . X / ` minnie ' [X^[ ` cat ', ` domestic cat ', `pet ', ` mammal ', ` vertebrate ']] ; yes . X / ` molly ' [X^[ ` cat ', ` domestic cat ', `pet ', ` mammal ', ` vertebrate ']] ; yes . X / ` frida ' [X^[ ` dog ', ` domestic dog ', ` canis ', `pet ', ` mammal ', ` vertebrate ']] Looking instead for a less speci c vertebrate produces ve solutions: ?- X ^[ vertebrate ], animal (X ). yes . X = ` minnie ' X^[ ` dog ', ` domestic dog ', ` canis ', `pet ', ` mammal ', ` vertebrate '] ; yes . X = ` minnie ' X^[ ` cat ', ` domestic cat ', `pet ', ` mammal ', ` vertebrate '] ; yes . X = ` molly ' X^[ ` cat ', ` domestic cat ', `pet ', ` mammal ', ` vertebrate '] ; yes . X = ` frida ' X^[ ` dog ', ` domestic dog ', ` canis ', `pet ', ` mammal ', ` vertebrate '] ; yes . X = `nemo ' X^[ ` fish ',` aquatic vertebrates ', ` vertebrate '] A relevant aspect of LVLP is that labels are not subject to the single-assignment assumption: each time two labelled variables unify, their labels are processed and combined according to a user-de ned function that embeds the desired computational model, and the resulting label is associated to the uni ed variable. Thus, the LP model per se is left untouched, whereas diverse computational models can be de ned next to it, possibly in uencing the result of a logic computation by restricting the set of admissible solutions according to each speci c domain.
For instance, let us consider the case in which the knowledge base consists of a collection of ingredients, each featuring properties such as calories count, amount of proteins, fat, etc. There, labels could be used to describe the weight, calories and category of the food, as in the program below: meat (M) :- M ^[100 g , 156 cal , [ alternativeMeats ]] , M=[ ` tofu meatballs ']. meat (M) :- M ^[100 g , 145 cal , [ curedMeats ]] , M=[ ` Parma ham ']. meat (M) :- M ^[100 g , 210 cal , [ curedMeats ]] , M=[ ` ham ']. meat (M) :- M ^[200 g , 220 cal , [ whiteMeats ]] , M=[ ` chicken ']. vegetable (V) :- V ^[100 g , 35 cal , [ vegetables ]] , V=[ ` carrots ']. vegetable (V) :- V ^[ 50g , 10 cal , [ vegetables ]] , V=[ ` salad ']. bread (B) :- B ^[100 g , 265 cal , [ whiteBread ]] , B=[ ` bread with poolish ']. bread (B) :- B ^[100 g , 240 cal , [ integralBread ]] , B=[ ` whole grain bread ']. recipe (R) :- R^ , meat ( Meat ), vegetable ( Vegetable ), R =[ Meat , Vegetable ]. recipe (R) :- R^ , Meat ^[ any , any , [ curedMeats ]] , bread ( Bread ), meat ( Meat ), vegetable ( Vegetable ), R =[ Bread , Meat , Vegetable ].
Labels (with
representing the any label) make it possible, for instance, to ask for a meal with an upper bound of calories, with a given tolerance. Assuming, e.g., that the label-combining function accounts for a 10% tolerance, a possible query asking for a recipe with 200( 20) calories could be the following: ?- R ^[ any , 200 cal , any ], recipe (R ). yes . R / [` tofu meatballs ', ` carrots '] R ^[200 g , 191 cal , [ alternativeMeats , vegetables ]] ; yes . R / [` tofu meatballs ', ` salad '] R ^[200 g , 166 cal , [ alternativeMeats , vegetables ]] ; yes . R / [` Parma ham ', ` carrots '] R ^[200 g , 180 cal , [ curedMeats , vegetables ]] ; yes . R / [` ham ', ` salad '] R ^[150 g , 220 cal , [ curedMeats , vegetables ]] Comparing the labels of R in the query and in the answers should make it clear how avoiding single assignment in the labels (not in the logic variable) makes the language more expressive, without harming the logic computation.
Multiple matching criteria could also be applied simultaneously|for instance, combining calories with a speci c food category: ?- R ^[ any , 180 cal , [ alternativeMeats ]] , recipe (R ). yes . R / [` tofu meatballs ',` carrots '] R ^[200 g , 191 cal , [ alternativeMeats , vegetables ]] ; yes . R / [` tofu meatballs ',` salad ']
R ^[150 g , 166 cal , [ alternativeMeats , vegetables ]]
All \standard" domains for logic languages (like the CLP ones [
X ^[
X ^[
X ^[
Let C be the set of constants, with c1; c2 2 C being two generic constants. Let V be the set of variables, with v1; v2 2 V being two generic variables. Let F 2 H be the set of function symbols, with f1; f2 2 F being two generic function symbols. f 2 F is assigned to an arity ar (f ) > 0 that states the number of arguments. Let T H be the set of terms, with t1; t2 2 T being two generic terms. Terms can be either simple (constant, variable) or compound (when containing a f 2 F; ar (f ) > 0). Let H be the Herbrand universe and HB be the Herbrand base.
A Labelled Variables Model in Logic Programming is de ned as follows. { A set B = f 1; : : : ; ng of basic labels that are the basic entities of the domain of labels.3 { A set L }(B) of labels, where each ` 2 L is a subset of B, namely a set of basic labels (e.g., ` = f 1; 3; 6g). A \singleton" label f g where 2 B will be identi ed simply by in the following for the sake of simplicity. { A set of variables V , where v 2 V is the generic variable. { A labelling which is a set of pairs hvi; `ii, associating the label `i to the variable vi. A \singleton" labelling fhv; `ig { a labelled variable { will be identi ed simply by hv; `i in the following for the sake of simplicity. { A (label-)combining function fL, synthesising a new label from two given ones fL : L
L ! L We require that fL be associative, commutative, and idempotent (brie y, ACI), namely that fL(`1; fL(`2; `3)) = fL(fL(`1; `2); `3); fL(`1; `2) = fL(`2; `1); fL(`; `) = `. As discussed later, in some cases (e.g., incompatibility), the output of fL can be the empty set ; which is a signal for \wrong". 3.2
In a labelled variables logic program a rule is represented as
where Head is an atomic formula, Labellings is the list of Variable/Label associations in the clause and Body is a list of atomic formulas. This can be read declaratively as Head if Body given Labellings.
The uni cation of two labelled variables is represented by the extended tuple (true=false, , `), where true=false represents the existence of an answer, represents the most general substitution, and ` represents the new label associated to the uni ed variables de ned by the (label-)combining function fL.
More generally, considering all the variables of the goal, the solution is represented by the extended tuple (true=false, , A), where true=false represents the existence of an answer, represents the most general substitutions for all such variables, and A represents the corresponding label-variable associations. 3 In this paper we require that B is nite and it is not a real restriction for the applications we discuss. An in nite set of basic labels can be considered anyway, as soon as we can guarantee a sort of solution compactness of the extended uni cation algorithms involved.
; =6 d n )) a2 :::) lse if (`
L f ) 2 ` ; 1 ` ( ; L
f =6 ; e ) 2 2g ls n e h t 1 e ` C f n f e i h
t e l b a i r i a 1 v `
; n a b t 1 a 1 s c ir v d 1 on a le vh c v l
e 2 s d h 1 t v f i in g s n ab s2 ,2g ;`1 r 2 in ;` l
s u =
L f 1 s n i g r 1
s u = cc v2f lea
s o t ; f o e
e u s sn rt le eo en d h 2 t v f i e s l a f m r e t d p m o c n 1 u s o
L io f t a c i n U The tuple (true=false, , A) represents the solution of the labelled variables program. The implicit assumption is that the LP computation, whose answer is given by , and of the label computation, whose answer is given by A, can be read independently from each other from the domain expert's viewpoint.
This is as to say that, in principle, any computed label-variable association is \acceptable" in the domain|for instance, if LP computes over numbers and labels over colors, each number/color association might be equally valid.
For some application scenarios, however, this might not necessarily be the case: if the LP and label computations somehow capture di erent views over the same domain (or two interconnected domains), some label-variable association could actually be unacceptable from the domain expert's viewpoint|for instance, in the above example even numbers could not be red, or alike.
In order to formalise such a notion of acceptability, let us introduce the compatibility function fC as: fC : H
L ! ftrue; falseg In particular, given a a ground term t 2 H and label ` 2 L : fC (t; `) = 8>true > > < there exists at least an element of the domain which the interpretations of t and ` both refer to the same entity > > >:false otherwise Example 1 discusses an application scenario where variables are labelled with their admissible numeric interval, formalising the fL and fC functions accordingly.
Example 1. Let us suppose that the LP variables in a certain application scenario span over some integer domains and that they are labelled with their admissible numeric interval. In this case, the combining function fL, which embeds the scenario-speci c label semantics, is supposed to intersects intervals: accordingly, fL is de ned so that, given two labels `1 = f 11; : : : ; 1ng and `2 = f 21; : : : ; 2mg, the resulting label `3 is the intersection of `1 and `2, as:
`3 = fL(`1; `2) = fL(f 11; : : : 1ng; f 21; : : : 2mg) = f( 11 \ 21); ; ( 11 \ 2m); : : : ; ( 1n \ 21); ; ( 1n \ 2m)g In such a scenario, the LP computation aims to compute numeric values, while the label computation aims to compute admissible numeric intervals for the LP variables.
In principle, the solution tuple (true=false, , A) could describe situations such as (true; X = 3; h3; [4; 5]i), since the LP computation and the label computation proceed without interfering with each other. However, if numeric intervals are interpreted as the boundaries for acceptable values of LP variables, such label-variable associations could appear to be inconsistent to the domain expert's eyes. So, a reasonable behaviour for the LVLP system should allow the domain expert to embed his/her knowledge, capturing such incompatibility so that the system can reject this solution.
This is what the compatibility function fC is for: its purpose is to check whether the ground term t 2 H is compatible with the interval represented by label ` = [A::B]; ` 2 L. It could be de ned so as to return false for solutions where the computed LP values do not belong to the numeric interval computed by the corresponding label computation, thus capturing the connection among the two universes.
Summing up, the result of a labelled variables program can be written as: (true=false ^ fC ( ; A); ; A) meaning that the truth value potentially computed by the LP computation can be restricted { i.e., forced to false { by the fC ( ; A). In turn, this is a convenient shortcut for the conjunction of all fC (t; `) 8(t; `) couples, where ` and t are, respectively, such that the label-variable association hv; `i 2 A and the substitution v=t 2 . Of course, in case of independent domains, fC (t; `) is true for any t and any `.
Table 1 reports the uni cation rules for two generic terms: to lighten the notation, unde ned elements in the tuple are omitted|i.e., labels or substitutions that have no sense in a particular situation. 4
Labels domains are expected to support tests and operations on labels, in order to guarantee the basic theoretical results of logic programming, such as the equivalence of denotational and operational semantics.
In the following, in Subsection 4.1 we de ne the denotational ( xpoint) semantics in the context of labels domain (under reasonable requests for fL), while in Subsection 4.2 we discuss the operational semantics of the model describing an abstract state machine. 4.1
Let us call X = (H ; L) a labelled variable logic programming domain and let us de ne the notion of X -interpretation I as a set of pairs of the form p(t1; : : : ; tn); [`1; : : : ; `n] where p(t1; : : : ; tn) is a ground atom and `1; : : : ; `n are labels s.t. for i = 1; : : : ; n the term ti is compatible with the label `i, i.e. fC (ti; `i) = true. Truthness of fC is based on the LVLP domain X . With a slight abuse of notation, we write X j= [ht1; `1i; : : : ; htn; `ni] i Vin=1 fC (ti; `i) = true. We also write X j= (p(t1; : : : ; tn); [`1; : : : ; `n]) if p is a predicate symbol and Vn i=1 fC (ti; `i) = true.
We denote as the part of clause body that stores labelling associations. Without loss of generality we assume that there is exactly one label association for each variable in the head. We de ne the function feL that in a sense extends fL and takes as argument a rule r = h ; b1; : : : ; bn and n + 1 lists of labels. The rule r is used here to identify multiple occurrences of the variables. Let us assume the variables in h are x1; : : : ; xm, and consider one of them, say xi. If xi occurs in h (and hence in ) and in (some of) b1; : : : ; bn then the corresponding labels `; `1;i; : : : ; `n;i for xi are retrieved from (if xi does not occur in bj simply we do not consider such contribution). Then `0i = fL(`; fL(`1;i; : : : ; fL(`n 1;i; `n;i) : : : )) is computed and the pair hxi; `0i is returned. This is done for all variables x1; : : : ; xm occurring in the head h and the list [`01; : : : ; `0m] is returned.
The denotational semantics we are presenting is based on the one-step consequence functions T P de ned as:
T P (I) = h p(et); `e i : X j= r = p(xe) xe j b1; : : : ; bn (1) where r is a fresh renaming of a rule of P; v is a valuation on H such that v(xe) = et; (2) Vin=1 9 `ei s.t. hv(bi); `eii 2 I; (3) (4) et ^ Vin=1 fC v(bi); `ei ; `e = feL r; et; `e1; ; `en (5) where et = v( xe) = [ht1; `1i; : : : ; htn; `mi] if xe = [hx1; `1i; : : : ; hxm; `mi]. It is worth noting that the condition Vin=1 fC v(bi); `ei (line 4) is always satis ed when TP is used \bottom-up" starting from I = ;.
In the following some examples are discussed. Note that, in the LVLP the equality operator is represented by =/2 and its behaviour is summarised by Table 1 (uni cation rules). One label association is possibly null in that might be the any label, de ned as the neutral element of fL, henceforth represented as in the following. As a consequence, any standard (i.e. non labelled) LP variable is interpreted as labelled with . For such reasons, the =/2 in LVLP can be de ned as:
X = Y : [< X; >; < Y; >]; X =LP Y
where =LP is the standard =/2 LP operator.
Example 2. Now let us consider the labelled variables program P:
r (0). r (1). r (2). r (3). r (4).
r (5). r (6). r (7). r (8). r (9).
q(Y ,Z) :- Y ^[
p(X ,Y ,Z) :- X ^[
Let us consider the interpretation I0 = ;. Then:
hr(0); [ ]i; : : : ; hr(9)[ ]i Let us apply TP to I1: and now TP to I2:
I2 = T P (I1) = I1 [ hq(3; 3); [[3; 4]; [3; 4]]i; hq(4; 4); [[3; 4]; [3; 4]]i
I3 = T P (I2) = I2 [ hp(3; 3; 3); [[
The above example shows the similarities between labelled logic programming on a domain X (brie y, LVLP(X )) and CLP (X ). It would be su cient, e.g., to replace [hY; [2; 4]i; hZ; [3; 8]i] with Y in 2::4; Z in 3::8. However, this is not true for other domains of labels, as in Example 3.
Example 3. In the WordNet case presented in Section 2, labels are words
describing the variable object. The combination of two di erent labels
(combining function) returns a new label only if the two labels have a lexical
relation, fail otherwise. The decision is based on the WordNet network [
WordNet is a large lexical database of English. Nouns, verbs, adjectives and adverbs are grouped into sets of cognitive synonyms (synsets). Synsets are interlinked by means of conceptual-semantic and lexical relations. The resulting network of meaningfully related words and concepts can be navigated. WordNet super cially resembles a thesaurus, in that it groups words together based on their meanings.
Here, the knowledge base locally stores some WordNet groups (a dynamic consultation to WordNet could be implemented, instead). Let be program P represented by the following facts|where wordnet fact is a simulated wordnet synset, while animal(Name) is a predicate describing an animal's name: wordnet_fact ([ ` dog ',` domestic dog ',` canis ',` pet ',` mammal ']). wordnet_fact ([ ` cat ', ` domestic cat ', `pet ', ` mammal ']). wordnet_fact ([ ` fish ',` aquatic vertebrates ', ` vertebrate ']). wordnet_fact ([ ` frog ',` toad ', ` anauran ', ` batrachian ']). pet_name (` minnie '). fish_name (` nemo '). animal (X) :- X^[ ` pet '], pet_name (X ). animal (X) :- X^[ ` fish '], fish_name (X ). The combining function fL is supposed to nd and return a wordnet synset compatible with both labels. For instance, if `1 = pet and `2 = `domestic cat0, the new generated label `3 will be [`cat0; `domestic cat0; `pet0; `mammal0]. The compatibility function fC in this scenario is always true, since any animal name is considered compatible with any animal group.
In order to show the construction of TP , let us consider the interpretation I0 = ;. Then, the subsequent step I1 can be computed as:
hpet name(`minnie0); [ ]i; h sh name(`nemo0); [ ]i Now, let us apply TP to I1 to compute I2:
I2 = T P (I1) = I1 [ hanimal(`minnie0); [[`dog0; `domestic dog0; `canis0; `pet0; `mammal0]]i; hanimal(`minnie0); [[`cat0; `domestic cat0; `pet0; `mammal0]]i; hanimal(`nemo0); [[` sh0; `aquatic vertebrates0; `vertebrate0]]i which is also the least xpoint of TP .
In order to guarantee soundness and completeness of TP in the following we demonstrate that it is a monotonic and continuous mapping on partial orders. De nition 1. An interpretation I is a model of a program P if for each rule r = p(xe) xe j b1; : : : ; bn of P and each valuation v of the variables in r on H (let us denote with et = v(xe)) it holds that { if for i = 1; : : : ; n there are hv(bi); `eii 2 I { such that X j= fC (v(bi); `ei) and { X j= et, then it must be { p(et); feL r; et; `e1; ; `en 2 I.
Proposition 1. Given a LVLP program P and a LVLP domain X , TP is (1) monotonic and (2) continuos and (3) TP (I) I i I is a model of P . Proof. (1) Let I and J be two interpretations such that I J . We need to prove that TP (I) TP (J ). If a = h p(et); `e i 2 TP (I) it means that there is a clause r 2 P , a valuation v on H for the variables in r and n elements hv(bi); `eii 2 I satisfying the remaining conditions. Since I J they belong to J as well. Then a 2 TP (J ). (2) Let us consider a chain of interpretations I0 I1 : : : . We need to prove that: TP Sk1=0 Ik = Sk1=0 TP (Ik). ( ) Let a = h p(et); `e i 2 TP Si1=0 Ik . This means that there is a clause r 2 P , a valuation v on H for the variables in r and n elements hv(bi); `eii 2 Sk1=0 Ik satisfying the remaining conditions. This means that there are j1; : : : ; jn such that for i = 1; : : : ; n hv(bi); `eii 2 Iji . Let j = maxfj1; : : : ; jng, since I0 I1
Ij we have that all hv(bi); `eii 2 Ij . Thus a 2 TP (Ij+1) and henceforth a 2 S1
k=0 TP (Ik). ( ) Let a = h p(et); `e i 2 Sk1=0 TP (Ik). This means that there is j such that a 2 TP (Ij ). Then, due to monotonicity, a 2 TP Sk1=0 Ik . (3) Let TP (I) I and let r = p(xe) xe ; b1; : : : ; bn be a generic clause of P , and v be a generic valuation on H of all the variables of r. If we assume that hv(bi); `eii 2 I for i = 1; : : : ; n, and that X j= fC (v(bi); `ei) and X j= et, then the pair h = v(p(xe); `e) 2 TP (I) by de nition of TP |and `e is the same of the de nition of model. Since TP (I) I then h 2 I, therefore (since r and v are chosen in general) I is a model of P .
On the other hand, if I is a model of P we prove that TP (I) I. Let a = h p(et); `e i 2 TP (I). This means that there is a rule r = p(xe) xe ; b1; : : : ; bn of P and a valuation v of the variables in r on H such that for i = 1; : : : ; n there are v(bi); `ei 2 I and X j= ; `en ). such that t and `e = feL r; et; `e1; e X j= fC (v(bi); `ei). Since I is a model, and X j= fC (v(bi); `ei) then a 2 I. tu Let be TP " ! de ned as usual: TP " ! = SfTP " k : k 0g. Then: Corollary 1. There is a notion of least model which is TP " !. Proof. Immediate from Knaster-Tarksi theorem, Kleene's xpoint Theorem, and Proposition 1. tu 4.2
In this section we de ne the operational interpretation of labels: our approach is
inspired by the methodology introduced for Constraint Logic Programming [
= ht0 t1:::tn; W; i where { t0 t1:::tn is the list of terms (goals) { W is the current list of variables bindings { is the set of the current labelling associations on W .
An inference step for the machine consists of making a transition from the state to a state 0 by applying a program rule. Considering the rule (m 0) s0
0; s1; s2; : : : ; sm where 0 is the set of the labellings of the rule, if the following conditions hold: { 9 mgu such that (t0) = (s0) and { fe L( ; ( 0)) 6= ; the rule is applied (fail otherwise). The function fe L is a generalisation of the combining function fL in that takes as arguments two vectors of labelling associations. If xi occurs both in and ( 0) with labels ` and `0, `00 = fL(`; `0) is rst calculated, then, if fC ( (xi); `00) = true the labelling association hxi; `00i is returned. The new state becomes: 0 = h (s1; : : : ; sm; t1; : : : ; tn); W 0 = W ; 00 = fe L( ; ( 0))i where applies the classical composition of substitutions.
A solution is found when a nal state is reached. The nal state has the form: f = ( ; Wf ; f ) where is the empty sequence, Wf is the nal list of variables and bindings, f is the corresponding labelling associations set. A sequence of applications of inference steps is said a derivation. A derivation is successful if it ends in a nal state, failing if it ends in a non- nal state where no inference step is possible. Proposition 2. Let p(xe) be an atom, v a valuation on H such that v(xe) = et where et are ground terms, and `e a list of labels. Then there is a successful derivation for hp(et); v; hv(xe); `eii i hp(et); `ei 2 TP " !.
Proof (In the following we provide a proof sketch, deferring the full proof to a future paper for the sake of brevity). (!). We prove the proposition by induction on the length k of the derivation. If k = 0 the result holds trivially.
For the inductive case, let us suppose that there is a successful derivation for hp(et); v; hv(xe); `eii of k + 1 steps. Let us focus on the rst step: there is a rule r: s0 0; s1; s2; : : : ; sm such that (p(et)) = (s0) leading to the new state = h (s1; s2; : : : ; sm); v ; 00 = fe L( ; ( 0)i, where fC ( 00) = true, that admits a successful derivation of k steps.
Consider now the states 1; : : : ; m de ned as i = h (si); v ; 0i0i where 0i0 is the restriction of 00 to the variables in si. Since admits a successful derivation of k + 1 steps, each i should admit a successful derivation of at most k steps.
If for all i 2 f1; : : : ; mg, (si) is ground, then, by inductive hypothesis we have that h (si); `ii 2 TP " ! where `i = 2( 0i0), and hence that there are his such that h (si); `ii 2 TP " hi. Since Tp is monotonic, all of them belong to TP " h where h = maxi=1;:::;m hi. Then, by applying TP considering the rule r, since we already know that 00 = fe L( ; ( 0)), and fC ( 00) = true, we have that hp(et); `ei 2 TP " h + 1, hence to TP " !.
If for some i, (si) is not ground, the above property holds for any ground instantiation of the remaining variables and again the results follows. ( ). Now, let us analyse the converse direction. If hp(et); `ei 2 TP " ! this means that there is a k 0 such that hp(et); `ei 2 TP " k.
Let us prove by induction on k. Again, if k = 0 the result holds trivially. Let us suppose now that hp(et); `ei 2 TP " k + 1. This means (by de nition of TP ) that there is a rule r: s0 0; s1; s2; : : : ; sm such that s0 = p(xe) and there is a valuation u on H such that u(s0) = p(et) and that, in particular, hs1; `1i; : : : ; hsm; `mi 2 TP " k (and fL can be computed and fC is true on these arguments). By inductive hypothesis, for i 2 f1; : : : ; mg there is a derivation, say, of hi steps for i = hu(si); v u; hu(si); `iii
Since fC is true on such arguments and fL can be computed, the same holds for TP : so, we have a derivation of Pim=1 hi + 1 steps for hp(et); v u ; het; `eii.
This completes the proof of the inductive step. tu 5
The primary result of this paper is the de nition of the LVLP theoretical framework, where di erent domain-speci c computational models can be expressed via labelled variables, capturing suitably-tailored labelled models. The framework is aimed at extending LP to face the challenges of today's pervasive systems, by providing the models and technologies required to e ectively support distributed situated intelligence, while maintaining the features of a declarative programming paradigm. We also present the xpoint and operational semantics, discuss correctness, completeness, and equivalence.
Beside completing our LVLP prototype [
Future work will be devoted to a more complete proof of the result sketched
in Subsection 4.1 as well as to the deeper exploration and better understanding
of the consequences of applying labels to formulas, as suggested by Gabbay
[