Rules in a FASILL program have the same role than clauses in PROLOG (or MALP [8, 4, 11]) programs, that is, stating that a certain predicate relates some terms (the head) if some conditions (the body) hold.

As a logic language, FASILL inherits the concepts of substitution, unifier and most general unifier (mgu). Some of them are extended to cope with similarities. Concretely, the most general unifier is replaced by the concept of weak most general unifier (w.m.g.u.), following the line of Bousi∼Prolog [5]. Roughly speaking, the weak unification algorithm states that two expressions (i.e, terms or atomic formulas) f(t1,...,tn) and g(s1,...,sn) weakly unify if the root symbols f and g are close with a certain degree (i.e. R(f,g) = r > ⊥) and each of their arguments ti and si weakly unify. Therefore, there is a weak unifier for two expressions even if the symbols at their roots are not syntactically equals ( f ≡ g).

More technically, the weak unification algorithm we are using is a reformulation/extension of the one which appears in [16] for arbitrary complete lattices. We formalize it as a transition system supported by a similarity-based unification relation “⇒”. The unification of the expressions E1 and E2 is obtained by a state transformation sequence starting from an initial state ⟨G ≡ {E1 ≈ E2},id,α0⟩, where id is the identity substitution and α0 = ⊤ is the supreme of (L,≤): ⟨G,id,α0⟩ ⇒ ⟨G1,θ1,α1⟩ ⇒ ··· ⇒ ⟨Gn,θn,αn⟩. When the final state ⟨Gn,θn,αn⟩, with Gn = ∅, is reached (i.e., the equations in the initial state have been solved), the expressions E1 and E2 are unifiable by similarity with w.m.g.u. θn and unification degree αn. Therefore, the final state ⟨∅,θn,αn⟩ signals out the unification success. On the other hand, when expressions E1 and E2 are not unifiable, the state transformation sequence ends with failure (i.e., Gn = Fail).

Rule 1 decomposes two expressions and annotates the relation between the function (or predicate) symbols at their root. The second rule eliminates spurious information and the fourth rule interchanges the position of the symbols to be coped by other rules. The third and fifth rules perform an occur check of variable X in a term t. In case of success, it generates a substitution {X/t}; otherwise the algorithm ends with failure. It can also end with failure if the relation between function (or predicate) symbols in R is ⊥, as stated by Rule 6. 

Usually, given two expressions E1 and E2, if there is a successful transition sequence, ⟨{E1 ≈ E2},id,⊤⟩ ⇒⋆ ⟨∅,θ,r⟩, then we write that wmgu(E1,E2) = ⟨θ,r⟩, being θ the weak most general unifier of E1 and E2, and r is their unification degree.

Finally note that, in general, a w.m.g.u. of two expressions E1 and E2 is not unique [16]. Certainly, the weak unification algorithm only computes a representative of a w.m.g.u. class, in the sense that, if θ = {x1/t1,...,xn/tn} is a w.m.g.u., with degree β, then, by definition, any substitution θ′ = {x1/s1,...,xn/sn}, satisfying R(si,ti) > ⊥, for any 1 ≤ i ≤ n, is also a w.m.g.u. with approximation degree β′ = β ∧(∧n1 R(si,ti)), where “∧′′ is a selected t-norm. However, observe that, the w.m.g.u. representative computed by the weak unification algorithm is one with an approximation degree equal or greater than other w.m.g.u. As in the case of the classical syntactic unification algorithm, our algorithm always terminates returning a success or a failure.

In order to describe the procedural semantics of the FASILL language, in the following we denote by C[A] a formula where A is a sub-expression (usually an atom) which occurs in the –possibly empty– context C[] whereas C[A/A′] means the replacement of A by A′ in the context C[]. Moreover, Var(s) denotes the set of distinct variables occurring in the syntactic object s and θ[Var(s)] refers to the substitution obtained from θ by restricting its domain to Var(s). In the next definition, we always consider that A is the selected atom in a goal Q and L is the complete lattice associated to Π.

Definition 2.1 (Computational Step). Let Q be a goal and let σ be a substitution. The pair ⟨Q, σ⟩ is a state. Given a program ⟨Π,R,L⟩ and a t-norm ∧ in L, a computation is formalized as a state transition system, whose transition relation -> is the smallest relation satisfying these rules: 

1) Successful step (denoted as ->^SS): 

• ⟨Q[A], σ⟩ ->^SS ⟨Q[A/B∧r]θ, σθ⟩ if A′ ← B ∈ Π, wmgu(A,A′) = ⟨θ,r⟩ 

2) Failure step (denoted as ->^FS): 

• ⟨Q[A], σ⟩ ->^FS ⟨Q[A/⊥], σ ⟩ if there is no A′ ← B ∈ Π such that wmgu(A,A′) = ⟨θ,r⟩, r > ⊥ 

3) Interpretive step (denoted as ->^IS):

• ⟨Q[@(r1,...,rn)], σ⟩ ->^IS ⟨Q[@(r1,...,rn)/rn+1], σ⟩ if [[@]](r1,...,rn)=rn+1 

A derivation is a sequence of arbitrary lenght ⟨Q;id⟩ —>∗⟨Q′;σ⟩. As usual, rules are renamed apart. When Q′ = r ∈ L, the state ⟨r; σ ⟩ is called a fuzzy computed answer (f.c.a.) for that derivation.

4 For convenience, R (x, y), also denoted xR y, refers both the syntactic expression (that symbolizes that the elements x, y ∈ U are related by R ) and the truth degree μR (x, y), i.e., the affinity degree of the pair (x, y) ∈ U × U with the verbal predicate R .

5In order to subsume the syntactic conventions of MALP, in our programs we also admit weighted rules with shape “A ←i B with v”, which are internally treated as “A ← (v&iB)” (this transformation preserves the meaning of rules as proved in [10]).