Designing Multi-Agent Systems from Logic Specifications - Distributed Artificial Intelligence, Agent Technology, and Collaborative Applications - page 12

Similarly, < goal 1> can be constructed as:
< goal 1[ l ]> = < t , ff , true , false , MT , false , ∅: R > where
true = γ( n:MT )< MT [ l , n ]>=< true >. true , n : R , true
false = γ( n:MT ) < MT[l, [ l , n ]>=< false >. false , false
ff = γ( false , n ) n≠ true ∧ type ( n ) ≠R . false
t = γ( true , n ) type ( n ) ≠R . true
Because the input l in < goal 1[ l ]> is computed using expression:
extract , fail , result , < goal 0 >
the verification program should be:
<goal 1 [ extract , fail , result , < goal 0 [ u ]>]> = < t , ff , true , false , MT , false , ∅: R > where
Let l = extract , fail , result , < goal 0 [ u ]>
true = γ( n:MT )< MT [ l , n ]>=< true >. true , n : R , true
false = γ( n:MT ) < MT[l, [ l , n ]>=< false >. false , false
ff = γ( false , n ) n≠ true ∧ type ( n ) ≠R . false
t = γ( true , n ) type ( n ) ≠R . true
With similar reasoning, we can construct:
<goal 2 [ extract , fail , result , < goal 1 [ l ]>]> = < t , ff , true , false , EM , false , ∅: R > where
Let n = extract , fail , result , < goal 1 [ l ]>
true = γ( e:EM )< NT [ n , e ]>=< true >. true , e : R , true
false = γ( e:EM ) < NT [ n , e ]>=< false >. false , false
ff = γ( false , e ) e≠ true ∧ type ( e ) ≠R . false
t = γ( true , e ) type ( e ) ≠R . true
To construct the program for
goal ≡ ∃ e : EM . ∀ s : DT . ST ( e , s )
we firstly construct the program for
∀ s : DT . ST ( e , s )
Using Rule 1, we get:
< goal' [ e ]> = < f, tt , true , false , DT, true > where
true = γ( s : DT )< ST [ e, s ]>=< true >. true , true
false = γ( s : DT ) <ST [ e, s ]>=< false >. false , false
tt = γ( true , s ) s≠ false . true