arXiv:1009.1976v1 [cs.LO] 10 Sep 2010

A Transformation-based Implementation
for CLP with Qualification and Proximity ∗
Preliminary Version (Technical Report SIC-4-10)
R. CABALLERO, M. RODRÍGUEZ-ARTALEJO and C. A. ROMERO-DÍAZ
Departamento de Sistemas Informáticos y Computación, Universidad Complutense
Facultad de Informática, 28040 Madrid, Spain
(e-mail: {rafa,mario}@sip.ucm.es, cromdia@fdi.ucm.es)

Abstract
Uncertainty in logic programming has been widely investigated in the last decades, leading
to multiple extensions of the classical LP paradigm. However, few of these are designed
as extensions of the well-established and powerful CLP scheme for Constraint Logic Programming. In a previous work we have proposed the SQCLP (proximity-based qualified
constraint logic programming) scheme as a quite expressive extension of CLP with support
for qualification values and proximity relations as generalizations of uncertainty values and
similarity relations, respectively. In this paper we provide a transformation technique for
transforming SQCLP programs and goals into semantically equivalent CLP programs and
goals, and a practical Prolog-based implementation of some particularly useful instances of
the SQCLP scheme. We also illustrate, by showing some simple—and working—examples,
how the prototype can be effectively used as a tool for solving problems where qualification
values and proximity relations play a key role. Intended use of SQCLP includes flexible
information retrieval applications.
KEYWORDS: Constraint Logic Programming, Program Transformation, Qualification
Domains and Values, Similarity and Proximity Relations, Flexible Information Retrieval.

1 Introduction
Many extensions of LP (logic programming) to deal with uncertain knowledge and
uncertainty have been proposed in the last decades. These extensions have been
proposed from different and somewhat unrelated perspectives, leading to multiple
approaches in the way of using uncertain knowledge and understanding uncertainty.
A recent work by us (Rodrı́guez-Artalejo and Romero-Dı́az 2010a) focuses on
the declarative semantics of a new proposal for an extension of the CLP scheme
supporting qualification values and proximity relations. More specifically, this work
defines a new generic scheme SQCLP (proximity-based qualified constraint logic
programming) whose instances SQCLP(S, D, C) are parameterized by a proximity
∗ This work has been partially supported by the Spanish projects STAMP (TIN2008-06622-C0301), PROMETIDOS–CM (S2009TIC-1465) and GPD–UCM (UCM–BSCH–GR58/08-910502).

2

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

relation S, a qualification domain D and a constraint domain C. The current paper is intended as a continuation of (Rodrı́guez-Artalejo and Romero-Dı́az 2010a)
with the aim of providing a semantically correct program transformation technique
that allows us to implement a sound and complete implementation of some useful instances of SQCLP on top of existing CLP systems like SICStus Prolog or
SWI-Prolog. In the introductory section of (Rodrı́guez-Artalejo and Romero-Dı́az
2010a) we have already summarized some related approaches of SQCLP with a
special emphasis on their declarative semantics and their main semantic differences
with SQCLP. In the next paragraphs we present a similar overview but, this time,
putting the emphasis on the goal resolution procedures and system implementation
techniques, when available.
Within the extensions of LP using annotations in program clauses we can find
the seminal proposal of quantitative logic programming by (van Emden 1986) that
inspired later works such as the GAP (generalized annotated programs) framework
by (Kifer and Subrahmanian 1992) and the QLP (qualified logic programming)
scheme by us (Rodrı́guez-Artalejo and Romero-Dı́az 2008). In the proposal of van
Emden, one can find a primitive goal solving procedure based in and/or trees (these
are similar to the alpha-beta trees used in game theory), used to prune the search
space when proving some specific ground atom for some certainty value in the
real interval [0, 1]. In the case of GAP, the goal solving procedure uses constrained
SLD resolution in conjunction with a—costly—computation of so-called reductants
between variants of program clauses. In contrast, QLP goal solving uses a more
efficient resolution procedure called SLD(D) resolution, implemented by means of
real domain constraints, used to compute the qualification value of the head atom
based on the attenuation factor of the program clause and the previously computed
qualification values of the body atoms. Admittedly, the gain in efficiency of SLD(D)
w.r.t. GAP’s goal solving procedure is possible because QLP focuses on a more
specialized class of annotated programs. While in all these three approaches there
are some results of soundness and completeness, the results for the QLP scheme
are the stronger ones (again, thanks to its also more focused scope w.r.t. GAP).
From a different viewpoint, extensions of LP supporting uncertainty can be
roughly classified into two major lines: approaches based in fuzzy logic (Zadeh 1965;
Hájek 1998) and approaches based in similarity relations. Historically, Fuzzy LP
languages were motivated by expert knowledge representation applications. Early
Fuzzy LP languages implementing the resolution principle introduced in (Lee 1972)
include Prolog-Elf (Ishizuka and Kanai 1985), Fril Prolog (Baldwin et al. 1995) and
F-Prolog (Li and Liu 1990). More recent approaches such as the Fuzzy LP languages in (Vojtáš 2001; Guadarrama et al. 2004) and Multi-Adjoint LP (MALP
for short) in the sense of (Medina et al. 2001a) use clause annotations and a fuzzy
interpretation of the connectives and aggregation operators occurring in program
clauses and goals. The Fuzzy Prolog system proposed in (Guadarrama et al. 2004)
is implemented by means of real constrains on top of a CLP(R) system, using a
syntactic expansion of the source code during the Prolog compilation. A complete
procedural semantics for MALP using reductants has been presented in (Medina

A Transformation-based Implementation for SQCLP (Preliminary Version) 3
et al. 2001b). A method for translating a MALP like program into standard Prolog
has been described in (Julián et al. 2009).
The second line of research mentioned in the previous paragraph was motivated
by applications in the field of flexible query answering. Classical LP is extended to
Similarity-based LP (SLP for short), leading to languages which keep the classical
syntax of LP clauses but use a similarity relation over a set of symbols S to allow
“flexible” unification of syntactically different symbols with a certain approximation
degree. Similarity relations over a given set S have been defined in (Zadeh 1971;
Sessa 2002) and related literature as fuzzy relations represented by mappings S : S×
S → [0, 1] which satisfy reflexivity, symmetry and transitivity axioms analogous to
those required for classical equivalence relations. Resolution with flexible unification
can be used as a sound and complete goal solving procedure for SLP languages as
shown e.g. in (Sessa 2002). SLP languages include Likelog (Arcelli and Formato
1999; Arcelli Fontana 2002) and more recently SiLog (Loia et al. 2004), which has
been implemented by means of an extended Prolog interpreter and proposed as a
useful tool for web knowledge discovery.
In the last years, the SLP approach has been extended in various ways. The
SQLP (similarity-based qualified logic programming) scheme proposed in (Caballero
et al. 2008) extended SLP by allowing program clause annotations in QLP style
and generalizing similarity relations to mappings S : S × S → D taking values
in a qualification domain not necessarily identical to the real interval [0, 1]. As
implementation technique for SQLP, (Caballero et al. 2008) proposed a semantically
correct program transformation into QLP, whose goal solving procedure has been
described above. Other related works on transformation-based implementations of
SLP languages include (Sessa 2001; Medina et al. 2004). More recently, the SLP
approach has been generalized to work with proximity relations in the sense of
(Dubois and Prade 1980) represented by mappings S : S × S → [0, 1] which satisfy
reflexivity and symmetry axioms but do not always satisfy transitivity. SLP like
languages using proximity relations include Bousi∼Prolog (Julián-Iranzo and RubioManzano 2009a) and the SQCLP scheme (Rodrı́guez-Artalejo and Romero-Dı́az
2010a). Two prototype implementations of Bousi∼Prolog are available: a low-level
implementation (Julián-Iranzo and Rubio-Manzano 2009b) based on an adaptation
of the classical WAM (called Similarity WAM) implemented in Java and able to
execute a Prolog program in the context of a similarity relation defined on the first
order alphabet induced by that program; and a high-level implementation (JuliánIranzo et al. 2009) done on top of SWI-Prolog by means of a program transformation
from Bousi∼Prolog programs into a so-called Translated BPL code than can be
executed according to the weak SLD resolution principle by a meta-interpreter.
Let us now refer to approaches related to constraint solving and CLP. An analogy of proximity relations in the context of partial constraint satisfaction can be
found in (Freuder and Wallace 1992), where several metrics are proposed to measure the proximity between the solution sets of two different constraint satisfaction
problems. Moreover, some extensions of LP supporting uncertain reasoning use
constraint solving as implementation technique, as discussed in the previous paragraphs. However, we are only aware of three approaches which have been conceived

4

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

as extensions of the classical CLP scheme proposed for the first time in (Jaffar and
Lassez 1987). These three approaches are: (Riezler 1998) that extends the formulation of CLP by (Höhfeld and Smolka 1988) with quantitative LP in the sense of
(van Emden 1986) and adapts van Emden’s idea of and/or trees to obtain a goal
resolution procedure; (Bistarelli et al. 2001) that proposes a semiring-based approach to CLP, where constraints are solved in a soft way with levels of consistency
represented by values of the semiring, and is implemented with clp(FD,S) for a
particular class of semirings which enable to use local consistency algorithms, as
described in (Georget and Codognet 1998); and the SQCLP scheme proposed in our
previous work (Rodrı́guez-Artalejo and Romero-Dı́az 2010a), which was designed
as a common extension of SQLP and CLP.
As we have already said at the beginning of this introduction, this paper deals
with transformation-based implementations of the SQCLP scheme. Our main results include: a) a transformation technique for transforming SQCLP programs
into semantically equivalent CLP programs via two specific program transformations named elimS and elimD ; and b) and a practical Prolog-based implementation
which relies on the aforementioned program transformations and supports several
useful SQCLP instances. As far as we know, no previous work has dealt with the
implementation of extended LP languages for uncertain reasoning which are able
to support clause annotations, proximity relations and CLP style programming. In
particular, our previous paper (Caballero et al. 2008) only presented a transformation analogous to elimS for a programming scheme less expressive than SQCLP,
which supported neither non-transitive proximity relations nor CLP programming.
Moreover, the transformation-based implementation reported in (Caballero et al.
2008) was not implemented in a system.
The reader is assumed to be familiar with the semantic foundations of LP (Lloyd
1987; Apt 1990) and CLP (Jaffar and Lassez 1987; Jaffar et al. 1998). The rest
of the paper is structured as follows: Section 2 presents a brief overview of the
semantics of the SQCLP scheme, focusing on the essential notions needed to understand the following sections and concluding with an abstract discussion of goal
solving procedures for SQCLP. Section 3 briefly discusses two specializations of
SQCLP, namely QCLP and CLP, which are used as the targets of the program
transformations elimS and elimD , respectively. Section 4 presents these two program transformations along with mathematical results which prove their semantic
correctness, relying on the declarative semantics of the SQCLP, QCLP and CLP
schemes. Section 5 presents a Prolog-based prototype system which relies on the
transformations proposed in the previous section and implements several useful SQCLP instances. Finally, Section 6 summarizes conclusions and points to some lines
of planned future research.
2 The Scheme SQCLP and its Declarative Semantics
We present in this section a short overview of the declarative semantics of the SQCLP scheme originally presented in (Rodrı́guez-Artalejo and Romero-Dı́az 2010a),
focusing on the essential notions needed to understand the following sections. In-

A Transformation-based Implementation for SQCLP (Preliminary Version) 5
terested readers are referred to (Rodrı́guez-Artalejo and Romero-Dı́az 2010a) and
its extended version (Rodrı́guez-Artalejo and Romero-Dı́az 2010b) for a full-fledged
exposition of SQCLP semantics and a discussion of various extended LP languages
for uncertain reasoning which can be obtained as specializations and instances of
SQCLP. Some technical notions and results from (Rodrı́guez-Artalejo and RomeroDı́az 2010b) will be cited along this paper when needed to support mathematical
proofs.
Constraint domains C, sets of constraints Π and their solutions, as well as terms,
atoms and substitutions over a given C are well known notions underlying the CLP
scheme. The reader is referred (Rodrı́guez-Artalejo and Romero-Dı́az 2010b) for a
relational formalization of constraint domains and some examples, including the real
constraint domain R. We assume the following classification of atomic C-constraints:
defined atomic constraints p(tn ), where p is a program-defined predicate symbol;
primitive constraints r(tn ) where r is a C-specific primitive predicate symbol; and
equations t == s.
We use ConC as a notation for the set of all C-constraints and κ as a notation for
an atomic primitive constraint. Constraints are interpreted by means of C-valuations
η ∈ ValC , which are ground substitutions. The set SolC (Π) of solutions of Π ⊆ ConC
includes all the valuations η such that Πη is true when interpreted in C. Π ⊆ ConC
is called satisfiable if SolC (Π) 6= ∅ and unsatisfiable otherwise. π ∈ ConC is entailed
by Π ⊆ ConC (noted Π |=C π) iff SolC (Π) ⊆ SolC (π).
Qualification domains were first introduced in (Rodrı́guez-Artalejo and RomeroDı́az 2008) with the aim of providing elements, called qualification values, which can
be attached to computed answers. They are defined as structures D = hD, P, b, t, ◦i
verifying the following requirements:
1. hD, P, b, ti is a lattice with extreme points b (called infimum or bottom element) and t (called maximum or top element) w.r.t. the partial ordering P
(called qualification ordering). For given elements d, e ∈ D, we write d u e for
the greatest lower bound (glb) of d and e, and d t e for the least upper bound
(lub) of d and e. We also write d C e as abbreviation for d P e ∧ d 6= e.
2. ◦ : D × D → D, called attenuation operation, verifies the following axioms:
(a)
(b)
(c)
(d)

◦ is associative, commutative and monotonic w.r.t. P.
∀d ∈ D : d ◦ t = d and d ◦ b = b.
∀d, e ∈ D : d ◦ e P e and even b 6= d ◦ e P e if d, e ∈ D \ {b}.
∀d, e1 , e2 ∈ D : d ◦ (e1 u e2 ) = (d ◦ e1 ) u (d ◦ e2 ).

For any S = {e1 , e2 , . . . , en } ⊆ D, the glb (also called infimum of S) exists and can
d
be computed as S = e1 u e2 u · · · u en (which reduces to t in the case n = 0). The
dual claim concerning lubs is also true. As an easy consequence of the axioms, one
d
d
gets the identity d ◦ S = {d ◦ e | e ∈ S}.
Technical details, explanations and examples can be found in (Rodrı́guez-Artalejo
and Romero-Dı́az 2010b), including: the qualification domain B of classical boolean
values, the qualification domain U of uncertainty values, the qualification domain
W of weight values, and other qualification domains built from these by means of

6

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

the strict cartesian product operation ⊗. The following definition is borrowed from
(Rodrı́guez-Artalejo and Romero-Dı́az 2010a):
Definition 2.1 (Expressing D in C)
A qualification domain D is expressible in a constraint domain C if there is an
injective embedding mapping ı : D \ {b} → C and moreover:
1. There is a C-constraint qVal(X) such that SolC (qVal(X)) is the set of all
η ∈ ValC verifying η(X) ∈ ran(ı).
2. There is a C-constraint qBound(X, Y, Z) encoding “x P y ◦ z” in the following
sense: any η ∈ ValC such that η(X) = ι(x), η(Y ) = ι(y) and η(Z) = ι(z)
verifies η ∈ SolC (qBound(X, Y, Z)) iff x P y ◦ z.
In addition, if qVal(X) and qBound(X, Y, Z) can be chosen as existential constraints
of the form ∃X1 . . . ∃Xn (B1 ∧ . . . ∧ Bm )—where Bj (1 ≤ j ≤ m) are atomic—we
say that D is existentially expressible in C.
It can be proved that B, U, W and and any qualification domain built from these
with the help of ⊗ are existentially expressible in any constraint domain C that
includes the basic values and computational features of R.
Admissible triples hS, D, Ci consist of a constraint domain C, a qualification domain D and a proximity relation S : S × S → D—where D is the carrier set of
D and S is the set of all variables, basic values and signature symbols available in
C—satisfying the following properties:
• ∀x ∈ S : S(x, x) = t (reflexivity).
• ∀x, y ∈ S : S(x, y) = S(y, x) (symmetry).
• Some additional technical conditions explained in (Rodrı́guez-Artalejo and
Romero-Dı́az 2010b).
A proximity relation S is called similarity iff it satisfies the additional property
∀x, y, z ∈ S : S(x, z) Q S(x, y) u S(y, z) (transitivity). The scheme SQCLP has
instances SQCLP(S, D, C) where hS, D, Ci is an admissible triple.
A SQCLP(S, D, C)-program is a set P of qualified program rules (also called
α
qualified clauses) C : A ←
− B1 ]w1 , . . . , Bm ]wm , where A is a defined atom, α ∈
D \ {b} is called the attenuation factor of the clause and each Bj ]wj (1 ≤ j ≤ m)
is an atom Bj annotated with a so-called threshold value wj ∈ (D \ {b}) ] {?}. The
intended meaning of C is as follows: if for all 1 ≤ j ≤ m one has Bj ]ej (meaning
that Bj holds with qualification value ej ) for some ej Q? wj , then A]d (meaning
that A holds with qualification value d) can be inferred for any d ∈ D \ {b} such
dm
that d P α ◦ j=1 ej . By convention, ej Q? wj means ej Q wj if wj 6= ? and is
identically true otherwise. In practice threshold values equal to ‘?’ and attenuation
values equal to t can be omitted.
Figure 1 shows a simple SQCLP(Ss , U, R)-program Ps which illustrates the expressivity of the SQCLP scheme to deal with problems involving flexible information retrieval. Predicate search can be used to answer queries asking for books
in the library matching some desired language, genre and reader level. Predicate
guessRdrLvl takes advantage of attenuation factors to encode heuristic rules to

A Transformation-based Implementation for SQCLP (Preliminary Version) 7
% Book representation: book( ID, Title, Author, Lang, Genre, VocLvl, Pages ).
1

library([ book(1, ‘Tintin’, ‘Hergé’, french, comic, easy, 65),

2

book(2, ‘Dune’, ‘F.P. Herbert’, english, sciFi, medium, 345),

3

book(3, ‘Kritik der reinen Vernunft’, ‘I. Kant’, german, philosophy, difficult, 1011),

4

book(4, ‘Beim Hauten der Zwiebel’, ‘G. Grass’, german, biography, medium, 432) ])
% Auxiliary predicate for computing list membership:

5

member(B, [B| ])

6

member(B, [ |T]) ← member(B, T)
% Predicates for getting the explicit attributes of a given book:

7

getId(book(ID, Title, Author, Lang, Genre, VocLvl, Pages), ID)

8

getTitle(book( ID, Title, Author, Lang, Genre, VocLvl, Pages), Title)

9

getAuthor(book( ID, Title, Author, Lang, Genre, VocLvl, Pages), Author)

10

getLanguage(book( ID, Title, Author, Lang, Genre, VocLvl, Pages), Lang)

11

getGenre(book( ID, Title, Author, Lang, Genre, VocLvl, Pages), Genre)

12

getVocLvl(book( ID, Title, Author, Lang, Genre, VocLvl, Pages), VocLvl)

13

getPages(book( ID, Title, Author, Lang, Genre, VocLvl, Pages), Pages)
% Function for guessing the reader level of a given book:

14

guessRdrLvl(B, basic) ← getVocLvl(B, easy), getPages(B, N), N < 50

15

guessRdrLvl(B, intermediate) ←−− getVocLvl(B, easy), getPages(B, N), N ≥ 50

16

guessRdrLvl(B, basic) ←−− getGenre(B, children)

17

guessRdrLvl(B, proficiency) ←−− getVocbLvl(B, difficult), getPages(B, N), N ≥ 200

0.8

0.9

0.9

0.8

18

guessRdrLvl(B, upper) ←−− getVocLvl(B, difficult), getPages(B, N), N < 200

19

guessRdrLvl(B, intermediate) ←−− getVocLvl(B, medium)

20

guessRdrLvl(B, upper) ←−− getVocLvl(B, medium)

0.8

0.7

% Function for answering a particular kind of user queries:
21

search(Lang, Genre, Level, Id) ← library(L)#1.0, member(B, L)#1.0,

22

getLanguage(B, Lang), getGenre(B, Genre),

23

guessRdrLvl(B, Level), getId(B, Id)#1.0
% Proximity relation Ss :

24

Ss (sciFi, fantasy) = Ss (fantasy, sciFi) = 0.9

25

Ss (adventure, fantasy) = Ss (fantasy, adventure) = 0.7

26

Ss (essay, philosophy) = Ss (philosophy, essay) = 0.8

27

Ss (essay, biography) = Ss (biography, essay) = 0.7

Fig. 1. SQCLP(Ss , U, R)-program Ps (Library with books in different languages)
compute reader levels on the basis of vocabulary level and other book features.
The other predicates compute book features in the natural way, and the proximity
relation Ss allows flexibility in any unification (i.e. solving of equality constraints)
arising during the invocation of the program predicates.
The declarative semantics of a given SQCLP(S, D, C)-program P relies on qualified constrained atoms (briefly qc-atoms) of the form A]d ⇐ Π, intended to assert

8

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

that the validity of atom A with qualification degree d ∈ D is entailed by the constraint set Π. A qc-atom is called defined, primitive or equational according to the
syntactic form of A; and it is called observable iff d ∈ D \ {b} and Π is satisfiable.
Program interpretations are defined as sets of observable qc-atoms which obey a
natural closure condition. The results proved in (Rodrı́guez-Artalejo and RomeroDı́az 2010a) show two equivalent ways to characterize declarative semantics, using a
fix-point approach and a proof-theoretical approach, respectively. For the purposes
of the present paper it suffices to consider the proof theoretical approach, that relies
on a formal inference system called Proximity-based Qualified Constrained Horn
Logic—in symbols, SQCHL(S, D, C)—intended to infer observable qc-atoms from
P and consisting of the three inference rules displayed in Figure 2. Rule SQEA
depends on a relation ≈d,Π between terms that is defined in the following way:
t ≈d,Π s iff there exist two terms t̂ and ŝ such that Π |=C t == t̂, Π |=C s == ŝ and
b 6= d P S(t̂, ŝ). This allows to deduce equations from Π in a flexible way, taking
the proximity relation S into account. The reader is referred to (Rodrı́guez-Artalejo
and Romero-Dı́az 2010b) for more motivating comments on SQCHL(S, D, C) and
some technical properties of the ≈d,Π relation.

SQDA

( (t0i == ti θ)]di ⇐ Π )i=1...n ( Bj θ]ej ⇐ Π )j=1...m
p0 (t0 n )]d ⇐ Π
α

if (p(tn ) ←
− B1 ]w1 , . . . , Bm ]wm ) ∈ P, θ subst., S(p0 , p) = d0 6= b,
d
dm
?
ej Q wj (1 ≤ j ≤ m) and d P n
i=0 di u α ◦
j=1 ej .
SQEA

(t == s)]d ⇐ Π

if t ≈d,Π s.

SQPA

κ]d ⇐ Π

if Π |=C κ.

Fig. 2. Proximity-based Qualified Constrained Horn Logic

We will write P `S,D,C ϕ to indicate that ϕ can be deduced from P in SQCHL(S,
D, C), and P `kS,D,C ϕ in the case that the deduction can be performed with exactly
k SQDA inference steps. As usual in formal inference systems, SQCHL(S, D, C)
proofs can be represented as proof trees whose nodes correspond to qc-atoms, each
node being inferred from its children by means of some SQCHL(S, D, C) inference step. The following theorem, proved in (Rodrı́guez-Artalejo and Romero-Dı́az
2010b), characterizes least program models in the scheme SQCLP. This result allows
to use SQCHL(S, D, C)-derivability as a logical criterion for proving the semantic
correctness of program transformations, as we will do in Section 4.
Theorem 2.1 (Logical characterization of least program models in SQCHL)
For any SQCLP(S, D, C)-program P, its least model can be characterized as:
MP = {ϕ | ϕ is an observable defined qc-atom and P `S,D,C ϕ}.
Let us now discuss goals and their solutions. Goals for a given SQCLP(S, D, C)-

A Transformation-based Implementation for SQCLP (Preliminary Version) 9
program P have the form
G : A1 ]W1 , . . . , Am ]Wm 8 W1 Q? β1 , . . . , Wm Q? βm

abbreviated as (Ai ]Wi , Wi Q? βi )i=1...m . The Ai ]Wi are called annotated atoms.
The pairwise different variables Wi ∈ War are called qualification variables; they
are taken from a set War assumed to be disjoint from the set Var of data variables
used in terms. The conditions Wi Q? βi (with βi ∈ (D \ {b}) ] {?}) are called
threshold conditions and their intended meaning (relying on the notations ‘?’ and
‘Q? ’) is as already explained when introducing program clauses above. In the sequel,
war(o) will denote the set of all qualification variables occurring in the syntactic
object o. In particular, for a goal G as displayed above, war(G) denotes the set
{Wi | 1 ≤ i ≤ m}. In the case m = 1 the goal is called atomic. The following
definition relies on SQCHL(S, D, C)-derivability to provide a natural declarative
notion of goal solution:
Definition 2.2 (Goal Solutions)
Assume a given SQCLP(S, D, C)-program P and a goal G for P with the syntax
displayed above. Then:
1. A solution for G is any triple hσ, µ, Πi such that σ is a C-substitution, Wµ ∈
D \ {b} for all W ∈ dom(µ), Π is a satisfiable and finite set of atomic Cconstraints and the following two conditions hold for all i = 1 . . . m: Wi µ =
di Q? βi and P `S,D,C Ai σ]Wi µ ⇐ Π. The set of all solutions for G w.r.t. P
is noted SolP (G).
2. A solution hη, ρ, Πi for G is called ground iff Π = ∅ and η ∈ ValC is a variable
valuation such that Ai η is a ground atom for all i = 1 . . . m. The set of all
ground solutions for G w.r.t. P is noted GSolP (G) ⊆ SolP (G).
3. A ground solution hη, ρ, ∅i ∈ GSolP (G) is subsumed by hσ, µ, Πi iff there is
some ν ∈ SolC (Π) s.t. η =var(G) σν and Wi ρ P Wi µ for i = 1 . . . m.
A possible goal Gs for the library program displayed in Figure 1 is
Gs : search(german, essay, intermediate, ID)#W 8 W ≥ 0.65

and one solution for Gs is h{ID 7→ 4}, {W 7→ 0.7}, ∅i. In this simple case, the
constraint set Π within the solution is empty. Other examples of goal solutions can
be found in (Rodrı́guez-Artalejo and Romero-Dı́az 2010b) and Sections 4 and 5
below.
In practice, users of SQCLP languages will rely on some available goal solving
system for computing goal solutions. The following definition specifies two important abstract properties of goal solving systems which will be taken as a reference
for the implementation presented in this paper.
Definition 2.3 (Correct Abstract Goal Solving Systems)
An abstract goal solving system for SQCLP(S, D, C) is any device that takes a
program P and a goal G as input and yields various triples hσ, µ, Πi, called computed
answers, as outputs. Such a goal solving system is called:
1. Sound iff every computed answer is a solution hσ, µ, Πi ∈ SolP (G).

10

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az
2. Weakly complete iff every ground solution hη, ρ, ∅i ∈ GSolP (G) is subsumed
by some computed answer.
3. Correct iff it is both sound and weakly complete.

Every goal solving system for a SQCLP instance should be sound and ideally also
weakly complete. In principle, goal solving systems with these properties for extensions of the classical LP paradigm can be formalized as extensions of the well-known
SLD-resolution method (Lloyd 1987; Apt 1990). A sound and complete extensions
of SLD-resolution for the CLP scheme can be found e.g. in (Jaffar et al. 1998), and
several extensions of SLD resolution for LP languages aiming at uncertain reasoning
SQCLP scheme have been mentioned in Section 1.
Our aim in this paper is to present an implementation based on a semantically
correct program transformation from SQCLP into CLP, rather than developing a
sound and complete extension of SLD resolution. Nevertheless, both our implementation and SLD-based approaches for SLP languages in the line of (Sessa 2002)
must share the ability to solve unification problems w.r.t. to a proximity relation
S : S × S → [0, 1] over signature symbols, which is assumed to be transitive in
(Sessa 2002) but not in our setting. The lack of transitivity makes a crucial difference w.r.t. the behavior of unification algorithms. In the rest of this section we
briefly discuss the problem by means of a simple example.
(Sessa 2002) presents a flexible unification algorithm for solving unification problems represented as systems of the form S 8 α, where S is a set of equations between
terms and α is a certainty degree. A solution of such a system is any substitution θ
which verifies S(sθ, tθ) ≥ α for all equations s == t belonging to S. This notion of
solution is consistent with the declarative semantics of the SQCLP scheme (more
specifically, with Definition 2.2), even in the case that S is a non-transitive proximity relation. Following a traditional approach, Sessa presents the flexible unification
algorithm as set of transformation rules which convert systems S 8 α into solved
form systems which represent unifiers. The transformations are similar to those
presented in e.g. Section 4.6 of (Baader and Nipkow 1998) for the case of classical
syntactic unification, extended with suitable computations to update α during the
process, taking the given similarity relation S into account. One of the transformations allows to transform a system of the form X == t, S 8 α into S{X 7→ t} 8 α
(provided that X is not identical to t and does not occur in t, the so-called occurs
check). Unfortunately, this transformation can lose solutions in case that S is not
transitive. Consider for instance the following example:
Example 2.1
Assume constants a, b, c and a non-transitive proximity relation S such that
S(a, b) = S(b, a) = 0.7; S(a, c) = S(c, a) = 0.8; S(b, c) = S(c, b) = 0. Then,
the substitution θ = {X 7→ a} is obviously a solution of the unification problem
X == b, X == c 8 0.7. Nevertheless, the unification algorithm presented in (Sessa
2002) and related papers fails without computing any solution:
X == b, X == c 8 0.7 =⇒ X == c {X 7→ b} 8 0.7 =⇒ fail
The second transformation step leads to fail because X == c {X 7→ b} 8 0.7 is

A Transformation-based Implementation for SQCLP (Preliminary Version) 11
the same as b == c 8 0.7 and S(b, c) = 0 < 0.7. Should S satisfy transitivity, then
S(b, c) = S(c, b) ≥ 0.7, and Sessa’s unification algorithm would compute the unifier
σ = {X 7→ b} as follows:
X == b, X == c 8 0.7 =⇒ X == c {X 7→ b} 8 0.7 =⇒ {X 7→ b} 8 0.7

Note that σ is more general than θ in the sense that S(θ, σθ) = S(θ, σ) ≥ 0.7.
Therefore this example does not contradict the completeness of Sessa’s unification
algorithm for the case of (transitive) similarity relations.
Even in the case that S is transitive, we have found examples showing that a
goal solving system based on Sessa’s unification algorithm can fail to compute some
valid solutions for SQCLP(S, D, C)-programs whose clauses use attenuation factors
other than t. The unification algorithm underlaying the implementations presented
in Section 5—based on the program transformations from Section 4—avoids the
problematic transformation step X == t, S 8 α =⇒ S{X 7→ t} 8 α, that might cause
incompleteness; instead, Prolog’s backtracking is used to implement the effect of
a non-deterministic choice between several transformation steps X == c(tn ), S 8
α =⇒ X1 == t1 , . . . , Xn == tn , Sµ 8 α, where X1 , . . . , Xn are fresh variables and
µ = {X 7→ c0 (X n )} for some possible choice of c0 such that S(c, c0 ) ≥ α.
As an optimization, our prototype system allows the user to use a directive whose
effect is that the system avoids the backtracking search just discussed and implements just the effect of the transformation X == t, S 8 α =⇒ S{X 7→ t} 8 α. When
including this directive, the user runs the risk of losing some valid solutions. We
conjecture that no incompleteness occurs in the case of SQCLP(S, D, C)-programs
based on a transitive S and whose clauses do not use attenuation factors other than
t; i.e. SLP programs enriched with constraint solving.
3 The Schemes QCLP & CLP as Specializations of SQCLP
As discussed in the concluding section of (Rodrı́guez-Artalejo and Romero-Dı́az
2010a), several specializations of the SQCLP scheme can be obtained by partial
instantiation of its parameters. In particular, QCLP and CLP can be defined as
schemes with instances:
QCLP(D, C) =def SQCLP(Sid , D, C)
CLP(C) =def SQCLP(Sid , B, C) = QCLP(B, C)
where Sid is the identity proximity relation and B is the qualification domain including just the two classical boolean values. As explained in the introduction, QCLP
and CLP are the targets of the two program transformations to be developed in
Section 4. In this brief section we provide an explicit description of the syntax and
semantics of these two schemes, derived from their behavior as specializations of
SQCLP.
3.1 Presentation of the QCLP Scheme
As already explained, the instances of QCLP can be defined by the equation
QCLP(D,C) = SQCLP(Sid ,D,C). Due to the admissibility of the parameter triple

12

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

hSid , D, Ci, the qualification domain D must be (existentially) expressible in the constraint domain C. Technically, the QCLP scheme can be seen as a common extension
of the classical CLP scheme for Constraint Logic Programming (Jaffar and Lassez
1987; Jaffar et al. 1998) and the QLP scheme for Qualified Logic Programming
originally introduced in (Rodrı́guez-Artalejo and Romero-Dı́az 2008). Intuitively,
QCLP programming behaves like SQCLP programming, except that proximity information other than the identity is not available for proving equalities.
Program clauses and observable qc-atoms in QCLP are defined in the same way
as in SQCLP. The library program Ps in Figure 1 becomes a QCLP( U, R)-program
Ps0 just by replacing Sid for S. Of course, Ps0 does not support flexible unification
as it was the case with Ps .
As explained in Section 2, the proof system consisting of the three displayed in
Figure 2 characterizes the declarative semantics of a given SQCLP(S, D, C)-program
P. In the particular case S = Sid , the inference rules specialize to those displayed
in Figure 3, yielding a formal proof system called Qualified Constrained Horn Logic
– in symbols, QCHL(D, C) – which characterizes the declarative semantics of a
given QCLP(D, C)-program P. Note that rule SQEA depends on a relation ≈Π
between terms that is defined to behave the same as the specialization of ≈d,Π to
the case S = Sid . It is easily checked that t ≈Π s does not depend on d and holds
iff Π |=C t == s. Both ≈d,Π and ≈Π allow to use the constraints within Π when
deducing equations. However, c(tn ) ≈Π c0 (sn ) never holds in the case that c and c0
are not syntactically identical.

QDA

( (t0i == ti θ)]di ⇐ Π )i=1...n ( Bj θ]ej ⇐ Π )j=1...m
p(t0 n )]d ⇐ Π
α

if (p(tn ) ←
− B1 ]w1 , . . . , Bm ]wm ) ∈ P, θ subst.,
d
dm
ej Q? wj (1 ≤ j ≤ m) and d P n
i=1 di u α ◦
j=1 ej .
QEA

(t == s)]d ⇐ Π

if t ≈Π s.

QPA

κ]d ⇐ Π

if Π |=C κ.

Fig. 3. Qualified Constrained Horn Logic

SQCHL(S, D, C) proof trees and the notations related to them can be naturally
specialized to QCHL(D, C). In particular, we will use the notation P `D,C ϕ (resp.
P `kD,C ϕ) to indicate that the qc-atom ϕ can be inferred in QCHL(D, C) from
the program P (resp. it can be inferred by using exactly k QDA inference steps).
Theorem 2.1 also specializes to QCHL, yielding the following result:
Theorem 3.1 (Logical characterization of least program models in QCHL)
For any QCLP(D, C)-program P, its least model can be characterized as:
MP = {ϕ | ϕ is an observable defined qc-atom and P `D,C ϕ}.

A Transformation-based Implementation for SQCLP (Preliminary Version) 13
Concerning goals and their solutions, their specialization to the particular case
S = Sid leaves the syntax of goals G unaffected and leads to the following definition,
almost identical to Definition 2.2:
Definition 3.1 (Goal Solutions in QCLP )
Assume a given QCLP(S, D)C-program P and a goal G : ( Ai ]Wi , Wi Q? βi )i=1...m .
Then:
1. A solution for G is any triple hσ, µ, Πi such that σ is a C-substitution, W µ ∈
D \ {b} for all W ∈ dom(µ), Π is a satisfiable and finite set of atomic Cconstraints, and the following two conditions hold for all i = 1 . . . m: Wi µ =
di Q? βi and P `D,C Ai σ]Wi µ ⇐ Π. The set of all solutions for G is noted
SolP (G).
2. A solution hη, ρ, Πi for G is called ground iff Π = ∅ and η ∈ ValC is a variable
valuation such that Ai η is a ground atom for all i = 1 . . . m. The set of all
ground solutions for G is noted GSolP (G) ⊆ SolP (G).
3. A ground solution hη, ρ, ∅i ∈ GSolP (G) is subsumed by hσ, µ, Πi iff there is
some ν ∈ SolC (Π) s.t. η =var(G) σν and Wi ρ P Wi µ for i = 1 . . . m.
Finally, the notion of correct abstract goal solving system for SQCLP given in
Definition 2.3 specializes to QCLP without any formal change. Therefore, we state
no new definition at this point.

3.2 Presentation of the CLP Scheme
As already explained, the instances of CLP can be defined by the equation CLP(C)
= SQCLP(Sid , B, C), or equivalently, CLP(C) = QCLP(B, C). Due to the fixed choice
D = B, the only qualification value d ∈ D\{b} available for use as attenuation factor
or threshold value is d = t. Therefore, CLP can only include threshold values equal
to ‘?’ and attenuation values equal to the top element t = true of B. As explained
in Section 2, such trivial threshold and attenuation values can be omitted, and CLP
clauses can be written with the simplified syntax A ← B1 , . . . , Bm .
Since t = true is the only non-trivial qualification value available in CLP, qcatoms A]d ⇐ Π are always of the form A]true ⇐ Π and can be written as
A ⇐ Π. Moreover, all the side conditions for the inference rule QDA in Figure
3 become trivial when specialized to the case D = B. Therefore, the specialization of QCHL(D, C) to the case D = B leads to the formal proof system called
Constrained Horn Logic – in symbols, CHL(C) – consisting of the three inference
rules displayed in Figure 4, which characterizes the declarative semantics of a given
CLP(C)-program P.
QCHL(D, C) proof trees and the notations related to them can be naturally
specialized to CHL(C). In particular, we will use the notation P `ϕ (resp. P `k ϕ)
to indicate that the qc-atom ϕ can be inferred in CHL(C) from the program P
(resp. it can be inferred by using exactly k DA inference steps). Theorem 3.1 also
specializes to CHL, yielding the following result:

14

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

DA

( (t0i == ti θ) ⇐ Π )i=1...n ( Bj θ ⇐ Π )j=1...m
p(t0 n ) ⇐ Π
if (p(tn ) ← B1 , . . . , Bm ) ∈ P and θ subst.

EA

(t == s) ⇐ Π

if t ≈Π s.

PA

κ⇐Π

if Π |=C κ.

Fig. 4. Constrained Horn Logic

Theorem 3.2 (Logical characterization of least program models in CHL)
For any CLP(C)-program P, its least model can be characterized as:
MP = {ϕ | ϕ is an observable defined qc-atom and P `ϕ }.
Concerning goals and their solutions, their specialization to the scheme CLP
leads to the following definition:
Definition 3.2 (Goals and their Solutions in CLP)
Assume a given CLP(C)-program P. Then:
1. Goals for P have the form G : A1 , . . . , Am , abbreviated as ( Ai )i=1...m , where
Ai (1 ≤ i ≤ m) are atoms.
2. A solution for a goal G is any pair hσ, Πi such that σ is a C-substitution, Π is
a satisfiable and finite set of atomic C-constraints, and P `C Ai σ ⇐ Π holds
for all i = 1 . . . m. The set of all solutions for G is noted SolP (G).
3. A solution hη, Πi for G is called ground iff Π = ∅ and η ∈ ValC is a variable
valuation such that Ai η is a ground atom for all i = 1 . . . m. The set of all
ground solutions for G is noted GSolP (G). Obviously, GSolP (G) ⊆ SolP (G).
4. A ground solution hη, ∅i ∈ GSolP (G) is subsumed by hσ, Πi iff there is some
ν ∈ SolC (Π) s.t. η =var(G) σν.
The notion of correct abstract goal solving system for SQCFLP given in Definition
2.3 specializes to CLP with only minor formal changes, as follows:
Definition 3.3 (Correct Abstract Goal Solving Systems for CLP)
A goal solving system for CLP(C) is any effective procedure which takes a program
P and a goal G as input and yields various pairs hσ, Πi, called computed answers,
as outputs. Such a goal solving system is called:
1. Sound iff every computed answer is a solution hσ, Πi ∈ SolP (G).
2. Weakly complete iff every ground solution hη, ∅i ∈ GSolP (G) is subsumed by
some computed answer.
3. Correct iff it is both sound and weakly complete.
We close this Subsection with a technical lemma that will be useful for proving
some results in Subsection 4.2:

A Transformation-based Implementation for SQCLP (Preliminary Version) 15
Lemma 3.1
Assume an existential C-constraint π(X n ) = ∃Y1 . . . ∃Yk (B1 ∧ . . . ∧ Bm ) with free
variables X n and a given CLP(C)-program P including the clause C : p(X n ) ←
B1 , . . . , Bm , where p ∈ DP n does not occur at the head of any other clause of P.
Then, for any n-tuple tn of C-terms and any finite and satisfiable Π ⊆ ConC , one
has:
1. P `C (p(tn ) ⇐ Π) =⇒ Π |=C π(tn ), where π(tn ) stands for the result of
applying the substitution {X n 7→ tn } to π(X n ).
2. The opposite implication Π |=C π(tn ) =⇒ P `C (p(tn ) ⇐ Π) holds if tn
is a ground term tuple. Note that for ground tn the constraint entailment
Π |=C π(tn ) simply means that π(tn ) is true in C.
3. Π |=C π(tn ) =⇒ P `C (p(tn ) ⇐ Π) may fail if tn is not a ground term tuple.
Proof
We prove each item separately:
1. Assume P `C (p(tn ) ⇐ Π). Note that C is the only clause for p in P and that each
atom Bj in C’s body is an atomic constraint. Therefore, the CHL(C) proof must
use a DA step based on an instance Cθ of clause C such that Π |=C ti == Xi θ
holds for all 1 ≤ i ≤ n and Π |= Bj θ holds for all 1 ≤ j ≤ m. These conditions and
the syntactic form of π(X n ) obviously imply Π |=C π(tn ).
2. Assume now Π |=C π(tn ) and tn ground. Then π(tn ) is true in C, and due to the
syntactic form of π(X n ), there must be some substitution θ such that Xi θ = ti
(syntactic identity) for all 1 ≤ i ≤ n and Bj θ is ground and true in C for all
1 ≤ j ≤ m. Trivially, Π |=C ti == Xi θ holds for all 1 ≤ i ≤ n and Π |=C Bj θ also
holds for all 1 ≤ j ≤ m. Then, it is obvious that P `C (p(tn ) ⇐ Π) can be proved
by using a DA step based on the instance Cθ of clause C.
3. We prove that Π |=C π(tn ) =⇒ P `C (p(tn ) ⇐ Π) can fail if tn is not ground
by presenting a counterexample based on the constraint domain R, using the syntax for R-constraints explained in (Rodrı́guez-Artalejo and Romero-Dı́az 2010b).
Consider the existential R-constraint π(X) = ∃Y (op+ (Y, Y, X)), and a CLP(R)program P including the clause C : p(X) ← op+ (Y, Y, X) and no other occurrence
of the defined predicate symbol p. Consider also Π = {cp≥ (X, 0.0)} and t = X.
Then Π |=R π(X) is obviously true, because any real number x ≥ 0.0 satisfies
∃Y (op+ (Y, Y, x)) in R. However, there is no R-term s such that Π |=R op+ (s, s, X),
and therefore there is no instance Cθ of clause C that can be used to prove
P `C (p(X) ⇐ Π) by applying a DA step.
4 Implementation by Program Transformation
The purpose of this section is to introduce a program transformation that transforms SQCLP(S, D, C) programs and goals into semantically equivalent CLP(C)
programs and goals. This transformation is performed as the composition of the
two following specific transformations:

16

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az
1. elimS — Eliminates the proximity relation S of arbitrary SQCLP(S, D, C)
programs and goals, producing equivalent QCLP(D, C) programs and goals.
2. elimD — Eliminates the qualification domain D of arbitrary QCLP(D, C)
programs and goals, producing equivalent CLP(C) programs and goals.

Thus, given a SQCLP(S, D, C)-program P—resp. SQCLP(S, D, C)-goal G—, the
composition of the two transformations will produce an equivalent CLP(C)-program
elimD (elimS (P))—resp. CLP(C)-goal elimD (elimS (G))—.
Example 4.1 (Running example: SQCLP(Sr , U⊗W, R)-program Pr )
As a running example for this section, consider the SQCLP(Sr , U⊗W, R)-program
Pr as follows:
(0.9,1)

R1

famous(sha) ←−−−−

R2

wrote(sha, kle) ←−−−

R3

wrote(sha, hamlet) ←−−−

R4

good work(G) ←−−−−− famous(A)#(0.5,100), authored(A, G)

(1,1)

(1,1)

(0.75,3)

S1

Sr (wrote, authored) = Sr (authored, wrote) = (0.9,0)

S2

Sr (kle, kli) = Sr (kli, kle) = (0.8,2)

where the constants shakespeare, king lear and king liar have been respectively
replaced, for clarity purposes in the subsequent examples, by sha, kle and kli.
In addition, consider the SQCLP(Sr , U⊗W, R)-goal Gr as follows:
good work(X)#W 8 W Q? (0.5,10)
We will illustrate the two transformation by showing, in subsequent examples,
the program clauses of elimS (Pr ) and elimD (elimS (Pr )) and the goals elimS (Gr )
and elimD (elimS (Gr )).
The next two subsections explain each transformation in detail.

4.1 Transforming SQCLP into QCLP
In this subsection we assume that the triple hS, D, Ci is admissible. In the sequel
we say that a defined predicate symbol p ∈ DP n is affected by a SQCLP(S, D, C)program P iff S(p, p0 ) 6= b for some p0 occurring in P. We also say that an atom
A is relevant for P iff some of the three following cases hold: a) A is an equation
t == s; b) A is a primitive atom κ; or c) A is a defined atom p(tn ) such that p is
affected by P.
As a first step towards the definition of the first program transformation elimS ,
we define a set EQS of QCLP(D, C) program clauses that emulates the behavior
of equations in SQCLP(S, D, C). The following definition assumes that the binary
predicate symbol ∼ ∈ DP 2 (used in infix notation) and the nullary predicate symbols payλ ∈ DP 0 are not affected by P.

A Transformation-based Implementation for SQCLP (Preliminary Version) 17
Definition 4.1
We define EQS as the following QCLP(D, C)-program:
t

EQS =def { X ∼ Y ←
− (X == Y )]? }
S
t
{ u ∼ u0 ←
− payλ ]? | u, u0 ∈ BC and S(u, u0 ) = λ 6= b }
S
t
{ c(X n ) ∼ c0 (Y n ) ←
− payλ ]?, ( (Xi ∼ Yi )]? )i=1...n | c, c0 ∈ DC n
and S(c, c0 ) = λ 6= b }
S
λ
{ payλ ←
− | for each λ ∈ D \ {b} }.
The following lemma shows the relation between the semantics of equations in
SQCHL(S, D, C) and the behavior of the binary predicate symbol ‘∼’ defined by
EQS in QCHL(D, C).
Lemma 4.1
Consider any two arbitrary terms t and s; EQS defined as in Definition 4.1; and a
satisfiable finite set Π of C-constraints. Then, for every d ∈ D \ {b}:
t ≈d,Π s ⇐⇒ EQS `D,C (t ∼ s)]d ⇐ Π .
Proof
We separately prove each implication.
[=⇒] Assume t ≈d,Π s. Then, there are two terms t̂, ŝ such that:
(1) t ≈Π t̂

(2) s ≈Π ŝ

(3) t̂ ≈d ŝ

We use structural induction on the form of the term t̂.
• t̂ = Z, Z ∈ Var. From (3) we have ŝ = Z. Then (1) and (2) become t ≈Π Z and
s ≈Π Z, therefore t ≈Π s. Now EQS `D,C (t ∼ s)]d ⇐ Π can be proved with a
proof tree rooted by a QDA step of the form:
(t == Xθ)]t ⇐ Π

(s == Y θ)]t ⇐ Π
(t ∼ s)]d ⇐ Π

(X == Y )θ]t ⇐ Π

t

using the clause X ∼ Y ←
− (X == Y )]? ∈ EQS instantiated by the substitution
θ = {X 7→ t, Y 7→ s}. Therefore the three premises can be derived from EQS
with QEA steps since t ≈Π t, s ≈Π s and t ≈Π s, respectively. Checking the side
conditions of all inference steps is straightforward.
• t̂ = u, u ∈ BC . From (3) we have ŝ = u0 for some u0 ∈ BC such that d P λ =
S(u, u0 ). Then (1) and (2) become t ≈Π u and s ≈Π u0 , which allow to build a
proof of EQS `D,C (t ∼ s)]d ⇐ Π by means of a QDA step using the clause
t

u ∼ u0 ←
− payλ ]?.
• t̂ = c, c ∈ DC 0. From (3) we have ŝ = c0 for some c0 ∈ DC 0 such that d P λ =
S(c, c0 ). Then (1) and (2) become t ≈Π c and s ≈Π c0, which allow us to build
a proof of EQS `D,C (t ∼ s)]d ⇐ Π by means of a QDA step using the clause
t

c ∼ c0 ←
− payλ ]?.
• t̂ = c(tn ), c ∈ DC n with n > 0. In this case, and because of (3), we can assume
ŝ = c0 (sn ) for some c0 ∈ DC n satisfying d P d0 =def S(c, c0 ) and d P di =def S(ti , si )

18

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

for i = 1 . . . n. Then EQS `D,C (t ∼ s)]d ⇐ Π with a proof tree rooted by a QDA
step of the form:
(t == c(tn ))]t ⇐ Π
payd0 ]d0 ⇐ Π
0
(s == c (sn ))]t ⇐ Π
( (ti ∼ si )]di ⇐ Π )i=1...n
(t ∼ s)]d ⇐ Π
t

using the EQS clause C : c(X n ) ∼ c0 (Y n ) ←
− payd0 ]?, ((Xi ∼ Yi )]?)i=1...n instantiated by the substitution θ = {X1 7→ t1 , Y1 7→ s1 , . . . , Xn 7→ tn , Yn 7→ sn }. Note
that C has attenuation factor t and threshold values ? at the body. Therefore, the
side conditions of the QDA step boil down to d P di (1 ≤ i ≤ n) which are true by
assumption. It remains to prove that each premise of the QDA step can be derived
from EQS in QCHL(D, C):
— EQS `D,C (t == c(tn ))]t ⇐ Π and EQS `D,C (s == c0 (sn ))]t ⇐ Π are trivial
consequences of t ≈Π c(tn ) and s ≈Π c0 (sn ), respectively. In both cases, the
QCHL(D,C) proofs consist of one single QEA step.
d

0
∈ EQS in
— EQS `D,C payd0 ]d0 ⇐ Π can be proved using the clause payd0 ←−
one single QDA step.
— EQS `D,C (ti ∼ si )]di ⇐ Π for i = 1 . . . n. For each i, we observe that ti ≈di ,Π
si holds because of t̂i = ti , ŝi = si which satisfy ti ≈Π t̂i , si ≈Π ŝi and
t̂i ≈di ŝi . Since t̂i = ti is a subterm of t̂ = c(tn ), the inductive hypothesis can
be applied.

[⇐=] Let T be a QCHL(D, C)-proof tree witnessing EQS `D,C (t ∼ s)]d ⇐ Π. We
prove t ≈d,Π s reasoning by induction on the number n = kT k of nodes in T that
represent conclusions of QDA inference steps. Note that all the program clauses
belonging to EQS define either the binary predicate symbol ‘∼’ or the nullary
predicates payλ .
Basis (n = 1).
In this case we have for the QDA inference step that there can be used three
possible EQS clauses:
t

1. The program clause is X ∼ Y ←
− (X == Y )]?. Then the QDA inference
step must be of the form:
(t == t0 )]d1 ⇐ Π

(s == s0 )]d2 ⇐ Π
(t ∼ s)]d ⇐ Π

(t0 == s0 )]e1 ⇐ Π

with d P d1 u d2 u e1 . The proof of the three premises must use the QEA
inference rule. Because of the conditions of this inference rule we have
t ≈Π t0 , s ≈Π s0 and t0 ≈Π s0 . Therefore t ≈Π s is clear. Then t ≈d,Π s
holds by taking t̂ = ŝ = t because, trivially, t ≈Π t̂, s ≈Π ŝ and t̂ ≈d ŝ.
t
2. The program clause is u ∼ u0 ←
− payλ ]? with u, u0 ∈ BC such that S(u, u0 ) =
λ 6= b. The QDA inference step must be of the form:
(t == u)]d1 ⇐ Π

(s == u0 )]d2 ⇐ Π
(t ∼ s)]d ⇐ Π

payλ ]e1 ⇐ Π

A Transformation-based Implementation for SQCLP (Preliminary Version) 19
with d P d1 u d2 u e1 . Due to the forms of the QEA inference rule and
λ
the EQS clause payλ ←
−, we can assume without loss of generality that
d1 = d2 = t and e1 = λ. Therefore d P λ. Moreover, the QCHL(D,C)
proofs of the first two premises must use QEA inferences. Consequently
we have t ≈Π u and s ≈Π u0 . These facts and u ≈d u0 imply t ≈d,Π s.
t

3. The program clause is c ∼ c0 ←
− payλ ]? with c, c0 ∈ DC 0 such that S(c, c0 ) =
λ 6= b. The QDA inference step must be of the form:
(t == c)]d1 ⇐ Π

(s == c0 )]d2 ⇐ Π
(t ∼ s)]d ⇐ Π

payλ ]e1 ⇐ Π

with d P d1 u d2 u e1 . Due to the forms of the QEA inference rule and
λ
the EQS clause payλ ←
−, we can assume without loss of generality that
d1 = d2 = t and e1 = λ. Therefore d P λ. Moreover, the QCHL(D,C)
proofs of the first two premises must use QEA inferences. Consequently
we have t ≈Π c and s ≈Π c0 . These facts and c ≈d c0 imply t ≈d,Π s.
Inductive step (n > 1).
In this case t and s must be of the form t = c(tn ) and s = c0 (sn ). The EQS
clause used in the QDA inference step at the root must be of the form:
t

c(X n ) ∼ c0 (Y n ) ←
− payd0 ]?, ((Xi ∼ Yi )]?)i=1...n
with S(c, c0 ) = d0 6= b. The inference step at the root will be:
payd0 ]e0 ⇐ Π
(t == c(tn ))]d1 ⇐ Π
( (ti ∼ si )]ei ⇐ Π )i=1...n
(s == c0 (sn ))]d2 ⇐ Π
(t ∼ s)]d ⇐ Π
dn
d0
with d P d1 u d2 u i=0 ei . Due to the forms of the EQS clause payd0 ←−
and
the QEA inference rule there is no loss of generality in assuming d1 = d2 = t
dn
and e0 = d0 , therefore we have d P d0 u i=1 ei . By the inductive hypothesis
ti ≈ei ,Π si (1 ≤ i ≤ n), i.e. there are constructor terms t̂i , ŝi such that ti ≈Π tˆi ,
si ≈Π ŝi and t̂i ≈ei ŝi for i = 1 . . . n. Thus, we can build t̂ = c(t̂1 , . . . , t̂n ) and
ŝ = c0 (ŝ1 , . . . , ŝn ) having t ≈d,Π s because:
• t ≈Π t̂, i.e. c(tn ) ≈Π c(t̂n ), by decomposition since ti ≈Π t̂i .
• s ≈Π ŝ, i.e. c0 (sn ) ≈Π c0 (ŝn ), again by decomposition since si ≈Π ŝi .
dn
dn
• t̂ ≈d ŝ, since d P d0 u i=1 ei P S(c, c0 ) u i=1 S(t̂i , ŝi ) = S(t̂, ŝ) .
We are now ready to define elimS acting over programs and goals.
Definition 4.2
Assume a SQCLP(S, D, C)-program P and a SQCLP(S, D, C)-goal G for P whose
atoms are all relevant for P. Then we define:
1. For each atom A, let A∼ be t ∼ s if A : t == s; otherwise let A∼ be A.
α
2. For each clause C : (p(tn ) ←
− B) ∈ P let CˆS be the set of QCLP(D, C) clauses
consisting of:

20

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az
α

— The clause Ĉ : (b
pC (tn ) ←
− B ∼ ), where pbC ∈ DP n is not affected by P
(chosen in a different way for each C) and B ∼ is obtained from B by
replacing each atom A occurring in B by A∼ .
t
− payλ ]?, ((Xi ∼ ti )]?)i=1...n , pbC (tn )]? for each p0 ∈
— A clause p0 (X n ) ←
DP n such that S(p, p0 ) = λ 6= b. Here, X n must be chosen as n pairwise
different variables not occurring in the clause C.
S
3. elimS (P) is the QCLP(D, C)-program EQS ∪ P̂S where P̂S =def C∈P CˆS .
4. elimS (G) is the QCLP(D, C)-goal G∼ obtained from G by replacing each atom
A occurring in G by A∼ .
The following example illustrates the transformation elimS .
Example 4.2 (Running example: QCLP(U ⊗W, R)-program elimS (Pr ))
Consider the SQCLP(Sr , U⊗W, R)-program Pr and the goal Gr for Pr as presented
in Example 4.1. The transformed QCLP(U⊗W, R)-program elimS (Pr ) is as follows:
(0.9,1)

R̂1
R1.1

f̂amousR1 (sha) ←−−−−
famous(X) ← payt , X∼sha, f̂amousR1 (sha)
(1,1)

R̂2

ŵroteR2 (sha, kle) ←−−−

R2.1

wrote(X, Y) ← payt , X∼sha, Y∼kle, ŵroteR2 (sha, kle)

R2.2

authored(X, Y) ← pay(0.9,0) , X∼sha, Y∼kle, ŵroteR2 (sha, kle)
(1,1)

R̂3

ŵroteR3 (sha, hamlet) ←−−−

R3.1

wrote(X, Y) ← payt , X∼sha, Y∼hamlet, ŵroteR3 (sha, hamlet)

R3.2

authored(X, Y) ← pay(0.9,0) , X∼sha, Y∼hamlet, ŵroteR3 (sha, hamlet)
(0.75,3)

R̂4
R4.1

ĝood workR4 (G) ←−−−−− famous(A)#(0.5,100), authored(A, G)
good work(X) ← payt , X∼G, ĝood workR4 (G)
% Program clauses for ∼:

% Program clauses for pay:

X ∼Y ← X==Y

payt ←

kle ∼ kli ← pay(0.8,2)

pay(0.9,0) ←−−−−

[. . .]

pay(0.8,2) ←−−−−

(0.9,0)

(0.8,2)

Finally, the goal elimS (Gr ) for elimS (Pr ) is as follows:
good work(X)#W 8 W Q? (0.5,10)

The next theorem proves the semantic correctness of the program transformation.
Theorem 4.1
Consider a SQCLP(S, D, C)-program P, an atom A relevant for P, a qualification
value d ∈ D \ {b} and a satisfiable finite set of C-constraints Π. Then, the following
two statements are equivalent:
1. P `S,D,C A]d ⇐ Π
2. elimS (P) `D,C A∼ ]d ⇐ Π
where A∼ is understood as in Definition 4.2(1).

A Transformation-based Implementation for SQCLP (Preliminary Version) 21
Proof
We separately prove each implication.
[1. ⇒ 2.] (the transformation is complete). Assume that T is a SQCHL(S, D, C)
proof tree witnessing P `S,D,C A]d ⇐ Π. We want to show the existence of a
QCHL(D, C) proof tree T 0 witnessing elimS (P) `D,C A∼ ]d ⇐ Π. We reason by
complete induction on kT k. There are three possible cases according to the syntactic
form of the atom A. In each case we argue how to build the desired proof tree T 0 .
— A is a primitive atom κ. In this case A∼ is also κ and T contains only one
SQPA inference node. Because of the inference rules SQPA and QPA, both
P `S,D,C κ]d ⇐ Π and elimS (P) `D,C κ]d ⇐ Π are equivalent to Π |=C κ, therefore
T 0 trivially contains just one QPA inference node.
— A is an equation t == s. In this case A∼ is t ∼ s and T contains just one SQEA
inference node. We know P `S,D,C (t == s)]d ⇐ Π is equivalent to t ≈d,Π s because
of the inference rule SQEA. From this equivalence follows EQS `D,C (t ∼ s)]d ⇐ Π
due to Lemma 4.1 and hence elimS (P) `D,C (t ∼ s)]d ⇐ Π by construction of
elimS (P). In this case, T 0 will be a proof tree rooted by a QDA inference step.
— A is a defined atom p0 (t0 n ) with p0 ∈ DP n. In this case A∼ is p0 (t0 n ) and the
root inference of T must be a SQDA inference step of the form:
( (t0i == ti θ)]di ⇐ Π )i=1...n ( Bj θ]ej ⇐ Π )j=1...m
(♣)
p0 (t0 n )]d ⇐ Π
α

with C : (p(tn ) ←
− B1 ]w1 , . . . , Bm ]wm ) ∈ P, θ substitution, S(p0 , p) = d0 6= b,
?
ej Q wj (1 ≤ j ≤ m), d P di (0 ≤ i ≤ n) and d P α ◦ ej (1 ≤ j ≤ m)—which
means d P α in the case m = 0. We can assume that the first n premises at (♣) are
proved in SQCLP(S, D, C) w.r.t. P by proof trees T1i (1 ≤ i ≤ n) satisfying kT1i k <
kT k (1 ≤ i ≤ n), and the last m premises at (♣) are proved in SQCLP(S, D, C)
w.r.t. P by proof trees T2j (1 ≤ j ≤ m) satisfying kT2j k < kT k (1 ≤ j ≤ m).
By Definition 4.2, we know that the transformed program elimS (P) contains two
clauses of the following form:
α

m
1
]wm
]w1 , . . . , B∼
− B∼
Ĉ : p̂C (tn ) ←
t

Ĉp0 : p0 (X n ) ←
− payd0 ]?, ( (Xi ∼ ti )]? )i=1...n , p̂C (tn )]?
j
where Xi (1 ≤ i ≤ n) are fresh variables not occurring in C and B∼
(1 ≤ j ≤ m)
is the result of replacing ‘∼’ for ‘==’ if Bj is equation; and Bj itself otherwise.
Given that the n variables Xi do not occur in C, we can assume that σ =def θ0 ] θ
with θ0 =def {X1 7→ t01 , . . . , Xn 7→ t0n } is a well-defined substitution. We claim
that elimS (P) `D,C A∼ ]d ⇐ Π can be proved with a proof tree T 0 rooted by the
QDA inference step (♠.1), which uses the clause Ĉp0 instantiated by σ and having
dn+1 = d.

( (t0i == Xi σ)]t ⇐ Π )i=1...n
payd0 σ]d0 ⇐ Π
( (Xi ∼ ti )σ]di ⇐ Π )i=1...n
p̂C (tn )σ]dn+1 ⇐ Π
p0 (t0 n )]d ⇐ Π

(♠.1)

( (t0i == Xi θ0 )]t ⇐ Π )i=1...n
payd0 ]d0 ⇐ Π
( (Xi θ0 ∼ ti θ)]di ⇐ Π )i=1...n
p̂C (tn θ)]dn+1 ⇐ Π
p0 (t0 n )]d ⇐ Π

(♠.2)

22

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

By construction of σ, (♠.1) can be rewritten as (♠.2), and in order to build the
rest of T 0, we show that each premise of (♠.2) admits a proof in QCHL(D, C) w.r.t.
the transformed program elimS (P):
• elimS (P) `D,C (t0i == Xi θ0 )]t ⇐ Π for i = 1 . . . n. Straightforward using a single
QEA inference step since Xi θ0 = t0i and t0i ≈Π t0i is trivially true.
d

0
∈ elimS (P)
• elimS (P) `D,C payd0 ]d0 ⇐ Π. Immediate using the clause (payd0 ←−)
with a single QDA inference step.
• elimS (P) `D,C (Xi θ0 ∼ ti θ)]di ⇐ Π for i = 1 . . . n. From the first n premises of (♣)
we know P `S,D,C (t0i == ti θ)]di ⇐ Π with a proof tree T1i satisfying kT1i k < kT k
for i = 1 . . . n. Therefore, for i = 1 . . . n, elimS (P) `D,C (t0i ∼ ti θ)]di ⇐ Π with some
0
QCHL(D,C) proof tree T1i
by inductive hypothesis. Since (Xi θ0 ∼ ti θ) = (t0i ∼ ti θ)
for i = 1 . . . n, we are done.
• elimS (P) `D,C p̂C (tn θ)]d ⇐ Π. This is proved by a QCHL(D, C) proof tree with a
QDA inference step node at its root of the following form:

j
θ]ej ⇐ Π )j=1...m
( (ti θ == ti θ)]di ⇐ Π )i=1...n ( B∼
(♥)
p̂C (tn θ)]d ⇐ Π

which uses the program clause Ĉ instantiated by the substitution θ. Once more, we
have to check that the premises can be derived in QCHL(D, C) from the transformed
program elimS (P) and that the side conditions of (♥) are satisfied:
— The first n premises can be trivially proved using QEA inference steps.
— The last m premises can be proved w.r.t. elimS (P) with some QCHL(D, C)
0
proof trees T2j
(1 ≤ j ≤ m) by the inductive hypothesis, since we have
premises ( Bj θ]ej ⇐ Π )j=1...m at (♣) that can be proved in SQCLP(S, D, C)
w.r.t. P with proof trees T2j of size kT2j k < kT k (1 ≤ j ≤ m).
— The side conditions—namely: ej Q? wj (1 ≤ j ≤ m), d P di (1 ≤ i ≤ n) and
d P α ◦ ej (1 ≤ j ≤ m)—trivially hold because they are also satisfied by (♣).

Finally, we complete the construction of T 0 by checking that (♠.2) satisfies the
side conditions of the inference rule QDA:

• All threshold values at the body of Ĉp0 are ‘?’, therefore the first group of side
conditions becomes di Q? ? (0 ≤ i ≤ n + 1), which are trivially true.
• The second side condition reduces to d P t, which is also trivially true.
• The third, and last, side condition is d P t ◦ di (0 ≤ i ≤ n + 1), or equivalently
d P di (0 ≤ i ≤ n + 1). In fact, d P di (0 ≤ i ≤ n) holds due to the side conditions
in (♣), and d P dn+1 holds because dn+1 = d by construction of (♠.1) and (♠.2).
[2. ⇒ 1.] (the transformation is sound). Assume that T 0 is a QCHL(D, C) proof
tree witnessing elimS (P) `D,C A∼ ]d ⇐ Π. We want to show the existence of a
SQCHL(S, D, C) proof tree T witnessing P `S,D,C A]d ⇐ Π. We reason by complete
induction of kT 0 k. There are three possible cases according to the syntactic form of
the atom A∼ . In each case we argue how to build the desired proof tree T .
— A∼ is a primitive atom κ. In this case A is also κ and T 0 contains only one QPA
inference node. Both elimS (P) `D,C κ]d ⇐ Π and P `S,D,C κ]d ⇐ Π are equivalent

A Transformation-based Implementation for SQCLP (Preliminary Version) 23
to Π |=C κ because of the inference rules QPA and SQPA, therefore T trivially
contains just one SQPA inference node.
— A∼ is of the form t ∼ s. In this case A is t == s and T 0 is rooted by a QDA
inference step. From elimS (P) `D,C (t ∼ s)]d ⇐ Π and by construction of elimS (P)
we have EQS `D,C (t ∼ s)]d ⇐ Π. By Lemma 4.1 we get t ≈d,Π s and, by the
definition of the SQEA inference step, we can build T as a proof tree with only
one SQEA inference node proving P `S,D,C (t == s)]d ⇐ Π.
— A∼ is a defined atom p0 (tn ) with p0 ∈ DP n and p0 6= ∼. In this case A = A∼
and the step at the root of T 0 must be a QDA inference step using a clause C 0 ∈
elimS (P) with head predicate p0 and a substitution θ. Because of Definition 4.2 and
α
the fact that p0 is relevant for P, there must be some clause C : (p(tn ) ←
− B) ∈ P
such that S(p, p0 ) = d0 6= b, and C 0 must be of the form:
t

C 0 : p0 (X n ) ←
− payd0 ]?, ((Xi ∼ ti )]?)i=1...n , p̂C (tn )]?
where the variables X n do not occur in C. Thus the QDA inference step at the
root of T 0 must be of the form:
( (t0i == Xi θ)]d1i ⇐ Π )i=1...n
payd0 θ]e10 ⇐ Π
( (Xi ∼ ti )θ]e1i ⇐ Π )i=1...n
p̂C (tn )θ]e1(n+1) ⇐ Π
p0 (t0 n )]d ⇐ Π

(♠)

and the proof of the last premise must use the only clause for p̂C introduced in
elimS (P) according to Definition 4.2, i.e.:
α

1
m
Ĉ : p̂C (tn ) ←
− B∼
]w1 , . . . , B∼
]wm .

Therefore, the proof of this premise must be of the form:
j 0
θ ]e2j ⇐ Π )j=1...m
( (ti θ == ti θ0 )]d2i ⇐ Π )i=1...n ( B∼
(♥)
p̂C (tn )θ]e1(n+1) ⇐ Π

for some substitution θ0 not affecting X n . We can assume that the last m premises in
(♥) are proved in QCHL(D, C) w.r.t. elimS (P) by proof trees Tj0 satisfying kTj0 k <
kT 0 k (1 ≤ j ≤ m). Then we use the substitution θ0 and clause C to build a
SQCHL(S, D, C) proof tree T with a SQDA inference step at the root of the form:
( (t0i == ti θ0 )]e1i ⇐ Π )i=1...n ( Bj θ0 ]e2j ⇐ Π )j=1...m
(♣)
p0 (t0 n )]d ⇐ Π
Next we check that the premises of this inference step admit proofs in SQCHL(S, D,
C) and that (♣) satisfies the side conditions of a valid SQDA inference step.
• P `S,D,C (t0i == ti θ0 )]e1i ⇐ Π for i = 1 . . . n.
— From the premises ((Xi ∼ ti )θ]e1i ⇐ Π)i=1...n of (♠) and by construction of
elimS (P) we know EQS `D,C (Xi ∼ ti )θ]e1i ⇐ Π (1 ≤ i ≤ n). Therefore by
Lemma 4.1 we have Xi θ ≈e1i ,Π ti θ for i = 1 . . . n.
— Consider now the premises ((t0i == Xi θ)]d1i ⇐ Π)i=1...n of (♠). Their proofs

24

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

must rely on QEA inference steps, and therefore t0i ≈Π Xi θ holds for i =
1 . . . n.
— Analogously, from the proofs of the premises ((ti θ == ti θ0 )]d2i ⇐ Π)i=1...n
we have ti θ ≈Π ti θ0 (or equivalently ti θ0 ≈Π ti θ) for i = 1 . . . n.

•

•
•
•
•

From the previous points we have Xi θ ≈e1i ,Π ti θ, t0i ≈Π Xi θ and ti θ0 ≈Π ti θ,
which by Lemma 2.7(1) of (Rodrı́guez-Artalejo and Romero-Dı́az 2010b) imply
t0i ≈e1i ,Π ti θ0 (1 ≤ i ≤ n). Therefore the premises ((t0i == ti θ0 )]e1i ⇐ Π)i=1...n can
be proven in SQCHL(S, D, C) using a SQEA inference step.
j 0
P `S,D,C Bj θ0 ]e2j ⇐ Π for j = 1 . . . m. We know elimS (P) `D,C B∼
θ ]e2j ⇐ Π with
0
0
0
a proof tree Tj satisfying kTj k < kT k (1 ≤ j ≤ m) because of (♥). Therefore we
have, by inductive hypothesis, P `S,D,C Bj θ0 ]e2j ⇐ Π for some SQCHL(S, D, C)
proof tree Tj (1 ≤ j ≤ m).
S(p, p0 ) = d0 6= b. As seen above.
e2j Q? wj for j = 1 . . . m. This is a side condition of the QDA step in (♥).
d P e1i for i = 1 . . . n. Straightforward from the side conditions of (♠), which
include d P t ◦ e1i for (0 ≤ i ≤ n + 1).
d P α◦e2j for j = 1 . . . m. This follows from the side conditions of (♠) and (♥), since
we have d P t◦e1i for i = 0 . . . n+1 (in particular d P e1(n+1) ) and e1(n+1) P α◦e2j
for j = 1 . . . m.
Finally, the next theorem extends the previous result to goals.
Theorem 4.2
Let G be a goal for a SQCLP(S, D, C)-program P whose atoms are all relevant for
P. Assume P 0 = elimS (P) and G0 = elimS (G). Then, SolP (G) = SolP 0 (G0 ).
Proof
According to the definition of goals in Section 2, and Definition 4.2, G and G0 must
be of the form (Ai ]Wi , Wi Q? βi )i=1...m and (Ai∼ ]Wi , Wi Q? βi )i=1...m , respectively.
By Definitions 2.2 and 3.1, both SolP (G) and SolP 0 (G0 ) are sets of triples hσ, µ, Πi
where σ is a C-substitution, µ : war(G) → DD \ {b} (note that war(G) = war(G0 ))
and Π is a satisfiable finite set of C-constraints. Moreover:

1. hσ, µ, Πi ∈ SolP (G) iff Wi µ = di Q? βi and P `S,D,C Ai σ]Wi µ ⇐ Π (1 ≤ i ≤ m).
2. hσ, µ, Πi ∈ SolP 0 (G0 ) iff Wi µ = di Q? βi and P 0 `D,C Ai∼ σ]Wi µ ⇐ Π (1 ≤ i ≤ m).
Because of Theorem 4.1, conditions (1) and (2) are equivalent.
4.2 Transforming QCLP into CLP
The results presented in this subsection are dependant on the assumption that the
qualification domain D is existentially expressible in the constraint domain C via
an injective mapping ı : DD \ {b} → CC and two existential C-constraints of the
following form:
qVal(X) = ∃U1 . . . ∃Uk (B1 ∧ . . . ∧ Bm )
qBound(X, Y, Z) = ∃V1 . . . ∃Vl (C1 ∧ . . . ∧ Cq )

A Transformation-based Implementation for SQCLP (Preliminary Version) 25
Our aim is to present semantically correct transformations from QCLP(D, C)
into CLP(C), working both for programs and goals. In order to compute with the
encodings of D values in C, we will use the CLP(C)-program ED consisting of the
following two clauses:
qVal(X) ← B1 , . . . , Bm
qBound(X, Y, Z) ← C1 , . . . , Cq
where qVal ∈ DP 1 and qBound ∈ DP 3 do not occur in the QCLP(D, C) programs
and goals to be transformed.
The lemma stated below is an immediate consequence of Lemma 3.1 and Definition 2.1.
Lemma 4.2
For any satisfiable finite set Π of C-constraints one has:
1. For any ground term t ∈ CC :
t ∈ ran(ı) ⇐⇒ qVal(t) true in C ⇐⇒ ED `C qVal(t) ⇐ Π
2. For any ground terms r = ı(x), s = ı(y), t = ı(z) with x, y, z ∈ DD \ {b}:
x P y ◦ z ⇐⇒ qBound(r, s, t) true in C ⇐⇒ ED `C qBound(r, s, t) ⇐ Π
The two items above are also valid if ED is replaced by any CLP(C)-program
including the two clauses in ED and having no additional occurrences of qVal and
qBound at the head of clauses.
Now we are ready to define the transformations from QCLP(D, C) into CLP(C).
Definition 4.3
Assume that D is existentially expressible in C, and let qVal(X), qBound(X, Y, Z)
and ED be as explained above. Assume also a QCLP(D, C)-program P and a
QCLP(D, C)-goal G for P without occurrences of the defined predicate symbols
qVal and qBound. Then:
1. P is transformed into the CLP(C)-program elimD (P) consisting of the two
clauses in ED and the transformed C T of each clause C ∈ P, built as specified
in Figure 5. The transformation rules of this figure assume a different choice
of p0 ∈ DP n+1 for each p ∈ DP n.
2. G is transformed into the CLP(C)-goal elimD (G) built as specified in Figure
5. Note that the qualification variables Wn occurring in G become normal
CLP variables in the transformed goal.
The following example illustrates the transformation elimD .
Example 4.3 (Running example: CLP(R)-program elimD (elimS (Pr )))
Consider the QCLP(U⊗W, R)-program elimS (Pr ) and the goal elimS (Gr ) for the
same program as presented in Example 4.2. The transformed CLP(R)-program
elimD (elimS (Pr )) is as follows:

26

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

Transforming Atoms
TEA

(t == s)T = (t == s, ı(t)).

TPA

(κ)T = (κ, ı(t)) with κ primitive atom.

TDA

(p(tn ))T = (p0 (tn , W ), W ) with p ∈ DP n and W a fresh CLP variable.

Transforming qc-Atoms
TQCA

AT = (A0 , w)
(A]d ⇐ Π)T = (A0 ⇐ Π, {qVal(w), qBound(ı(d), ı(t), w)})

Transforming Program Clauses
TPC
CT

( BjT = (Bj0 , wj0 ) )j=1...m


qVal(wj0 ), pwj0 Q? ı(wj )q,
= p0 (tn , W ) ← qVal(W ),
qBound(W, ı(α), wj0 ), Bj0 j=1...m
α

where C : p(tn ) ←
− B1 ]w1 , . . . , Bm ]wm , W is a fresh CLP variable and
pwj0 Q? ı(wj )q is omitted if wj = ?, i.o.c. abbreviates qBound(ı(wj ), ı(t), wj0 ).
Transforming Goals
TG


elimD (G) =

( BjT = (Bj0 , wj0 ) )j=1...m

qVal(Wj ), pWj Q? ı(βj )q,
qVal(wj0 ), qBound(Wj , ı(t), wj0 ), Bj0 j=1...m

where G : (Bj ]Wj , Wj Q? βj )j=1...m and pWj Q? ı(βi )q as in TPC above.

Fig. 5. Transformation rules

R̂1
R1.1

f̂amousR1 (sha, W) ← qVal(W), qBound(W, t, (0.9,1))
famous(X, W) ← qVal(W), qVal(W1 ), qBound(W, t, W1 ), payt (W1 ),
qVal(W2 ), qBound(W, t, W2 ), ∼(X, sha, W2 ),
qVal(W3 ), qBound(W, t, W3 ), f̂amousR1 (sha, W3 )

R̂2
R2.1

ŵroteR2 (sha, kle, W) ← qVal(W), qBound(W, t, (1,1))
wrote(X, Y, W) ← qVal(W), qVal(W1 ), qBound(W, t, W1 ), payt (W1 ),
qVal(W2 ), qBound(W, t, W2 ), ∼(X, sha, W2 ),
qVal(W3 ), qBound(W, t, W3 ), ∼(Y, kle, W3 ),
qVal(W4 ), qBound(W, t, W4 ), ŵroteR2 (sha, kle, W4 )

R2.2

authored(X, Y, W) ← qVal(W), qVal(W1 ), qBound(W, t, W1 ), pay(0.9,0) (W1 ),
qVal(W2 ), qBound(W, t, W2 ), ∼(X, sha, W2 ),
qVal(W3 ), qBound(W, t, W3 ), ∼(Y, kle, W3 ),
qVal(W4 ), qBound(W, t, W4 ), ŵroteR2 (sha, kle, W4 )

R̂3
R3.1

ŵroteR3 (sha, hamlet, W) ← qVal(W), qBound(W, t, (1,1))
wrote(X, Y, W) ← qVal(W), qVal(W1 ), qBound(W, t, W1 ), payt (W1 ),
qVal(W2 ), qBound(W, t, W2 ), ∼(X, sha, W2 ),
qVal(W3 ), qBound(W, t, W3 ), ∼(Y, hamlet, W3 ),
qVal(W4 ), qBound(W, t, W4 ), ŵroteR3 (sha, hamlet, W4 )

A Transformation-based Implementation for SQCLP (Preliminary Version) 27
R3.2

authored(X, Y, W) ← qVal(W), qVal(W1 ), qBound(W, t, W1 ), pay(0.9,0) (W1 ),
qVal(W2 ), qBound(W, t, W2 ), ∼(X, sha, W2 ),
qVal(W3 ), qBound(W, t, W3 ), ∼(Y, hamlet, W3 ),
qVal(W4 ), qBound(W, t, W4 ), ŵroteR3 (sha, hamlet, W4 )

R̂4

ĝood workR4 (X, W) ← qVal(W),
qVal(W1 ), qBound((0.5,100), t, W1 ), qBound(W, (0.75,3), W1 ), famous(Y, W1 ),
qVal(W2 ), qBound(W, (0.75,3), W2 ), authored(Y, X, W2 )

R4.1

good work(G, W) ← qVal(W), qVal(W1 ), qBound(W, t, W1 ), payt (W1 ),
qVal(W2 ), qBound(W, t, W2 ), ∼(G, X, W2 ),
qVal(W3 ), qBound(W, t, W3 ), ĝood workR4 (X, W3 )
% Program clauses for ∼:
∼(X, Y, W) ← qVal(W), qVal(t), qBound(W, t, t), X==Y
∼(kle, kli, W) ← qVal(W), qVal(W1 ), qBound(W, t, W1 ), pay(0.8,2) (W1 )
[. . .]
% Program clauses for pay:
payt (W) ← qVal(W), qBound(W, t, t)
pay(0.9,0) (W) ← qVal(W), qBound(W, t, (0.9,0))
pay(0.8,2) (W) ← qVal(W), qBound(W, t, (0.8,2))
% Program clauses for qVal & qBound:
qVal((X1 ,X2 )) ← X1 > 0, X1 ≤ 1, X2 ≥ 0
qBound((W1 ,W2 ), (Y1 ,Y2 ), (Z1 ,Z2 )) ← W1 ≤ Y1 × Z1 , W2 ≥ Y2 + Z2

Finally, the goal elimD (elimS (Gr )) for elimD (elimS (Pr )) is as follows:
qVal(W), qBound((0.5,10), t, W), qVal(W’), qBound(W, t, W’), good work(X, W’)

Note that, in order to improve the clarity of the program clauses of this example,
the qualification value (1,0)—top value in U⊗W—has been replaced by t.
The next theorem proves the semantic correctness of the program transformation.
Theorem 4.3
Let A be an atom such that qVal and qBound do not occur in A. Assume d ∈ D\{b}
such that (A]d ⇐ Π)T = (A0 ⇐ Π, Ω). Then, the two following statements are
equivalent:
1. P `D,C A]d ⇐ Π
2. elimD (P) `C A0ρ ⇐ Π for some ρ ∈ SolC (Ω) such that dom(ρ) = var(Ω).
Proof
We separately prove each implication.
[1. ⇒ 2.] (the transformation is complete). We assume that T is a QCHL(D, C)
proof tree witnessing P `D,C A]d ⇐ Π. We want to show the existence of a CLP(C)
proof tree T 0 witnessing elimD (P) `C A0ρ ⇐ Π for some ρ ∈ SolC (Ω) such that
dom(ρ) = var(Ω). We reason by complete induction on kT k. There are three possible

28

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

cases, according to the the syntactic form of the atom A. In each case we argue
how to build the desired proof tree T 0.
— A is a primitive atom κ. In this case TQCA and TPA compute A0 = κ and
Ω = {qVal(ı(t)), qBound(ı(d), ı(t), ı(t))}. Now, from P `D,C κ]d ⇐ Π follows
Π |=C κ due to the QPA inference, and therefore taking ρ = ε we can prove
elimD (P) `C κε ⇐ Π with a proof tree T 0 containing only one PA node. Moreover, ε ∈ SolC (Ω) is trivially true because the two constraints belonging to Ω are
obviously true in C.
— A is an equation t == s. In this case TQCA and TEA compute A0 = (t == s)
and Ω = {qVal(ı(t)), qBound(ı(d), ı(t), ı(t))}. Now, from P `D,C (t == s)]d ⇐ Π
follows t ≈Π s due to the QEA inference, and therefore taking ρ = ε we can prove
elimD (P) `C (t == s)ε ⇐ Π with a proof tree T 0 containing only one EA node.
Moreover, ε ∈ SolC (Ω) is trivially true because the two constraints belonging to Ω
are obviously true in C.
— A is a defined atom p(t0 n ) with p ∈ DP n . In this case TQCA and TDA compute
A0 = p0 (t0 n , W ) and Ω = {qVal(W ), qBound(ı(d), ı(t), W )} where W is a fresh CLP
variable. On the other hand, T must be rooted by a QDA step of the form:
( (t0i == ti θ)]di ⇐ Π )i=1...n ( Bj θ]ej ⇐ Π )j=1...m
p(t0 n )]d ⇐ Π

(♣)

α

− B1 ]w1 , . . . , Bm ]wm ) ∈ P instantiated by a substitution
using a clause C : (p(tn ) ←
θ and such that the side conditions ej Q? wj (1 ≤ j ≤ m), d P di (1 ≤ i ≤ n) and
d P α ◦ ej (1 ≤ j ≤ m) are fulfilled.
For j = 1 . . . m we can assume BjT = (Bj0 , wj0 ) and thus (Bj θ]ej ⇐ Π)T = (Bj0 θ ⇐
Π, Ωj ) where Ωj = {qVal(wj0 ), qBound(ı(ej ), ı(t), wj0 )}. The proof trees Tj of the
last m premises of (♣) will have less than kT k nodes, and hence the induction
hypothesis can be applied to each (Bj θ]ej ⇐ Π) with 1 ≤ j ≤ m, obtaining
CHL(C) proof trees Tj0 proving elimD (P) `C Bj0 θρj ⇐ Π for some ρj ∈ SolC (Ωj )
with dom(ρj ) = var(Ωj ).
Consider ρ = {W 7→ ı(d)} and C T ∈ elimD (P) of the form:


qVal(wj0 ), pwj0 Q? ı(wj )q,
C T : p0 (tn , W 0 ) ← qVal(W 0 ),
qBound(W 0 , ı(α), wj0 ), Bj0 j=1...m.
Obviously, ρ ∈ SolC (Ω) and dom(ρ) = var(Ω). To finish the proof we must prove
elimD (P) `C A0ρ ⇐ Π. We claim that this can be done with a CHL(C) proof tree
T 0 whose root inference is a DA step of the form:






( (t0i ρ == ti θ0 ) ⇐ Π )i=1...n
(W ρ == W 0 θ0 ) ⇐ Π
qVal(W 0 )θ0 ⇐ Π
qVal(wj0 )θ0 ⇐ Π
pwj0 Q? ı(wj )qθ0 ⇐ Π
qBound(W 0 , ı(α), wj0 )θ0 ⇐ Π
Bj0 θ0 ⇐ Π
p0 (t0 n , W )ρ ⇐ Π





j=1...m

(♠)

A Transformation-based Implementation for SQCLP (Preliminary Version) 29
using C T instantiated by the substitution θ0 = θ ] ρ1 ] · · · ] ρm ] {W 0 7→ ı(d)}. We
check that the premises of (♠) can be derived from elimD (P) in CHL(C):
• elimD (P) `C (t0i ρ == ti θ0 ) ⇐ Π for i = 1 . . . n. By construction of ρ and θ0, these
are equivalent to prove elimD (P) `C (t0i == ti θ) ⇐ Π for i = 1 . . . n and these hold
with CHL(C) proof trees of only one EA node because of t0i ≈Π ti θ, which is a
consequence of the first n premises of (♣).
• elimD (P) `C (W ρ == W 0 θ0 ) ⇐ Π. By construction of ρ and θ0, this is equivalent to
prove elimD (P) `C (ı(d) == ı(d)) ⇐ Π which results trivial.
• elimD (P) `C qVal(W 0 )θ0 ⇐ Π. By construction of θ0 , this is equivalent to prove
elimD (P) `C qVal(ı(d)) ⇐ Π. We trivially have that ı(d) ∈ ran(ı). Then, by Lemma
4.2, this premise holds.
• elimD (P) `C qVal(wj0 )θ0 ⇐ Π for j = 1 . . . m. By construction of θ0 and Lemma 4.2
we must prove, for any fixed j, that qVal(wj0 ρj ) is true in C. As ρj ∈ SolC (Ωj ) we
know ρj ∈ SolC (qVal(wj0 )), therefore qVal(wj0 ρj ) is trivially true in C.
• elimD (P) `C pwj0 Q? ı(wj )qθ0 ⇐ Π for j = 1 . . . m. We reason for any fixed j.
If wj = ? this results trivial. Otherwise, it amounts to qBound(ı(wj ), ı(t), wj0 ρj )
being true in C, by construction of θ0 and Lemma 4.2. As seen before, qVal(wj0 ρj )
is true in C, therefore wj0 ρj = ı(e0j ) for some e0j ∈ D \ {b}. From the side conditions
of (♣) we have wj P ej . On the other hand, ρj ∈ SolC (Ωj ) and, in particular,
ρj ∈ SolC (qBound(ı(ej ), ı(t), wj0 )). This, together with wj0 ρj = ı(e0j ), means ej P e0j ,
which with wj P ej implies wj P e0j , i.e. qBound(ı(wj ), ı(t), wj0 ρj ) is true in C.
• elimD (P) `C qBound(W 0 , ı(α), wj0 )θ0 ⇐ Π for j = 1 . . . m. We reason for any fixed j.
By construction of θ0 and Lemma 4.2, we must prove that qBound(ı(d), ı(α), wj0 ρj )
is true in C. As seen before, qVal(wj0 ρj ) is true in C, therefore wj0 ρj = ı(e0j ) for some
e0j ∈ D \{b}. From the side conditions of (♣) we have d P α◦ej . On the other hand,
ρj ∈ SolC (Ωj ) and, in particular, ρj ∈ SolC (qBound(ı(ej ), ı(t), wj0 )). This, together
with wj0 ρj = ı(e0j ), means ej P e0j . Now, d P α ◦ ej and ej P e0j implies d P α ◦ e0j ,
i.e. qBound(ı(d), ı(α), wj0 ρj ) is true in C.
• elimD (P) `C Bj0 θ0 ⇐ Π for j = 1 . . . m. In this case, it is easy to see that Bj0 θ0 =
Bj0 θρj by construction of θ0 and because of the program transformation rules. On
the other hand, proof trees Tj0 proving elimD (P) `C Bj0 θρj ⇐ Π can be obtained by
inductive hypothesis as seen before.
[2. ⇒ 1.] (the transformation is sound). We assume that T 0 is a a CHL(C) proof
tree witnessing elimD (P) `C A0 ρ ⇐ Π for some ρ ∈ SolC (Ω) such that dom(ρ) =
var(Ω). We want to to show the existence of a QCHL(D, C) proof tree T witnessing
P `D,C A]d ⇐ Π. We reason by complete induction on kT 0 k. There are three possible
cases according to the the syntactic form of the atom A0. In each case we argue how
to build the desired proof tree T .
— A0 is a primitive atom κ. In this case due to TQCA and TPA we can assume
A = κ and Ω = {qVal(ı(t)), qBound(ı(d), ı(t), ı(t))}. Note that dom(ρ) = var(Ω) =
∅ implies ρ = ε. Now, from elimD (P) `C κε ⇐ Π follows Π |=C κ due to the
PA inference, and therefore we can prove P `D,C κ]d ⇐ Π with a proof tree T
containing only one QPA node.
— A0 is an equation t == s. In this case due to TQCA and TEA we can assume

30

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

A = (t == s) and Ω = {qVal(ı(t)), qBound(ı(d), ı(t), ı(t))}. Note that dom(ρ) =
var(Ω) = ∅ implies ρ = ε. Now, from elimD (P) `C (t == s)ε ⇐ Π follows t ≈Π s
due to the EA inference, and therefore we can prove P `D,C (t == s)]d ⇐ Π with
a proof tree T containing only one QEA node.
— A0 is a defined atom p0 (t0 n , W ) with p0 ∈ DP n+1 . In this case due to TQCA
and TDA we can assume A = p(t0 n ) and Ω = {qVal(W ), qBound(ı(d), ı(t), W )}.
On the other hand, T 0 must be rooted by a DA step (♠) using a clause C T ∈
elimD (P) instantiated by a substitution θ0 . We can assume that (♠), C T and the
corresponding clause C ∈ P have the form already displayed in [1. ⇒ 2.].
By construction of C T , we can assume BjT = (Bj0 , wj0 ). Let θ = θ0 var(C) and
ρj = θ0 var(wj0 ) (1 ≥ j ≥ m). Then, due to the premises qVal(wj0 )θ0 ⇐ Π of (♠)
and Lemma 4.2 we can assume e0j ∈ D \ {b} (1 ≤ j ≤ m) such that wj0 ρj = ı(e0j ).
To finish the proof, we must prove P `D,C A]d ⇐ Π. We claim that this can
be done with a QCHL(D, C) proof tree T whose root inference is a QDA step of
the form of (♣), as displayed in [1. ⇒ 2.], using clause C instantiated by θ. In the
premises of this inference we choose di = t (1 ≤ i ≤ n) and ej = e0j (1 ≤ j ≤ m).
Next we check that these premises can be derived from P in QCHL(D, C) and that
the side conditions are fulfilled:
• P `D,C (t0i == ti θ)]di ⇐ Π for i = 1 . . . n. This amounts to t0i ≈Π ti θ which follows
from the first n premises of (♠) given that t0i ρ = t0i and ti θ0 = ti θ.
• P `D,C Bj θ]ej ⇐ Π for j = 1 . . . m. From BjT = (Bj0 , wj0 ) and due to rule TQCA, we
have ((Bj θ)]ej ⇐ Π)T = (Bj θ ⇐ Π, Ωj ) where Ωj = {qVal(wj0 ), qBound(ı(ej ), ı(t),
wj0 )}. From the premises of (♠) and the fact that Bj0 θ0 = Bj0 θρj we know that
elimD (P) `C Bj0 θρj ⇐ Π with a CHL(C) proof tree Tj0 such that kTj0 k < kT 0 k.
Therefore P `D,C Bj θ]ej ⇐ Π follows by inductive hypothesis provided that ρj ∈
SolC (Ωj ). In fact, due to the form of Ωj , ρj ∈ SolC (Ωj ) holds iff wj0 ρj = ı(e0j ) for
some e0j such that ej P e0j , which is the case because of the choice of ej .
• ej Q? wj for j = 1 . . . m. Trivial in the case that wj = ?. Otherwise they are
equivalent to wj P e0j which follow from premises pwj0 Q? ı(wj )qθ0 ⇐ Π (i.e.
pwj0 ρj Q? ı(wj )q ⇐ Π) of (♠) and Lemma 4.2.
• d P di for i = 1 . . . n. Trivially hold due to the choice of di = t.
• d P α◦ej for j = 1 . . . m. Note that ρ ∈ SolC (Ω) implies the existence of d0 ∈ D \{b}
such that ı(d0 ) = W ρ and d P d0 . On the other hand, ej = e0j by choice. It
suffices to prove d0 P α ◦ e0j for j = 1 . . . m. Premises of (♠) and Lemma 4.2
imply that qBound(W 0 θ0 , ı(α), wj0 θ0 ) is true in C. Moreover, W 0 θ0 = W ρ = ı(d0 )
because of another premise of (♠) and wj0 θ0 = ı(e0j ) as explained above. Therefore qBound(W 0 θ0 , ı(α), wj0 θ0 ) amounts to qBound(ı(d0 ), ı(α), ı(e0j )) which guarantees d0 P α ◦ e0j (1 ≤ j ≤ m).
The goal transformation correctness is established by the next theorem, which
will rely on the previous result:
Theorem 4.4
Let G be a goal for a QCLP(D, C)-program P such that qVal and qBound do not
occur in G. Let P 0 = elimD (P) and G0 = elimD (G). Assume a C-subtitution σ,

A Transformation-based Implementation for SQCLP (Preliminary Version) 31
a mapping µ : war(G) → DD \ {b} and a satisfiable finite set of C-constraints Π.
Then, the following two statements are equivalent:
1. hσ, µ, Πi ∈ SolP (G).
2. hθ, Πi ∈ SolP 0 (G0 ) for some θ that verifies the following requirements:
(a) θ =var(G) σ,
(b) θ =war(G) µı and
(c) W θ ∈ ran(ı) for each W ∈ var(G0 ) \ (var(G) ∪ war(G)).
Proof
As explained in Subsection 3.1 the syntax of goals in QCLP(D, C)-programs is the
same as that of goals for SQCLP(S, D, C)-programs, which is described in Section
2. Therefore G, and G0 due to rule TG, must have the following form:
G : ( Bj ]Wj , Wj Q? βj )j=1...m
G0 : ( qVal(Wj ), pWj Q? ı(βj )q, qVal(wj0 ), qBound(Wj , ı(t), wj0 ), Bj0 )j=1...m

with BjT = (Bj0 , wj0 ) (1 ≤ j ≤ m). Note that, because of rule TQCA, we have
(Bj σ]Wj µ ⇐ Π)T = (Bj0 σ ⇐ Π, Ωj ) with Ωj = {qVal(wj0 ), qBound(ı(Wj µ), ı(t),
wj0 )} for j = 1 . . . m. We now prove each implication.
[1. ⇒ 2.] Let hσ, µ, Πi ∈ SolP (G). This means, by Definition 3.1, Wj µ Q? βj and
P `D,C Bj σ]Wj µ ⇐ Π for j = 1 . . . m. In these conditions, Theorem 4.3 guarantees
P 0 `C Bj0 σρj ⇐ Π (1 ≤ j ≤ m) for some ρj ∈ SolC (Ωj ) such that dom(ρj ) = var(Ωj ).
It is easy to see that var(G0 )\(var(G)∪war(G)) = var(Ω1 )]· · ·]var(Ωm ). Therefore
it is possible to define a substitution θ verifying θ =var(G) σ, θ =war(G) µı and
θ =dom(ρj ) ρj (1 ≤ j ≤ m). Trivially, θ satisfies conditions 2.(a) and 2.(b). It also
satisfies condition 2.(c) because for any j and any variable X such that X ∈ var(Ωj ),
we have a constraint qVal(X) ∈ Ωj implying, due to Lemma 4.2, Xρj ∈ ran(ı)
(because ρj ∈ SolC (Ωj )).
In order to prove hθ, Πi ∈ SolP 0 (G0 ) in the sense of Definition 3.2 we check the
following items:
• By construction, θ is a C-substitution.
• By the theorem’s assumptions, Π is a satisfiable and finite set of C-constraints.
• P 0 `C Aθ ⇐ Π for every atom A in G0 . Because of the form of G0 we have to prove
the following for any fixed j:
— P 0 `C qVal(Wj )θ ⇐ Π. By construction of θ and Lemma 4.2, this amounts to
qVal(ı(Wj µ)) being true in C, which is trivial consequence of Wj µ ∈ D \ {b}.
— P 0 `C pWj Q? ı(βj )qθ ⇐ Π. If βj = ? this becomes trivial. Otherwise,
Wj θ = ı(Wj µ) by construction of θ, and by Lemma 4.2 it suffices to prove
qBound(ı(βj ), ı(t), ı(Wj µ)) is true in C. This follows from Wj µ Q? βj , that is
ensured by hσ, µ, Πi ∈ SolP (G).
— P 0 `C qVal(wj0 )θ ⇐ Π. By construction of θ and Lemma 4.2, this amounts to
qVal(wj0 ρj ) being true in C, that is guaranteed by ρj ∈ SolC (Ωj ).
— P 0 `C qBound(Wj , ı(t), wj0 )θ ⇐ Π. By construction of θ and Lemma 4.2, this
amounts to qBound(ı(Wj µ), ı(t), wj0 ρj ) being true in C, that is also guaranteed
by ρj ∈ SolC (Ωj ).

32

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

— P 0 `C Bj0 θ ⇐ Π. Note that, by construction of θ, Bj0 θ = Bj0 σρj . On the other
hand, ρj has been chosen above to verify P 0 `C Bj0 σρj ⇐ Π.
[2. ⇒ 1.] Let hθ, Πi ∈ SolP 0 (G0 ) and assume that θ verifies 2.(a), 2.(b) and 2.(c). In
order to prove hσ, µ, Πi ∈ SolP (G) in the sense of Definition 3.1 we must prove the
following items:
• By the theorem’s assumptions, σ is a C-substitution, µ : war(G) → DD \ {b} and
Π is a satisfiable finite set of C-constraints.
• Wj µ Q? βj . We reason for any fixed j. If βj = ? this results trivial. Otherwise, we
have P 0 `C pWj Q? ı(βj )qθ ⇐ Π which, by condition 2.(b) and Lemma 4.2 amounts
to qBound(ı(βj ), ı(t), ı(Wj µ)) is true C, i.e. Wj µ Q βj .
• P `D,C Bj σ]Wj µ ⇐ Π for j = 1 . . . m. We reason for any fixed j. Let ρj be the
restriction of θ to var(Ωj ). Then, P 0 `C Bj0 σρj ⇐ Π follows from hθ, Πi ∈ SolP 0 (G0 )
and Bj0 θ = Bj0 σρj . Therefore, P `D,C Bj σ]Wj µ ⇐ Π follows from Theorem 5.3
provided that ρj ∈ SolC (Ωj ). By Lemma 4.2 and the form of Ωj , ρj ∈ SolC (Ωj )
holds iff P 0 `C qVal(wj0 ρj ) ⇐ Π and P 0 `C qBound(ı(Wj µ), ı(t), wj0 ρj ) ⇐ Π, which
is true because hθ, Πi ∈ SolP 0 (G0 ) and construction of ρj .
4.3 Solving SQCLP Goals
In this subsection we show that the transformations from the two previous subsections can be used to define abstract goal solving systems for SQCLP and arguing about their correctness. In the sequel we consider a given SQCLP(S, D, C)program P and a goal G for P whose atoms are all relevant for P. We also consider
P 0 = elimS (P), G0 = elimS (G), P 00 = elimD (P 0 ) and G00 = elimD (G0 ). Due to the
definition of both elimS and elimD , we can assume:
G : ( Ai ]Wi , Wi Q? βi )i=1...m
G0 : ( Ai∼ ]Wi , Wi Q? βi )i=1...m
G00 : ( qVal(Wi ), pWi Q? ı(βi )q, qVal(wi0 ), qBound(Wi , ı(t), wi0 ), A0i )i=1...m
where ATi = (A0i , wi0 ).
We start by presenting an auxiliary result.
Lemma 4.3
Assume P, G, P 0, G0, P 00 and G00 as above. Let hσ 0 , Πi ∈ SolP 00 (G00 ), ν ∈ SolC (Π)
and θ = σ 0 ν. Then hθ, Πi ∈ SolP 00 (G00 ). Moreover, W θ ∈ ran(ı) for every W ∈
var(G00 ) \ var(G).1
Proof
Consider an arbitrary atom A00 occurring in G00. Because of hσ 0 , Πi ∈ SolP 00 (G00 ) we
have P `C A00 σ 0 ⇐ Π. On the other hand, because of ν ∈ SolC (Π) we have ∅ |=C Πν
and therefore also Π |=C Πν. This and Definition 3.1(4) of (Rodrı́guez-Artalejo and
Romero-Dı́az 2010b) ensure A00 σ 0 ⇐ Π <C A00 σ 0 ν ⇐ Π, i.e. A00 σ 0 ⇐ Π <C A00 θ ⇐ Π.
1

Note that war(G) ⊆ var(G00 ) \ var(G).

A Transformation-based Implementation for SQCLP (Preliminary Version) 33
This fact, P 00 `C A00 σ 0 ⇐ Π and the Entailment Property for Programs in CLP(C)
imply P 00 `C A00 θ ⇐ Π. Therefore, hθ, Πi ∈ SolP 00 (G00 ).
Consider now any W ∈ var(G00 ) \ var(G). By construction of G00, one of the
atoms occurring in G00 is qVal(W ). Then, due to hσ 0 Πi ∈ SolP 00 (G00 ) we have
P 00 `C qVal(W σ 0 ) ⇐ Π. Because of Lemma 3.1(1) this implies Π |=C qVal(W σ 0 ),
i.e. SolC (Π) ⊆ SolC (qVal(W σ 0 )). Since ν ∈ SolC (Π) we get ν ∈ SolC (qVal(W σ 0 )),
i.e. W σ 0 ν ∈ ran(ı). Since W σ 0 ν = W θ, we are done.
Next, we explain how to define an abstract goal solving system for SQCLP from
a given abstract goal solving system for CLP.
Definition 4.4
Let CLP-AGSS be an abstract goal solving system for CLP(C) (in the sense of
Definition 3.3). Then we define SQCLP-AGSS as an abstract goal solving system
for SQCLP(S, D, C) that works as follows:
1. Given a goal G for the SQCLP(S, D, C)-program P, consider P 0, G0, P 00 and
G00 as explained at the beginning of the subsection.
2. For each solution hσ 0 , Πi computed by CLP-AGSS for G00, P 00 and for any
ν ∈ SolC (Π), SQCLP-AGSS computes hσ, µ, Πi where θ = σ 0 ν, σ = θvar(G)
and µ = θı−1 war(G). Note that µ is well-defined thanks to Lemma 4.3.
The next theorem ensures that SQCLP-AGSS is correct provided that CLPAGSS is also correct. The proof relies on the semantic results of the two previous
subsections.
Theorem 4.5
Assume that CLP-AGSS is correct (in the sense of Definition 3.3). Let SQCLPAGSS be as in the previous definition. Then SQCLP-AGSS is correct in the sense
of Definition 2.3.
Proof
We separately prove that SQCLP-AGSS is sound and weakly complete.
— SQCLP-AGSS is sound. Let hσ, µ, Πi be an answer computed by SQCLP-AGSS
for G, P. We must prove that hσ, µ, Πi ∈ SolP (G). By Definition 4.4 we can assume
hσ 0 , Πi ∈ SolP 00 (G00 ) and ν ∈ SolC (Π) such that σ = θvar(G) and µ = θı−1 war(G)
with θ = σ 0 ν. Because of Lemma 4.3 we have hθ, Πi ∈ SolP 00 (G00 ) and W θ ∈ ran(ı)
for every W ∈ var(G00 ) \ var(G). Note that:
• θ =var(G0 ) σ. This follows from var(G0 ) = var(G) and the construction of σ.
• θ =war(G0 ) µı. This follows from war(G0 ) = war(G) and θ =war(G) µı, that is obvious
from the construction of µ.
• W θ ∈ ran(ı) for each W ∈ var(G00 ) \ (var(G0 ) ∪ war(G0 )). This is a consequence of
Lemma 4.3 since var(G00 ) \ (var(G0 ) ∪ war(G0 )) ⊆ var(G00 ) \ var(G0 ) and var(G0 ) =
var(G).
From the previous items and Theorem 4.4 we get hσ, µ, Πi ∈ SolP 0 (G0 ), which
trivially implies hσ, µ, Πi ∈ SolP (G) because of Theorem 4.2.

34

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

— SQCLP-AGSS is weakly complete. Let hη, ρ, ∅i ∈ GSolP (G) be a ground solution
for G w.r.t. P. We must prove that it is subsumed—in the sense of Definition
2.2(3)—by some answer hσ, µ, Πi computed by SQCLP-AGSS for G, P.
By Theorem 4.2 we have that hη, ρ, ∅i is also a ground solution for G0 w.r.t. P 0 .
In addition, by Theorem 4.4 hη 0 , ∅i ∈ SolP 00 (G00 ) for some η 0 such that
• (1) η 0 =var(G0 ) η,
• (2) η 0 =war(G0 ) ρı and hence η 0 (ı−1 ) =war(G0 ) ρ, and
• W η 0 ∈ ran(ı) for each W ∈ var(G00 ) \ (var(G0 ) ∪ war(G0 )) (i.e. wi0 η 0 ∈ ran(ı) for each
i = 1 . . . m such that wi0 is a variable).
By construction of η 0 , it is clear that hη 0 , ∅i is ground. Now, by the weak completeness of CLP-AGSS, there is some computed answer hσ 0 , Πi subsuming hη 0 , ∅i,
therefore satisfying
• (3) there is some ν ∈ SolC (Π), and
• (4) η 0 =var(G00 ) σ 0 ν.
Because of Definition 4.4 one can build a SQCLP-AGSS computed answer hσ, µ, Πi
as follows:
• (5) σ = σ 0 νvar(G)
• (6) µ = σ 0 νı−1 war(G)
We now check that hσ, µ, Πi subsumes hη, ρ, ∅i:
• Wi ρ P Wi µ and even Wi ρ = Wi µ because:

Wi ρ =(2) Wi η 0 (ı−1 ) =(4) Wi σ 0 ν(ı−1 ) =(6) Wi µ .

• ν ∈ SolC (Π) by (3) and, moreover, for any X ∈ var(G):
Xη =(1) Xη 0 =(4) Xσ 0 ν =(†) Xσ 0 νν =(5) Xσν
therefore η =var(G) σν.
The step (†) is justified because ν ∈ ValC implies ν = νν.

5 A Practical Implementation
This section is devoted to the more practical aspects of the SQCLP programming
scheme and it is developed in three subsections: Subsection 5.1 explains what steps
must be given when implementing a programming scheme like this and why the
theoretic results presented in the previous sections—with special emphasis in those
in Subsection 4.3—become useful for implementation. Subsection 5.2 introduces a
prototype implementation and explains how to write programs and how to solve
goals. Finally, in Subsection 5.3 we study the unavoidable overload introduced in
the system by qualifications and proximity relations when comparing the execution
of programs without any explicit use of such resources.

A Transformation-based Implementation for SQCLP (Preliminary Version) 35
5.1 SQCLP over a CLP Prolog System
Assume an available CLP Prolog System, a SQCLP(S, D, C)-program P and a goal
G for P. Our purpose is to implement a goal solving system for SQCLP following
Definition 4.4. We will examine each step in this schema, discussing the necessary
implementation details for putting theory into practice.
The first step is to obtain the transformed programs P 0 = elimS (P) and P 00 =
elimD (P 0 ); and the transformed goals G0 = elimS (G) and G00 = elimD (G0 ). According to Definition 4.2(3), P 0 = elimS (P) is of the form EQS ∪ P̂S , where EQS is
obtained following Definition 4.1 and P̂S is obtained following Definition 4.2(3,2).
When implementing EQS a first difficulty arises, namely the implementation of
∼ ∈ DP 2, which apparently requires one clause of the form:
t

u ∼ u0 ←
− payλ ]?
for each pair u, u0 ∈ BC such that S(u, u0 ) = λ 6= b, and one clause of the form:
t

c(X n ) ∼ c0 (Y n ) ←
− payλ ]?, ((Xi ∼ Yi )]?)i=1...n
for each pair c, c0 ∈ DC n such that S(c, c0 ) = λ 6= b. While this should obviously
require an infinite number of clauses (because DC n is infinite and S(c, c) = t 6= b
for all c ∈ DC n ; and also BC is infinite—in general—and S(u, u) = t 6= b for every
u ∈ BC ), in practice, it is enough to limit the number of clauses to the finite number
of different basic values u ∈ BC and constructors c ∈ DC n that can be found either
in P, G or S.
A similar difficulty arises when codifying the clauses for predicates payλ ∈ DP 0,
which according to Definition 4.1 there should be a clause of the form:
λ

payλ ←
−
in EQS for each λ ∈ DD \ {b}. In this case, the solution is also similar because
it suffices to generate enough payλ clauses for the finite λ ∈ DD \ {b} that can
be found occurring either in the clauses of P̂S or in the clauses implementing the
predicate ∼ ∈ DP 2.
The construction of P̂S , following Definition 4.2, presents no particular difficulα
− B) ∈ P we will generate a finite set CˆS of clauses,
ties. For each clause C : (p(tn ) ←
because the number of symbols p0 such that S(p, p0 ) = λ 6= b will be also finite in
practice. Finally, the construction of G0 is merely the straightforward replacement
of all the occurrences of ‘==’ in G by ‘∼’.
The transformation elimD from QCLP(D, C) into CLP(C), is defined in Definition 4.3. P 00 = elimD (P 0 ) is obtained by incorporating the two clauses of the
program ED to the result of applying the transformation rules in Figure 5 to the
QCLP(D, C)-program P 0. Applying the transformation rules is straightforward, but
the codification of constraints qVal(X) and qBound(X, Y, Z) in ED requires some
clarification. In our implementation we have considered the constraint domain R,
as well as any qualification domain that can be built from B, U and W by means
of the strict cartesian product operation ⊗ including, in particular, U⊗W. These
qualification domains are existentially expressible in R, therefore the constraints

36

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

can be implemented by defined predicates as explained in Section 4.2. In particular
in our prototype implementation these predicates are:
% qval( +QDom, ?W ):
qval(b, 1).
qval(u, W) :- {W > 0, W =< 1}.
qval(w, W) :- {W >= 0}.
qval((D1,D2), (W1,W2)) :- qval(D1, W1), qval(D2, W2).
% qbound( +QDom, ?X, ?Y, ?Z ):
qbound(b, 1, 1, 1).
qbound(u, X, Y, Z) :- {X =< Y * Z}.
qbound(w, X, Y, Z) :- {X >= Y + Z}.
qbound((D1,D2), (X1,X2), (Y1,Y2), (Z1,Z2)) :- qbound(D1, X1, Y1, Z1),
qbound(D2, X2, Y2, Z2).
Instead of using different qVal and qBound predicates for each allowable D, our
prototype implementation just uses two predicates qVal and qBound with an extra
first argument, used to encode an identifier of some specific allowable D. This parameter can take either the value b (for B), u (for U), w (for W) or a pair (D1 ,D2 )
(for D1 ⊗ D2 ), where each Di can be either b, u, w or another pair representing a
product. For instance ((u,w),w) represents the qualification domain (U⊗W)⊗W.
The compiler ensures that this argument takes the correct value for each transformed program and goal depending on the specific instance of the SQCLP scheme
the program is written for.
After obtaining P 00 and G00, the CLP Prolog System is used to solve G00 w.r.t.
00
P . This yields computed answers of the form hσ 0 , Πi. Now, instead of obtaining
particular substitutions θ = σ 0 ν, σ = θvar(G) and µ = θı−1 war(G) for any
ν ∈ SolC (Π) as explained in Definition 4.4(2), our prototype implementation limits
itself to display hσ 0 , Πi as the computed answer in SQCLP. The reason behind this
behavior is that, in general (and particularly in R), it is impossible to enumerate the
possible solutions ν ∈ SolC (Π). Thus, it results impossible to implement a technique
for obtaining all the possible triples hσ, µ, Πi. Note, however, that for a user it
will not be difficult to distinguish, in the shown computed answers, what variable
bindings correspond to the substitution σ of the triple and what to the substitution
µ, even when the qualification variables are not bound but constrained, which is a
common behavior in the context of CLP programming.
However, for the SQCLP-AGSS of Definition 4.4, it results mandatory to define
the computed answers in terms of ν ∈ SolC (Π), because our SQCLP-semantics relies
on proving instances of G for some specific ground values of the variables in war(G).
5.2 (S)QCLP: A Prototype System for SQCLP Programming
The prototype implementation object of this subsection is publicly available, and
can be found at:
http://gpd.sip.ucm.es/cromdia/qclp

A Transformation-based Implementation for SQCLP (Preliminary Version) 37
The system currently requires the user to have installed either SICStus Prolog or
SWI-Prolog, and it has been tested to work under Windows, Linux and MacOSX
platforms. The latest version available at the time of writing this paper is 0.6. If
a latter version is available some things might have changed but in any case the
main aspects of the system should remain the same. Please consult the changelog
provided within the system itself for specific changes between versions.
SQCLP is a very general programming scheme and, as such, it supports different
proximity relations, different qualification domains and different constraint domains
when building specific instances of the scheme for any specific purpose. As it would
result impossible to provide an implementation for every admissible triple (or instance of the scheme), it becomes mandatory to decide in advance what specific
instances will be available for writing programs in (S)QCLP. In essence:
1. In its current state, the only available constraint domain is R. Thus, under
both SICStus Prolog and SWI-Prolog the library clpr will provide all the
available primitives in (S)QCLP programs.
2. The available qualification domains are: ‘b’ for the domain B; ‘u’ for the
domain U; ‘w’ for the domain W; and any strict cartesian product of those,
as e.g. ‘(u,w)’ for the product domain U⊗W.
3. With respect to proximity relations, the user will have to provide, in addition
to the two symbols and their proximity value, their kind (either predicate or
constructor) and their arity. Both kind and arity must be the same for each
pair of symbols having a proximity value different of b.
Note, however, that when no specific proximity relation S is provided for a given
program, Sid is then assumed. Under this circumstances, an obvious technical optimization consists on transforming the original program only with elimD , thus
reducing the overload introduced in this case by elimS . The reason behind this
optimization is that for any given SQCLP(Sid , D, C)-program P, it is also true
that P is a QCLP(D, C)-program, therefore elimD (elimS (P)) must semantically
be equivalent to elimD (P). Nevertheless, elimD (P) behaves more efficiently than
elimD (elimS (P)) due to the reduced number of resulting clauses. Thus, in order to
improve the efficiency, the system will avoid the use of elimS when no proximity
relation is provided by the user.
The final available instances in the (S)QCLP system are: SQCLP(S, b, clpr),
SQCLP(S, u, clpr), SQCLP(S, w, clpr), SQCLP(S, (u, w), clpr), . . . and their counterparts in the QCLP scheme when S = Sid .
5.2.1 Programming in (S)QCLP
Programming in (S)QCLP is straightforward if the user is accustomed to the Prolog
programming style. However, there are three syntactic differences with pure Prolog:
1. Clauses implications are replaced by “<-d-” where d ∈ D \ {b}. If d = t, then
the implication can become just “<--”. E.g. “<-0.9-” is a valid implication
in the domains U and W; and “<-(0.9,2)-” is a valid implication in the
domain U⊗W.

38

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az
2. Clauses in (S)QCLP are not finished with a dot (.). They are separated by
layout, therefore all clauses in a (S)QCLP program must start in the same
column. Otherwise, the user will have to explicitly separate them by means
of semicolons (;).
3. After every body atom (even constraints) the user can provide a threshold
condition using ‘#’. The notation ‘?’ can also be used instead of some particular qualification value, but in this case the threshold condition ‘#?’ can be
omitted.

Comments are as in Prolog:
% This is a line comment.
/* This is a multi-line comment, /* and they nest! */. */
and the basic structure of a (S)QCLP program is the following (line numbers are for
reference):
File: Peano.qclp
1
2
3
4
5
6

% Directives...
# qdom w
% Program clauses...
% num( ?Num )
num(z) <-num(s(X)) <-1- num(X)

In the previous small program, lines 1, 3 and 4 are line comments, line 2 is a
program directive telling the compiler the specific qualification domain the program
is written for, and lines 5 and 6 are program clauses defining the well-known Peano
numbers. As usual, comments can be written anywhere in the program as they
will be completely ignored (remember that a line comment must necessarily end
in a new line character, therefore the very last line of a file cannot contain a line
comment), and directives must be declared before any program clause. There are
three program directives in (S)QCLP:
1. The first one is “#qdom qdom” where qdom is any system available qualification
domain, i.e. b, u, w, (u,w). . . See line 2 in the previous program sample as an
example. This directive is mandatory because the user must tell the compiler
for which particular qualification domain the program is written.
2. The second one is “#prox file” where file is the name of a file (with extension
.prox containing a proximity relation. If the name of the file starts with a
capital letter, or it contains spaces or any special character, file will have to
be quoted with single quotes. For example, assume that with our program
file we have another file called Proximity.prox. Then, we would have to write
“#prox ‘Proximity’” to link the program with such proximity relation. This
directive is optional, and if omitted, the system assumes that the program is
of an instance of the QCLP scheme.
3. The third one is “#optimized unif”. This directive tells the compiler that
the program is intended to be used with the optimized version of the unification algorithm, what improves the general efficiency of the goal solving

A Transformation-based Implementation for SQCLP (Preliminary Version) 39
process. However, as noted at the end of Section 2, this could have the effect
of losing valid answers, although we conjecture that if the proximity relation
is transitive and if the program clauses do not make use of attenuation factors
other that t, this will not happen.
Proximity relations are defined in files of extension .prox with the following form:
File: Work.prox
1
2
3
4

% Predicates: pprox( S1, S2, Arity, Value ).
pprox(wrote, authored, 2, (0.9,0)).
% Constructors: cprox( S1, S2, Arity, Value ).
cprox(king_lear, king_liar, 0, (0.8,2)).

where the file can contain pprox/4 Prolog facts, for defining proximity between
predicate symbols of any arity; or cprox/4 Prolog facts, for defining proximity
between constructor symbols of any arity. The arguments of both pprox/4 and
cprox/4 are: the two symbols, their arity and its proximity value. Note that, although it is not made explicit the qualification domain this proximity relation is
written for, all values in it must be of the same specific qualification domain, and
this qualification domain must be the same declared in every program using the
proximity relation. Otherwise, the solving of equations may produce unexpected
results or even fail.
Reflexive and symmetric closure is inferred by the system, therefore, there is no
need for writing reflexive proximity facts, nor the symmetric variants of proximity
facts already provided. You can notice this in the previous sample file in which
neither reflexive proximity facts, nor the symmetric proximity facts to those at lines
2 and 4 are provided. In the case of being explicitly provided, additional (repeated)
solutions might be computed for the same given goal, although soundness and weak
completeness of the system should still be preserved. Transitivity is neither checked
nor inferred so the user will be responsible for ensuring it if desired.
As the reader would have already guessed, the file Work.prox implements the
proximity relation Sr of Example 4.1 in (S)QCLP. Finally, the program Pr of Example 4.1 can be represented in (S)QCLP as follows:
File: Work.qclp
1
2
3
4
5
6
7
8
9

# qdom (u,w)
# prox ’Work’
% famous( ?Author )
famous(shakespeare) <-(0.9,1)% wrote( ?Author, ?Book )
wrote(shakespeare, king_lear) <-(1,1)wrote(shakespeare, hamlet) <-(1,1)% good_work( ?Work )
good_work(X) <-(0.75,3)- famous(Y)#(0.5,100), authored(Y,X)

Note that, at line 1 the qualification domain U⊗W is declared, and at line 2 the
proximity relation at Work.prox is linked to the program. In addition, observe

40

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

that one threshold constraint is imposed for a body atom in the program clause at
line 9, effectively requiring to prove famous(Y) for a qualification value of at least
(0.5,100) to be able to use this program clause.
Finally, we explain how constraints are written in (S)QCLP. As it has already
been said, only R is available, thus both in SICStus Prolog and SWI-Prolog the
library clpr is the responsible for providing the available primitive predicates.
Given that constraints are primitive atoms of the form r(tn ) where r ∈ P P n and
ti are terms; primitive atoms share syntax with usual Prolog atoms. At this point,
and having that many of the primitive predicates are syntactically operators (hence
not valid identifiers), the syntax for predicate symbols has been extended to include
operators, therefore predicate symbols like op+ ∈ P P 3 , which codifies the operation
+ in a 3-ary predicate, will let us to build constraints of the form +(A,B,C), that
must be understood as in A + B = C or C = A + B. Similarly, predicate symbols
like cp> ∈ P P 2 , which codifies the comparison operator > in a binary predicate,
will let us to build constraints of the form >(A,B), that must be understood as in
A > B. Any other primitive predicate such as maximize ∈ P P 1 , will let us to build
constraints like maximize(X). Valid primitive predicate symbols include +, -, *, /,
>, >=, =<, <, maximize, minimize, etc.
Threshold constraints can also be provided for primitive atoms in the body of
clauses with the usual notation. Note, however, that due the semantics of SQCLP,
all primitive atoms can be trivially proved with t if they ever succeeds—so threshold
constraints become, in this case, of no use.
The syntax for constraints explained above follows the standard syntax for atoms.
Nonetheless, the system also allows to write these constraints in a more natural infix notation. More precisely, +(A,B,C) can be also written in the infix form A+B=C
or C=A+B, and >(X,Y) in the infix form X>Y; and similarly for other op and cp constraints. When using infix notation, threshold conditions can be set by (optionally)
enclosing the primitive atom between parentheses, therefore becoming (A+B=C)#t,
(C=A+B)#t or (X>Y)#t (or any other valid qualification value or ‘?’). Using parentheses is recommended to avoid understanding that the threshold condition is set
only for the last term in the constraint, which would not be the case. Note that
even in infix notation, operators cannot be nested, that is, terms A, B, C, X and Y
cannot have operators as main symbols (neither in prefix nor in infix notation), so
the infix notation is just a syntactic sugar of its corresponding prefix notation.
As a final example for constraints, one could write the predicate double/2 in
(S)QCLP, for computing the double of any given number, with just the clause
double(N,D) <-- *(N,2,D), or double(N,D) <-- N*2=D for a clause with a more
natural syntax.
5.2.2 The interpreter for (S)QCLP
The interpreter for (S)QCLP has been implemented on top of both SICStus Prolog
and SWI-Prolog. To load it, one must first load her desired (and supported) Prolog
system and then load the main file of the interpreter—i.e. qclp.pl—, that will
be located in the main (S)QCLP folder among other folders. Once loaded, one will

A Transformation-based Implementation for SQCLP (Preliminary Version) 41
see the welcome message and will be ready to compile and load programs, and to
execute goals.
WELCOME TO (S)QCLP 0.6
(S)QCLP is free software and comes with absolutely no warranty.
Support & Updates: http://gpd.sip.ucm.es/cromdia/qclp.
Type ’:help.’ for help.
yes
| ?From the interpreter for (S)QCLP one can, in addition to making use of any standard Prolog goals, use the specific (S)QCLP commands required for both interacting
with the (S)QCLP system, and for compiling/loading SQCLP programs. All these
commands take the form:
:command.
if they do not require arguments, or:
:command(Arg1 , ..., Argn ).
if they do; where each argument Argi must be a prolog atom unless stated otherwise.
The most useful commands are:
• :cd(Folder).
Changes the working directory to Folder. Folder can be an absolute or relative
path.
• :compile(Program).
Compiles the (S)QCLP program ‘Program.qclp’ producing the equivalent Prolog program in the file ‘Program.pl’.
• :load(Program).
Loads the already compiled (S)QCLP program ‘Program.qclp’ (note that the
file ‘Program.pl’ must exist for the program to correctly load).
• :run(Program).
Compiles the (S)QCLP program ‘Program.qclp’ and loads it afterwards. This
command is equivalent to executing: :compile(Program), :load(Program).
For illustration purposes, we will assume that you have the files Work.prox and
Work.qclp (both as seen before) in the folder ∼/examples. Under these circumstances, after loading your preferred Prolog system and the interpreter for (S)QCLP,
one would only have to change the working directory to that where the files are
located:
| ?- :cd(’∼/examples’).
and run the program:
| ?- :run(’Work’).
If no errors are encountered, one should see the output:

42

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

| ?- :run(’Work’).
<Work> Compiling...
<Work> QDom: ’u,w’.
<Work> Prox: ’Work’.
<Work> Translating to QCLP...
<Work> Translating to CLP...
<Work> Generating code...
<Work> Done.
<Work> Loaded.
yes
and now everything is ready to execute goals for the program loaded.
5.2.3 Executing SQCLP-Goals
Recall that goals have the form A1 ]W1 , . . . , Am ]Wm 8 W1 Q? β1 , . . . , Wm Q? βm
which in actual (S)QCLP syntax becomes:
| ?- A1#W1, ..., Am#Wm :: W1 >= B1, ..., Wm >= Bm.
Note the following:
1. Goals must end in a dot (.).
2. The symbol ‘8’ is replaced by ‘::’.
3. The symbol ‘Q? ’ is replaced by ‘>=’ (and this is independent of the qualification domain in use, so that it may mean ≤ in W).
4. Conditions of the form W Q? ? must be omitted, therefore A1 ]W1 , A2 ]W2 8
W1 Q? ?, W2 Q? β2 becomes “A1#W1, A2#W2 :: W2 >= B2.”, and A]W 8
W Q? ? becomes just “A#W.”.

Assuming now that we have loaded the program Work.qclp as explained before,
we can execute the goal good work(king liar)]W 8 W Q? (0.5, 100):
| ?- good_work(king_liar)#W::W>=(0.5,10).
W = (0.6,5.0) ?
yes
5.2.4 Examples

To finish this subsection, we are now showing some additional goal executions using
the interpreter for (S)QCLP and the programs displayed along the paper.
Peano. Consider the program Peano.qclp as displayed at the beginning of Subsection 5.2.1. Qualifications in this program are intended as a cost measure for
obtaining a given number in the Peano representation, assuming that each use of
the clause at line 6 requires to pay at least 1. In essence, threshold conditions will
impose an upper bound over the maximum number obtainable in goals containing
the atom num(X). Therefore if we ask for numbers up to a cost of 3 we get the
following answers:

A Transformation-based Implementation for SQCLP (Preliminary Version) 43
Goal

?- num(X)#W::W>=3.

Sol1

W =
W =
W =
W =
no

Sol2
Sol3
Sol4

0.0,
1.0,
2.0,
3.0,

X
X
X
X

=
=
=
=

z ? ;
s(z) ? ;
s(s(z)) ? ;
s(s(s(z))) ? ;

Work. Consider now the program Work.qclp and the proximity relation Work.prox,
both as displayed in Subsection 5.2.1 above. In this program, qualifications behave
as the conjunction of the certainty degree of the user confidence about some particular atom, and a measure of the minimum cost to pay for proving such atom. In
these circumstances, we could ask—just for illustration purposes—for famous authors with a minimum certainty degree—for them being actually famous—of 0.5,
and with a proof cost of no more than 30 (think of an upper bound for possible searches in different databases). Such a goal would have, in this very limited
example, only the following solution:
Goal

?- famous(X)#W::W>=(0.5,30).

Sol1

W = (0.9,1.0), X = shakespeare ? ;
no

meaning that we can have a confidence of shakespeare being famous of 0.9, and
that we can prove it with a cost of 1.
Now, in a similar fashion we could try to obtain different works that can be
considered as good works by using the last clause in the example. Limiting the
search to those works that can be considered good with a qualification value better
or equal to (0.5,100) produce the following result:
Goal

?- good_work(X)#W::W>=(0.5,100).

Sol1

W = (0.675,4.0), X = king_lear ? ;
W = (0.6,5.0), X = king_liar ? ;
no

Sol2

It is important to remark here that the qualification value obtained for a particular
computed answer is not guaranteed to be the best possible one; rather, different
computed answers may compute different qualification values which can be observed
by the user. This is easy to see if we try to solve a more particular goal:
Goal

?- good_work(king_liar)#W::W>=(0.675,4.0).

Sol1

W = (0.675,4.0) ? ;
no

That is, not only good work(king liar) can be proved for for W = (0.6,5.0)
as shown in Sol2 above, but also with W = (0.675,4.0), which results a better
qualification value (i.e. greater certainty degree and lower proof cost).
Library. Finally, consider the program Ps and the proximity relation Ss , both as
displayed in Figure 1 of Section 2. As it has been said when this example was
introduced, the predicate guessRdrLvl takes advantage of attenuation factors to

44

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

encode heuristic rules to compute reader levels on the basis of vocabulary level and
other book features. As an illustration of use, consider the following goal:
Goal

?- guessRdrLvl(book(2, ’Dune’, ’F. P. Herbert’, english, sciFi,
medium, 345), Level)#W.

Sol1

W = 0.8, Level = intermediate ? ;
···
W = 0.7, Level = upper ?
yes

Sol6

Here we ask for possible ways of classifying the second book in the library according
to reader levels. We obtain as valid solutions, among others, intermediate with
a certainty factor of 0.8; and upper with a certainty factor of 0.7. These valid
solutions show that the predicate guessRdrLvl tries with different levels for any
certain book based on the heuristic implemented by the qualified clauses.
To conclude, consider now the goal proposed in Section 2 for this program. For
such goal we obtain:
Goal

?- search(german, essay, intermediate, ID)#W::W>=0.65.

Sol1

W = 0.8, ID = 4 ?
yes

What tells us that the forth book in the library is written in German, it can be
considered to be an essay, and it is targeted for an intermediate reader level. All
this with a certainty degree of at least 0.8.
5.3 Efficiency
The minimum—and unavoidable—overload introduced by qualifications and proximity relations in the transformed programs manifests itself in the case of (S)QCLP
programs which use the identity proximity relation and have t as the attenuation
factor of all their clauses. In order to measure this overload we have made some experiments using some program samples, taken from the SICStus Prolog Benchmark
that can be found in:
http://www.sics.se/isl/sicstuswww/site/performance.html
and we have compared the time it took to repeatedly execute a significant number
of times each program in both (S)QCLP and SICStus Prolog making use of a slightly
modified (to ensure a correct behavior in both systems) version of the harness also
provided in the same site.
From all the programs available in the aforementioned site, we selected the following four:
• naivrev: naive implementation of the predicate that reverses the contents of
a list.
• deriv: program for symbolic derivation.
• qsort: implementation of the well-known sorting algorithm Quicksort.
• query: obtaining the population density of different countries.

A Transformation-based Implementation for SQCLP (Preliminary Version) 45
No other program could be used because they included impure features such as cuts
which are not currently supported by our system. In order to adapt these Prolog
programs to our setting the following modifications were required:
1. All the program clause are assumed to have t as attenuation factor. After
including these attenuation factors, we obtain as results QCLP programs.
More specifically we obtain two QCLP programs for each initial Prolog program, one using the qualification domain B (because this domain uses trivial
constraints), and another using the qualification domain U (which uses Rconstraints).
2. We define an empty proximity relation, allowing us to obtain two additional
SQCLP-programs.
3. By means of the program directive “#optimized unif” defined in Subsection
5.2.1, each SQCLP program can be also executed in this optimized mode.
Therefore each original Prolog Program produces six (S)QCLP programs, denoted as Q(b), Q(u), PQ(b), PQ(u), SQ(b) and SQ(u) in Table 1.
Additionally some minor modifications to the program samples have been introduced for compatibility reasons, i.e. additions using the predicate is/2 were
replaced, both in the Prolog version of the benchmark and in the multiple (S)QCLP
versions, by clpr constraints. In any case, all the program samples used for this
benchmarks in this subsection can be found in the folder benchmarks/ of the
(S)QCLP distribution.
Finally, we proceeded to solve the same goals for every version of the benchmark
programs, both in SICStus Prolog and in (S)QCLP. The benchmark results can be
found in Table 1. All the experiments were performed in a computer with a Intel(R)
Core(TM)2 Duo CPU at 2.19GHz and with 3.5 GB RAM.
Table 1. Time overload factor with respect to Prolog
Program
naivrev
deriv
qsort
query
a
b
c
d
e
f

Q(b)a

Q(u)b

PQ(b)c

PQ(u)d

SQ(b)e

SQ(u)f

1.80
1.94
1.05
1.02

10.71
10.60
1.11
1.12

4289.79
331.45
135.59
7.17

4415.11
469.67
136.98
7.13

56.22
29.63
2.51
3.80

65.75
39.32
2.83
3.88

QCLP(B, R) version (i.e. the program does not have
QCLP(U , R) version (i.e. the program does not have
SQCLP(Sid , B, R) version.
SQCLP(Sid , U , R) version.
SQCLP(Sid , B, R) version with directive #optimized
SQCLP(Sid , U , R) version with directive #optimized

the #prox directive).
the #prox directive).

unif.
unif.

The results in the table indicate the slowdown factor obtained for each version
of each program. For instance, the first column indicates that the time required for
evaluating the goal corresponding to the sample program naivrev in QCLP(B, R)
is about 1.80 times the required time for the evaluation of the same goal in Prolog.
Next we discuss the results:

46

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az
• Influence of the qualification domain. In general the difference between the
slowdown factors obtained for the two considered qualification domains is not
large. However, in the case of QCLP-programs naivrev and deriv the difference
increases notably. This is due to the different ratios of the B-constraints w.r.t.
the program and U-constraints w.r.t. the program. It must be noticed that the
transformed programs are the same in both cases, but for the implementation
of qval and qbound constraints, which is more complex for U as one can see
in Section 5.1. In the case of naivrev and deriv this makes a big difference
because the number of computation steps directly required by the programs
is much smaller than in the other cases. Thus the slowdown factor becomes
noticeable for the qualification domain U in computations that requires a
large number of steps.
• Influence of the proximity relation. The introduction of a proximity relation,
even of empty, is very significative. This is due to the introduction of the predicate ∼, which replaces Prolog unification. The situation even worsens when
the computation introduces large constructor terms, as in the case of naivrev
which deals with Prolog lists. The efficient Prolog unification is replaced by
an explicit term decomposition.
• Influence of the optimized unification. As explained at the end of Section 2
this optimization can lead to the loss of solutions in general. However, this
is not the case for the chosen examples. As seen in the table, the use of the
program directive #optimized unif causes a clear increase in the efficiency
of goal solving for these examples.
6 Conclusions

In our recent work (Rodrı́guez-Artalejo and Romero-Dı́az 2010a) we extended the
classical CLP scheme to a new programming scheme SQCLP whose instances
SQCLP(S, D, C) were parameterized by a proximity relation S, a qualification domain D and a constraint domain C. This new scheme offered extra facilities for
dealing with expert knowledge representation and flexible query answering. In this
paper we have contributed to the aforementioned scheme providing, in a more practical sense, both a semantically correct transformation technique, in two steps, for
transforming SQCLP programs and goals intro equivalent CLP programs and goals;
and a prototype implementation on top CLP(R) systems like SICStus Prolog and
SWI-Prolog of some particularly interesting instances of the scheme.
The two-step transformation technique presented in Section 4 has provided us
with the needed theoretical results for effectively showing how proximity relations
can be reduced to qualifications and clause annotations by means of the transformation elimS ; and how qualifications and clause annotations can be reduced to
classical CLP programming by means of the transformation elimD . These two transformations altogether, ultimately enables the use of the classical mechanism of SLD
resolution to obtain computed answers for SQCLP goals w.r.t SQCLP programs,
via their equivalent CLP programs and goals and the computed answers obtained
from them by any capable CLP goal solving procedure.

A Transformation-based Implementation for SQCLP (Preliminary Version) 47
The prototype implementation presented in Section 5 has finally allowed us to
execute all the examples showed in this paper—and in previous ones—, and a series of benchmarks for measuring the overload actually introduced by proximity
relations—or by similarity relations—and by clause annotations and qualifications.
While we are aware that the prototype implementation presented in this paper has
to be considered a research application (and as such, we have to admit that it cannot be used for industrial applications), we think that it can contribute to the field
as a quite complete implementation of an extension of the CLP(R) scheme with
proximity relations and qualifications. Some related implementation techniques and
systems have been cited in the introduction. However, as far as we know, no other
implementation in this field has ever provided support for proximity (and similarity) relations, qualifications via clause annotations and CLP(R) style programming.
Moreover, our results in Section 4 on the semantic correctness of our implementation technique are in our opinion another contribution of this paper which has no
counterpart in related approaches.
In the future, and taking advantage of the prototype system we have already
developed, we plan to investigate possible applications which can profit from proximity relations and qualifications, such as in the area of flexible query answering.
In particular, we plan to investigate application related to flexible answering of
queries to XML documents, in the line of (Campi et al. 2009) and other related
papers. As support for practical applications, we also plan to increase the repertoire
of constraint and qualification domains which can be used in the (S)QCLP prototype, adding the constraint domain FD and the qualification domain Wd defined
in Section 2.2.3 of (Rodrı́guez-Artalejo and Romero-Dı́az 2010b). On a more theoretical line, other possible lines of future work include: a) extension of the SLD(D)
resolution procedure presented in (Rodrı́guez-Artalejo and Romero-Dı́az 2008) to
a SQCLP goal solving procedure able to work with constraints and a proximity
relation; b) investigation of the conjecture stated at the end of Section 2; and c)
extension of the QCFLP (qualified constraint functional logic programming) scheme
in (Caballero et al. 2009) to work with a proximity relation and higher-order functions, as well as the implementation of the resulting scheme in the CFLP(C)-system
Toy (Arenas et al. 2007).

References
Apt, K. R. 1990. Logic programming. In Handbook of Theoretical Computer Science,
J. van Leeuwen, Ed. Vol. B: Formal Models and Semantics. Elsevier and The MIT Press,
493–574.
Arcelli, F. and Formato, F. 1999. Likelog: a logic programming language for flexible data retrieval. In Proceedings of the 1999 ACM Symposium on Applied computing
(SAC’99). ACM Press, New York, NY, USA, 260–267.
Arcelli Fontana, F. 2002. Likelog for flexible query answering. Soft Computing 7,
107–114.
Arenas, P., Fernández, A. J., Gil, A., López-Fraguas, F. J., Rodrı́guez-Artalejo,
M., and Sáenz-Pérez, F. 2007. T OY, a multiparadigm declarative language. version
2.3.1. R. Caballero and J. Sánchez (Eds.), Available at http://toy.sourceforge.net.

48

R. Caballero, M. Rodrı́guez-Artalejo and C. A. Romero-Dı́az

Baader, F. and Nipkow, T. 1998. Term Rewriting and All That. Cambridge University
Press.
Baldwin, J. F., Martin, T., and Pilsworth, B. 1995. Fril-Fuzzy and Evidential Reasoning in Artificial Intelligence. John Wiley & Sons.
Bistarelli, S., Montanari, U., and Rossi, F. 2001. Semiring-based constraint logic
programming: Syntax and semantics. ACM Transactions on Programming Languages
and Systems 3, 1 (January), 1–29.
Caballero, R., Rodrı́guez-Artalejo, M., and Romero-Dı́az, C. A. 2008. Similaritybased reasoning in qualified logic programming. In PPDP ’08: Proceedings of the 10th
international ACM SIGPLAN conference on Principles and Practice of Declarative Programming. ACM, Valencia, Spain, 185–194.
Caballero, R., Rodrı́guez-Artalejo, M., and Romero-Dı́az, C. A. 2009. Qualified
computations in functional logic programming. In Logic Programming (ICLP’09), P. Hill
and D. Warren, Eds. LNCS, vol. 5649. Springer-Verlag Berlin Heidelberg, Pasadena, CA,
USA, 449–463.
Campi, A., Damiani, E., Guinea, S., Marrara, S., Pasi, G., and Spoletini, P. 2009.
A fuzzy extension of the XPath query language. Journal of Intelligent Information
Systems 33, 3 (December), 285–305.
Dubois, D. and Prade, H. 1980. Fuzzy Sets and Systems: Theory and Applications.
Academic Press, New York, NY, USA.
Freuder, E. C. and Wallace, R. J. 1992. Partial constraint satisfaction. Artificial
Intelligence 58, 1–3, 21–70.
Georget, Y. and Codognet, P. 1998. Compiling semiring-based constraints with
CLP(FD,S). In Proceedings of the 4th International Conference on Principles and Practice of Constraint Programming. LNCS, vol. 1520. Springer-Verlag, 205–219.
Guadarrama, S., Muñoz, S., and Vaucheret, C. 2004. Fuzzy prolog: A new approach
using soft constraint propagation. Fuzzy Sets and Systems 144, 1, 127–150.
Hájek, P. 1998. Metamathematics of Fuzzy Logic. Dordrecht: Kluwer.
Höhfeld, M. and Smolka, G. 1988. Definite relations over constraint languages. Tech.
Rep. LILOG Report 53, IBM Deutschland.
Ishizuka, M. and Kanai, N. 1985. Prolog-ELF incorporating fuzzy logic. In Proceedings
of the 9th International Joint Conference on Artificial Intelligence (IJCAI’85), A. K.
Joshi, Ed. Morgan Kaufmann, Los Angeles, CA, USA, 701–703.
Jaffar, J. and Lassez, J. L. 1987. Constraint logic programming. In Proceedings of the
14th ACM SIGACT-SIGPLAN symposium on Principles of Programming Languages
(POPL’87). ACM New York, NY, USA, Munich, West Germany, 111–119.
Jaffar, J., Maher, M., Marriott, K., and Stuckey, P. J. 1998. Semantics of constraints logic programs. Journal of Logic Programming 37, 1-3, 1–46.
Julián, R., Moreno, G., and Penabad, J. 2009. An improved reductant calculus using
fuzzy partial evaluation techniques. Fuzzy Sets and Systems 160, 2, 162–181.
Julián-Iranzo, P., Rubio, C., and Gallardo, J. 2009. Bousi∼Prolog: a prolog extension language for flexible query answering. In Proceedings of the Eighth Spanish Conference on Programming and Computer Languages (PROLE 2008), J. M. AlmendrosJiménez, Ed. ENTCS, vol. 248. Elsevier, Gijón, Spain, 131–147.
Julián-Iranzo, P. and Rubio-Manzano, C. 2009a. A declarative semantics for
Bousi∼Prolog. In PPDP’09: Proceedings of the 11th ACM SIGPLAN conference on
Principles and practice of declarative programming. ACM, Coimbra, Portugal, 149–160.
Julián-Iranzo, P. and Rubio-Manzano, C. 2009b. A similarity-based WAM for
Bousi∼Prolog. In Bio-Inspired Systems: Computational and Ambient Intelligence
(IWANN 2009). LNCS, vol. 5517. Springer Berlin / Heidelberg, Salamanca, Spain, 245–
252.

A Transformation-based Implementation for SQCLP (Preliminary Version) 49
Kifer, M. and Subrahmanian, V. S. 1992. Theory of generalized annotated logic
programs and their applications. Journal of Logic Programming 12, 3&4, 335–367.
Lee, R. C. T. 1972. Fuzzy logic and the resolution principle. Journal of the Association
for Computing Machinery (ACM) 19, 1 (January), 109–119.
Li, D. and Liu, D. 1990. A Fuzzy Prolog Database System. John Wiley & Sons.
Lloyd, J. W. 1987. Foundations of Logic Programming, Second Edition. Springer.
Loia, V., Senatore, S., and Sessa, M. I. 2004. Similarity-based SLD resolution and
its role for web knowledge discovery. Fuzzy Sets and Systems 144, 1, 151–171.
Medina, J., Ojeda-Aciego, M., and Vojtáš, P. 2001a. Multi-adjoint logic programming with continuous semantics. In Logic Programming and Non-Monotonic Reasoning
(LPNMR’01), T. Eiter, W. Faber, and M. Truszczyinski, Eds. LNAI, vol. 2173. SpringerVerlag, 351–364.
Medina, J., Ojeda-Aciego, M., and Vojtáš, P. 2001b. A procedural semantics for
multi-adjoint logic programming. In Progress in Artificial Intelligence (EPIA’01),
P. Brazdil and A. Jorge, Eds. LNAI, vol. 2258. Springer-Verlag, 290–297.
Medina, J., Ojeda-Aciego, M., and Vojtáš, P. 2004. Similarity-based unification: a
multi-adjoint approach. Fuzzy Sets and Systems 146, 43–62.
Riezler, S. 1998. Probabilistic constraint logic programming. Ph.D. thesis, Neuphilologischen Fakultät del Universität Tübingen.
Rodrı́guez-Artalejo, M. and Romero-Dı́az, C. A. 2008. Quantitative logic programming revisited. In Functional and Logic Programming (FLOPS’08), J. Garrigue and
M. Hermenegildo, Eds. LNCS, vol. 4989. Springer-Verlag, Ise, Japan, 272–288.
Rodrı́guez-Artalejo, M. and Romero-Dı́az, C. A. 2010a. A declarative semantics for
CLP with qualification and proximity. Theory and Practice of Logic Programming, 26th
Int’l. Conference on Logic Programming (ICLP’10) Special Issue 10, 4–6, 627–642.
Rodrı́guez-Artalejo, M. and Romero-Dı́az, C. A. 2010b. Fixpoint & Proof-theoretic
Semantics for CLP with Qualification and Proximity. Tech. Rep. SIC-1-10, Universidad
Complutense, Departamento de Sistemas Informáticos y Computación, Madrid, Spain.
Sessa, M. I. 2001. Translations and similarity-based logic programming. Soft Computing 5, 2.
Sessa, M. I. 2002. Approximate reasoning by similarity-based SLD resolution. Theoretical
Computer Science 275, 1-2, 389–426.
van Emden, M. H. 1986. Quantitative deduction and its fixpoint theory. Journal of Logic
Programming 3, 1, 37–53.
Vojtáš, P. 2001. Fuzzy logic programming. Fuzzy Sets and Systems 124, 361–370.
Zadeh, L. A. 1965. Fuzzy sets. Information and Control 8, 3, 338–353.
Zadeh, L. A. 1971. Similarity relations and fuzzy orderings. Information Sciences 3, 2,
177–200.

