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

Rule 6. For clause r = p ∨ q , < r > = < or , < p >: P , < q >: Q > where
or = γ(< p >: P , < q >: Q ) true . < p ∨ q >
Rule 7. For the goal = ∃ z : T z . Q ( a , z ), < goal > = < t , ff , true , false , T z , false , ∅: R > where
true = γ( z : T z )< Q [ a , z ]>=< true >. true , z : R , true
false = γ( z : T z ) <Q [ a , z ]>=< false >. false , false
ff = γ( false , z ) x≠ true ∧ type ( z ) ≠R . false
t = γ( true , z ) type ( z ) ≠R . true
where type ( z ) determines the type of element z .
Rule 1 generates a program that verifies a universally quantified clause. It tests the values in domain
N and replaces the values by either true or false according to the results of the verification. This is done
by two sub-programs true and false . Program tt then removes redundant true 's and f removes everything
including redundant false 's. However, a false cannot be removed by a true . This is because that once
there is a value that causes p ( x ) to be evaluated to false , ∀ x : N . p ( x ) is false . Note that p [ x ] denotes the
molecule obtained by replacing the hole by x . The true in the initial solution < f, tt , true , false , N, true >
ensures that there is at least a true in the multiset if N = ∅. When the solution < q > becomes inert, it
should be either < true > or < false >.
Similarly, Rule 2 generates a program that verifies an existentially quantified clause. Program ff
removes redundant false 's and t removes everything including redundant true 's. However, a true can-
not be removed by a false . This is because that once there is a value that causes p ( x ) to be evaluated to
true , ∃ x : N . p ( x ) is true . The false in the initial solution < t, ff , true , false , N, false > ensures that there is
at least a false in the multiset if N = ∅. Also, when the solution < q > becomes inert, it should be either
< true > or < false >.
Rule 3-6 generate programs that verify clauses based on the results of the sub-programs that verify
the sub-clauses.
Rule 7 is similar to Rule 2. However, since it generates the program in the top level of the nesting
hierarchy of the program tree, it should return the result that satisfies the goal . To this end, a multiset
R (initially set to ∅) is added into the solution to store the values in T z that satisfy Q ( a , z ). When sub-
program true finds a value that satisfies Q ( a , z ), it stores the values in R . ff and t are modified to keep
values in R . The final result of the program, viz., the inert solution < goal >, should be either < true , R >
and R ≠ ∅; or < false , ∅>. The latter indicates that the no results are found that meet the goal .
As an example, let's construct the program that verifies the Goldbach Conjecture (Richstein, 2001).
Firstly, let's construct the program that verifies predicate prime ( n ), which is defined as:
prime ( n ) ≡ n =2 ∨ n >2 ∧ ∀ m : N .(1< m < n → n % m ≠0)
Based on clause 1< m < n , the bounds of domain N is 2 (lower bound) and n -1 (upper bound). Let M
= [2 .. n -1], the clause ∀ m : N .(1< m < n → n % m ≠0) can be transformed to ∀ m : M . n % m ≠0. The program
that verifies ∀ m : M . n % m ≠0 can then be written (based on Rule 1) as:
< prime_m > = < f, tt , true , false , N, true > where
true = γ( m : M ) n % m ≠0. true , true
false = γ( m : M ) n % m =0. false , false