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

tt = γ( true , m ) m≠ false . true
f = γ( false , m ) true . false
The program that verifies n >2 ∧ ∀ m : N .(1< m < n → n % m ≠0) can then be written ( Rule 5) as:
< prime_n > = < and , < n> 2>: P , < prime_m >: Q > where
and = γ(< n> 2>: P , < prime_m >: Q ) true . < n> 2 ∧ prime_m >
The program that verifies prime ( n ) can then be written ( Rule 6) as:
< prime > = < or , < n =0>: P , < prime_n >: Q > where
or = γ(< n= 2>: P , < prime_n >: Q ) true . < n= 2 ∨ prime_n >
Then, we can construct the program that verifies the goal , which is defined as:
goal ≡ ∃ m , k : N .( prime ( m ) ∧ prime ( k ) ∧ n = m + k )
The domain of variable m is [2 .. n -1], as stated above. The domain of k is dependent upon that of m
based on the fact that n = m + k . The goal can be transformed to the following:
goal ≡ ∃ m : M .( prime ( m ) ∧ prime ( n-m ))
The verification program can be constructed based on Rule 7 as follows:
< goal > = < t , ff , true , false , M, false , ∅: R > where
true = γ( m : M ) prime [ m ] ∧ prime [ n-m ]. true , m : R , true
false = γ( m : M ) ¬ ( prime [ m ] ∧ prime [ n-m ]). false , false
ff = γ( false , m ) x≠ true ∧ type ( m ) ≠R . false
t = γ( true , m ) type ( m ) ≠R . true
The constructed program is a semantic verification program of the given logic specification. The
essence of this method is its adaptability to be implemented as an automatic rewrite system. We can
design a parser that generates the verification program for a given logic specification. In this process,
efficiency of the target program is not taken into consideration. It is well understandable that the target
program may have a low efficiency because the verification process involves a brute force testing of
samples in the input domain. Although there are methods for improving the efficiency of the program
by reducing the size of the domain using logic properties in the domain theory (see (Lin & Chen, 1998)
for detailed descriptions), let's highlight that this method is not intended to be used in the construction
of concrete programs that directly perform computations on first-class input data. Instead, it aims to
transform the logic specifications of system architectures to operational specifications. The architectural
specifications of MASs, for example, are composed of entities in the interfaces of program modules
instead of first-class data. These entities may include the messages exchanged among program units in
a distributed network system as well as meta data used for global control of the overall system. In the
following section, we discuss the application of this method in the design of MASs.