computed answer (abductive explanation) for abductive theory <FC,A,IC> and observation

G=Messages(X,Y) if there exists a LP computation G0... Gn such that G0=G and Gn=∆⊆A.

Definition 7 (A-correct answer): An abductive explanation or A-correct answer for a goal G

is a set ∆ of ground abducible formulae which when added to the program FC imply the goal

G and satisfy the integrity constraints in IC, ie.

FC ∪∆ |=lp G and FC ∪∆ |=lp IC

where |=lp is the underlying semantics of Logic Programming.

Theorem 3 (soundness, completeness): In an abductive theory <FC,A,IC>, FC is a logic

program that interprets evaluation of a communication protocol C, then the following holds:

Every A-computed answer is A-correct answer in <FC,A,IC> and for observation ?-

Messages(X,Y) (soundness).

Every A-correct answer is A-computed answer in <FC,A,IC> and for observation ?-

Messages(X,Y) (completeness).

Proof: Standard Abductive Logic theory [12].

Definition 8 (ADepth-computed answer): A set of instances of abducible predicates ∆ is

ADepth-computed answer (abductive explanation) for abductive theory <HC,A,IC>, HC is a

logic program, that interprets evaluation of communicating protocol C, HC=F1∪F2 ∪H3 ∪F4

16

PDF created with FinePrint pdfFactory trial version http://www.fineprint.com

reduced by constant MAX=n, n∈N, and observation G=Messages(X,Y) if there exists a LP

computation G0... Gn such that G0=G and Gn=∆⊆A.

Theorem 4(soundness, completeness): Consider FC= F1∪F2 ∪F3 ∪F4 and HC = F1∪F2 ∪H3

∪F4

1. If a set of abducible predicates ∆ is ADepth-computed answer for <HC,A,IC> and

observation ?-Messages(X,Y) then ∆ is also A-computed answer for <FC,A,IC> and

observation ?-Messages(X,Y).

2. If a set of abducible predicates ∆ is A-computed answer for <FC,A,IC> and observation ?-

Messages(X,Y) then ∆ is also ADepth-computed answer for <HC,A,IC> and observation ?-

Messages(X,Y).

Proof: Analogous as proof of theorem 2.

The computational process for deriving the abductive solution (explanation) consists of two

interleaving phases, called the abductive and consistency phases. In an abductive phase,

hypotheses on the abducible predicates are generated, by reducing the goals through model of

the problem in F, thus forming a possible solution set. A consistency phase checks whether

these hypotheses are consistent with respect to the integrity constraints. During a consistency

phase it is possible for new goals to be generated, if these are needed in order to ensure that

the hypotheses so far can indeed satisfy the integrity constraints. In turn these new goals can

generate further abducible assumptions, to be added to the solution set. It is also possible that

the consistency phase refines the solution set of assumptions generated originally “ by setting

constraints on the existential variables involved in the abducible assumptions “ when this

restriction can help ensure the satisfaction of (some of) the integrity constraints. In our case

the integrity constraints is the empty set.

3.3 Soundness and completeness DLA method

As it was said the DLA method is based on the combination of logic based data model

called datalog and abduction. We deal with abduction in previous chapter, now we will talk

about datalog. The name datalog was coined to suggest a version of Prolog suitable for

database systems. The underlying mathematical model of data for datalog is essentially that of

relational model. Predicate symbols in datalog denote relations. The classical dalalog doesn™t

allow function symbols.

3.3.1 Classical datalog

Datalog programs are built form atomic formulae, which are predicate symbols with a

list of arguments, e.g., p(A1,...,An), where p is the predicate symbol. An argument in datalog

can be either a variable or a constant.

17

PDF created with FinePrint pdfFactory trial version http://www.fineprint.com

In the logical view on databases, computing the answer to a query q from database

means to find all objects o for which formula q← o is true, detailed, such that the rule r0←

r1&...&rn is true. The usual approach to answer such queries in classical deductive databases

is following (for details see [36]):

1. rectification of rules. Instead of r0(c1,...,cn)← r1&...&rn work with the rule r0(X1,...,Xn)←

X1=c1& & Xn=cn&r1&...&rn “ means after that in the head of rule cannot be constants

only variables.

2. Having such rule and relations R1,...,Rn interpreting predicates r1,...,rn we use X1=c1& &

Xn=cn as selection condition and the body of rule is then interpreted by the join ><

(σc(R1),...,σc(Rn)) and the head is just projection to attributes of r0.

3. Multiple rectified rules r0i ← r1i ,..., rnii have the same head and hence their simultaneous

representation is union of them.

K

R0 = U (∏ X (>< (σ c ( R1i ),..., σ c ( R ni ))))

i

i =1

4. In such way we get m relational equations with m unknown relations. These m unknown

relations are intensional predicates. Extensional relations are those appearing only in

bodies. The system of equations

R0=f0(R0, R1,...,Rm)

R1=f1(R0, R1,..., Ri,...,Rm)

Rm=fm(R0, R1,...,Rm)

is solved using the smallest fixpoint of the production operator. Of cause this fixpoint

should be computable.

Definition 9 (TP operator): Operator defined by solution the system equations

R0=f0(R0, R1,...,Rm)

R1=f1(R0, R1,..., Ri,...,Rm)

Rm=fm(R0, R1,...,Rm)

is called TP operator.

Definition 10 (D-correct answer): Assume R1,...,Rn are interpretation of predicate symbols

r1,...,rn and FC is a logic program, then the relation R is a D-correct answer for R1,...,Rn and

query r if for all tuples (a1,...,an)∈R the substitution ˜={x1/a1,..., xn/an} is an L-correct answer

for the program FC extended by facts R1,...,Rn and query r0(x1,...,xn).

Definition 11 (D-computed answer): Assume I is the smallest fixpoint of the operator TP than

TP(I)(r0) is a D-computed answer.

Theorem 5 (soundness, completeness): Let P to be a datalog program, then the following

holds:

Every D-computed answer is D-correct answer for datalog program P (soundness).

Every D-correct answer is D-computed answer for datalog program P (completeness).

18

PDF created with FinePrint pdfFactory trial version http://www.fineprint.com

Proof: Standard Datalog Programming (LP) theory [36].

3.3.2 DLA “ Datalog with function symbols

In our DLA method we need to extend the classical datalog, because the classical

datalog doesn™t use the function symbols. This extension could leads to infinite relations. To

prevent this we use the function symbols only limited. The restriction in the rules with the

constant MAX and functions Depth_ is done to limited relations before infinity. The restriction

is the same as in chapter 4.1. This change means, that we change the classical datalog

production operator.

Definition 12 (DLA-computed answer): Let HC to be a extended datalog program that

interprets evaluation of a communication protocol C, the fixpoint (closure) of relation

Messages is said to be a DLA-computed answer for extended datalog program HC .

Definition 13 (DLA-correct answer): Let HC to be a extended datalog program (the same as

logic program restricted with constant MAX=n, n is positive integer) that interprets evaluation

of a communication protocol C. Assume R1,...,Rn are interpretation of predicate symbols

r1,...,rn. Then the relation R is a DLA-correct answer for R1,...,Rn and query r if for all tuples

(a1,...,an)∈R the substitution ˜={x1/a1,..., xn/an} is an LDepth-correct answer for the program

HC extended by facts R1,...,Rn and query r0(x1,...,xn).

Theorem 6 (soundness, completeness): Let HC to be a logic program that interprets

evaluation of a communication protocol C (HC has a function symbols and is restricted with

constant MAX=n, n is positive integer), then the following holds:

Every DLA-computed answer is DLA-correct answer for extended datalog program HC