Examples

Verification of visible equivalence

To appear.

Verification of strong equivalence

To appear.

Verification of weak equivalence for disjunctive programs

To appear

Verification of modular equivalence

Consider programs P and Q consisting of modules P1, P2, Q1, Q2. The encodings of the modules in the input language of lparse are as follows:

	p1.lp:	#external a,b.		p2.lp:	#external b.
		c :- not a.			a :- b.
	q1.lp:	#external a,b.		q2.lp:	#external a.
		c :- not b.			b :- a.

Declaration #external is used to tell lparse which atoms are not defined inside the module. This declaration does not match exactly what we would like the declaration of input atoms to be, but currently there is no direct support for declaring input atoms in lparse. Information hiding, however, can be obtained using #hide declaration. For more details see the user's manual of lparse.

lparse can be used to obtain the presentation of the modules in the internal format of smodels which is also the input format for lpeq and lpcat. For example, in the case of module P1:

$ lparse p1.lp > p1.sm
3: Warning: predicate 'a/0' doesn't occur in any rule head.
$ more p1.sm
1 2 1 1 3
0
2 c
3 a
0
B+
0
B-
1
0
1


Since lparse is designed for programs with a completely specified input, there is a warning message. Notice also that since atom b does not occur in the rules of P1 it does not appear in the symbol table of p1.sm. It is possible to add b to the symbol table by, for example, inserting a line "4 b" to the symbol table in p1.sm. Files p2.sm, q1.sm and q2.sm can be obtained similarly from files p2.lp, q1.lp and q2.lp, respectively.

lpcat computes the join of two modules with flag -m. For example, the composition P1 ⊕ P2 is obtained as follows.

$ lpcat -m p1.sm p2.sm > p1-p2.sm

The composition q2-p2.sm can be obtained similarly.

Now, we are ready to use lpeq to verify the equivalence of P and Q. First, we can verify the equivalence without taking into account our knowledge about the modular structure using the following commands.

$ lpeq p1-p2.sm q1-q2.sm | smodels 1
$ lpeq q1-q2.sm p1-p2.sm | smodels 1

The modular approach to equivalence verification goes as follows. In the first step one computes the translation EQT(P1,Q1) using lpeq with flag -m. The context module P2 is added using the tool lpcat with flag -m and smodels is used to see if the translation EQT(P1,Q1)⊕ P2 has stable models.

$ lpeq -m p1.sm q1.sm | lpcat -m - p2.sm | smodels 1

$ lpeq -m q1.sm p1.sm | lpcat -m - p2.sm | smodels 1

Since neither translation has stable models we learn that P1 ⊕ P2 is modularly equivalent to Q1 ⊕ P2. The second equivalence in the chain, that is, the equivalence of Q1 ⊕ P2 and Q1 ⊕ Q2, is verified similarly:

$ lpeq -m p2.sm q2.sm | lpcat -m - q1.sm | smodels 1
$ lpeq -m q2.sm p2.sm | lpcat -m - q1.sm | smodels 1

$ lpeq -m -i p1.sm q1.sm | smodels 1
smodels version 2.32. Reading...done
Answer: 1
Stable Model: a c'
True
Duration: 0.002
Number of choice points: 1
Number of wrong choices: 0
Number of atoms: 9
Number of rules: 8
Number of picked atoms: 3
Number of forced atoms: 0
Number of truth assignments: 13
Size of searchspace (removed): 2 (2)


The stable model {a,c'} for translation EQT(P1,Q1) gives us a counterexample for the modular equivalence of P1 and Q1: {a} is a stable model of P1 and {a,c} is the least model of Q1 with respect to the input {a}.