The procedural semantics of the multi-adjoint logic language L can be thought as an operational phase followed by an interpretive one. In this section we establish a clear separation between both phases.
The operational mechanism uses a generalization of modus ponens that, given a goal A and a program rule <A′←i B, v>, if there is a substitution θ = mgu({A′ = A}), we substitute the atom A by the expression (v&iB)θ. In the following, C[A] denotes a formula where A is a sub-expression which occurs in the –possibly empty– context C[]. Moreover, C[A/A′] means the replacement of A by A′ in context C[], whereas Var(s) refers to the set of distinct variables occurring in the syntactic object s, and θ[Var(s)] denotes the substitution obtained from θ by restricting its domain to Var(s).
Definition 1.1 [Admissible Steps] Let Q be a goal and let σ be a substitution. The pair <Q; σ> is a state and we denote by E the set of states. Given a program P, an admissible computation is formalized as a state transition system, whose transition relation →AS ⊆ (E × E) is the smallest relation satisfying the following admissible rules (where we always consider that A is the selected atom in Q and mgu(E) denotes the most general unifier of an equation set E):
1) <Q[A]; σ>→AS<(Q[A/v&iB])θ; σθ> if θ = mgu({A′ = A}), <A′←i B; v> in P and B is empty.
For instance, given the following rule R: p(a) ←prod p(f(a)) with 0,7. and the following goal where p(X) (underlined) is the selected atom:
< (p(b) &godel p(X)) &godel q(X);id > →AS1
< (p(b) &godel 0,7 &prod p(f(a))) &godel q(a); {X/a}>
2) <Q[A]; σ> →AS<(Q[A/v])θ; σθ> if θ = mgu({A′ = A}), and <A′←i ; v> in P.
For instance, let rule R be the fact R: p(a) with 0,5. and let p(X) (underlined) be the selected atom in the next goal:
< (p(b) &godel p(X)) &godel q(X);id > →AS2
< (p(b) &godel 0,5) &godel q(a); {X/a}>
3) <Q[A]; σ>→AS<(Q[A/⊥]); σ> if there is no rule in P whose head unifies with A.
This case is useful to cope with unsuccessful derivations, as occurs with the following step where p(X) is undefined.
< (p(b) &godel p(X)) &godel q(X);id > →AS3
< (p(b) &godel 0) &godel q(X); id >
As usual, rules are taken renamed apart. We shall use the symbols →AS1, →AS2 and →AS3 to distinguish among computation steps performed by applying one of the specific admissible rules. Also, the application of a rule on a step will be annotated as a superscript of the →AS symbol.
Definition 1.2 Let P be a program and let Q be a goal. An admissible derivation is a sequence <Q; id >→∗AS<Q′;θ>. When Q′ is a formula not containing atoms, the pair <Q′;σ>, where σ = θ[Var(Q)], is called an admissible computed answer (a.c.a.) for that derivation.
Example 1.3 Let P be the following program and let ([0, 1],≤) be the lattice where ≤ is the usual order on real numbers.
R1 : p(X) ←prod q(X, Y) &godel r(Y ) with 0.8
R2 : q(a, Y ) ←prod s(Y ) with 0.7
R3 : q(b, Y ) ←luka r(Y ) with 0.8
R4 : r(Y ) ←with 0.7
R5 : s(b) ←with 0.9
(download)
The labels prod, godel and luka mean for Product logic, Gödel intuitionistic logic and Łukasiewicz logic, respectively. That is, [[&prod]](x, y) = x · y, [[&godel]](x, y) = min(x, y), and [[&luka]](x, y) = max(0, x + y − 1). In the following admissible derivation for the program P and the goal ← p(X) &godel r(a), we underline the selected expression in each admissible step:
<p(X) &godel r(a); id> →AS1R1
<(0.8 &prod (q(X1, Y1) &godel r(Y1))) &godel r(a); σ1> →AS1R2
<(0.8&prod ((0.7 &prod s(Y2)) &godel r(Y2))) &godel r(a); σ2> →AS2R5
<(0.8 &prod ((0.7 &prod 0.9) &godel r(b))) &godel r(a); σ3>→AS2R4
<(0.8 &prod ((0.7 &prod 0.9) &godel 0.7)) &godel r(a); σ4>→AS2R4
<(0.8 &prod ((0.7 &prod 0.9) &godel 0.7)) &godel 0.7; σ5>,
where
σ1 = {X/X1},
σ2 = {X/a, X1/a, Y1/Y2},
σ3 = {X/a, X1/a, Y1/b, Y2/b},
σ4 = {X/a, X1/a, Y1/b, Y2/b, Y3/b},
σ5 = {X/a, X1/a, Y1/b, Y2/b, Y3/b, Y4/a}.
So, since σ5[Var(Q)] = {X/a}, the a.c.a. associated to this admissible derivation is: <(0.8 &prod ((0.7 &prod 0.9) &godel 0.7)) &godel 0.7; {X/a}>.
Let us now explain the interpretive phase. If we exploit all atoms of a goal, by applying admissible steps as much as needed during the operational phase, then it becomes a formula with no atoms which can be then directly interpreted in the multi–adjoint lattice L.
Definition 2.1 [Interpretive Step] Let P be a program, Q a goal and σ a substitution. We formalize the notion of interpretive computation as a state transition system, whose transition relation →IS ⊆ (E × E) is defined as the least one satisfying: <Q[@(r1, r2)]; σ> →IS<Q[@(r1,r2)/[[@]](r1,r2)]; σ>, where [[@]] is the truth function of connective @ in the lattice <L, ≤> associated to P.
For instance, since [[&prod]](x, y) = x · y, then:
<0,8 &luka (0,7 &prod 0,9); {X/a} > →IS
<0.8 &luka 0.63 ; {X/a}>
Definition 2.2 Let P be a program and <Q; σ> an a.c.a., that is, Q is a goal not containing atoms. An interpretive derivation is a sequence <Q; σ> →∗IS <Q′; σ>. When Q′ = r ∈ L, being <L, ≤> the lattice associated to P, the state <r; σ> is called a fuzzy computed answer (f.c.a.) for that derivation.
Example 2.3 We complete the previous derivation of Example 1.3 by executing the necessary interpretive steps to obtain the final fuzzy computed answer with respect to lattice ([0, 1],≤):
<(0.8 &prod ((0.7 &prod 0.9) &prod 0.7)) &godel 0.7; {X/a}>→IS
<(0.8 &prod (0.63 &godel 0.7)) &godel 0.7; {X/a}>→IS
<(0.8 &prod 0.63) &godel 0.7; {X/a}>→IS
<0.504 &godel 0.7; {X/a}>→IS
<0.504; {X/a}>.
Then, the f.c.a for this complete derivation is the pair <0.504; {X/a}>.