An Expert System Devoted to Automated Music Identification and Recognition - Intelligent Music Information Systems: Tools and Methodologies - page 94

application to automated
Veriication

Definition of the basic ideal I (“ ... ” are in-
cluded for the sake of space, CoCoA requires
writing all polynomials):

From the definition of ideal in a commutative ring
with “1” above, if the polynomial “1” belongs to
the ideal, the ideal is the whole ring.
If such is the case, then any formula “α”, in
particular a contradiction, would be a tautologi-
cal consequence of the information contained in
the ES.
But checking whether or not “1” belongs to
the ideal (in this chapter's case the ideals are of
the form I + K + J), is automatic, by just typing
the command:

I:=Ideal(x[1]^2-x[1],x[2]^2-x[2],x[3]^2-x[3],...,
x[23]^2-x[23],a[1]^2-a[1],...,a[3]^2-a[3],
b[1]^2-b[1],...,b[3]^2-b[3],c[1]^2-c[1],...,
c[4]^2-c[4],d[1]^2-d[1],...,d[4]^2-d[4],
e[1]^2-e[1],...,e[3]^2-e[3],f[1]^2-f[1],...,
f[4]^2-f[4],g[1]^2-g[1],...,g[3]^2-g[3],
h[1]^2-h[1],...,h[3]^2-h[3],i[1]^2-i[1],...
i[4]^2-i[4],s[1]^2-s[1],...,s[4]^2-s[4],
t[1]^2-t[1],...,t[4]^2-t[4],v[1]^2-v[1],...,
v[4]^2-v[4],...,z[1]^2-z[1],...,z[4]^2-z[4]);

Definition of the connectives corresponding
to classic Boolean logic:

GBasis(NEG(alpha),I+K+J);

If the output is [1], the polynomial “1” belongs
to the ideal and, thus, the ideal is the whole ring.
Therefore any formulae (in particular contradic-
tory formulae) are consequence of the ES, so that
the ES would be found to be inconsistent (in an
exact automated way). This is why it was said
in the introduction to this chapter that this ES is
sound regarding its verification.

NEG(M):=NF(1+M,I);
OR1(M,N):=NF(M+N+M*N,I);
AND1(M,N):=NF(M*N,I);
IMP(M,N):=NF(1+M+M*N,I);

cocoa translation of the production
rules

As already said, he total number of rules of ES1
is 370. CoCoA requires them to be written in
“prefix form”. For instance, the three production
rules corresponding to Table 2:

cocoa ImplementatIon
WorkIng In conjunctIon
WIth the guI

We shall use Courier font for CoCoA code. We
shall intermix the final parts of the program
with screens of the user interface, in order to
make our explanations more intuitive and better
understood.
Definition of he ring A (all the two dots are
CoCoA code):

X1 ∧ X3 → A1
¬X1 ∧ X3 → A2
¬X3 → A3

are introduced as follows

R1:=NF(IMP(AND1(x[1],x[3]),a[1]),I);
R3:=NF(IMP(AND1(NEG(x[1]),x[3]),a[2]),I);
R10:=NF(IMP(NEG(x[3]),a[3]),I);

A::=Z/(2)[x[1..23],a[1..3],c[1..4],
d[1..4],e[1..3],f[1..4],g[1..3],
h[1..3],i[1..3],s[1..4],t[1..4],
v[1..4],s[1..4],t[1..4],z[1..4]];
USEA;

Similarly, the next two production rules cor-
responding to Table 3: