Verification of Knowledge Based Systems with Commutative Algebra and Computer Algebra Techniques

Eugenio Roanes-Lozano ^{∗}  Luis M. Laita ^{†}

* Dept. Algebra, Universidad Complutense de Madrid † Dept. Artificial Intelligence, Universidad Politécnica de Madrid

Keywords: Verification of KBSs, Boolean Algebras, Ideals, Applications of Computer Algebra Systems

Abstract

In a previous paper [LR1], given a propositional Boolean algebra, an isomorphic polynomial Boolean algebra A, that is also a k-algebra, was constructed. Ideals and filters were principal, and preserved by this isomorphism. Moreover, the ideals of the polynomial Boolean algebra are the same as those of the polynomial k-algebra.

Later, this construct was used to build an algebraic model of Knowledge Based Systems (KBSs) based on bivalent logic [LR3]. To do so it is enough to consider the natural epimorphism onto A/J, where J is the ideal generated by the polynomial images of the negation of the rules, facts and constraints of the KBS.

With this modelization, the forward reasoning inconsistency of a given KBS can be interpreted as the degeneracy of the polynomial residual class ring A/J into {0} (i.e., J =<1>).

An implementation in a Computer Algebra System (Maple V) has been developed.

∗eroanes@fi.upm.es

†laita@fi.upm.es Partially supported by DGICYT of Spain

1 Introduction

When a Knowledge Based System (KBS), usually known as Expert System, is constructed, the expert (a human) gives a list of rules, facts and constraints. The knowledge of the expert would be supposed not to lead to any contradiction. Nevertheless, structural problems actually appear in most KBSs. Therefore much attention has been paid lately to check the reliability of the KBSs, because safety is the main goal in some applications, as clinical practice guidelines (diagnosis in Medicine) and decision taking in nuclear power-stations. The celebration of more than 20 international conferences and workshops on this topic since 1988 testify its importance.

Checking the forward reasoning consistency of a KBS is a very hard and still not completely closed problem. Usually the KBS is broken into small pieces (that look independent) and they are manually checked using diagrams. Other techniques use random checking and Petri-nets checking.

In our approach we give an interpretation of forward reasoning consistency using ideals of Boolean algebras. Then we construct an isomorphic polynomial K-algebra and use elementary techniques from Theory of Ideals (now ideals of a polynomial ring) to check the logic consistency of the knowledge of the expert (in an exhaustive way).

Although the ideal membership problem is involved, due to the kind of polynomial rings involved, Gröbner Basis are not used.

2 Implementation in Maple V

If the propositional variables of the propositional Boolean algebra are P, Q, ..., R, the class ring A is (ZZ/2ZZ)[p, q, ..., r]/ < p^{2} − p, q^{2} − q, ..., r^{2} − r > . To move from the polynomial ring (ZZ/2ZZ)[p, q, ..., r] to the class ring A can be implemented using Maple’s command convert( ,mod2) (from the point of view of simplification, it is enough to reduce modulus 2 both coefficients and powers).

Logical operators can be implemented very easily as &or, &and and &neg just taking into account the corresponding arithmetic definitions. For example:

> ’&or’:=proc(alfa,beta)

> convert(expand(alfa+beta+alfa*beta),mod2); > end;

The procedure baseideal, that returns the generator element of any given ideal (let us remember that all ideals are principal ones), is also very easy to implement in Maple V.

> baseideal:=proc(S : list) > local i,gen; > gen := 0; > for i to nops(S) do gen := convert(expand(gen &or op(i,S)),mod2) od; > gen; > end;

The implementation of the criteria just checks if the generator element of J is equal to 1 or not.

3 Complexity

As we say above, the problem is very hard: double-exponential space consuming (with respect to the number of variables or rules) in the worse case (with our approach).

Let us observe that, if the Boolean algebra has n propositional variables, then it has 2^{n} atoms and 2^{(2^{n})} elements.

Anyway the implementation can handle KBSs (such that the ideal J is generated by polynomials not involving many different propositional variables) in a 486-PC.

4 Final Remark

We think that this is a very innovative approach in the use of elementary techniques that are of common usage in Algebraic Geometry and in Computer Algebra to an important problem of Artificial Intelligence. Curiously, handling Boolean interpretations of propositional Boolean rings is more frequent in the work of the pioneers of Logic than in modern approaches. CA techniques have made possible to use in real problems certain known results that were almost curiosities, because they were too laborious (Sturm’s Theorem, Wu’s pseudoremainder method,...). We think that, in a similar way, nowadays CAS can produce a revival of polynomial approaches to certain problems in Logic.

Literature

[dA] A. de Antonio: Una interpretación algebraica de la verificación de sistemas basados en el conocimiento. Doctoral Dissertation (Directors: L. M. Laita and A. Pérez). Universidad Politécnica de Madrid, 1994.

[C1] B.W. Char et al.: Maple V Language Reference Manual. Springer-Verlag, 1991.

[C2] B.W. Char et al.: Maple V Library Reference Manual. Springer-Verlag, 1991.

[C3] B.W. Char et al.: First Leaves: A Tutorial Introduction to Maple. Springer-Verlag, 1991.

[GC] K.O. Geddes, S.R. Czapor, G. Labahn: Algorithms for Computer Algebra. Kluwer Academic Pub., 1992.

[Ha] P.R. Halmos: Lectures on Boolean Algebras. Springer-Verlag, 1974.

[He] A. Heck: Introduction to Maple. Springer-Verlag, 1993.

[Hr] H. Hermes: La teoría de retículos y su aplicación a la lógica matemática. Conf. Mat. VI. CSIC-Madrid, 1963.

[LR1] L. M. Laita, L. de Ledesma, E. Roanes L., E . Roanes M.: An Interpretation of the Propositional Boolean Algebra as a k-algebra. Effective Calculus. In: J. Campbell, J. Calmet (editors): Proceedings of the Second International Workshop/Conference on Artificial Intelligence and Symbolic Mathematical Computing (AISMC-2). Lecture Notes in Computer Science. Springer-Verlag. To appear.

[LR2] E. Roanes L., L. M. Laita: Verification of Knowledge Based Systems: An Algebraic Interpretation. Effective calculus. Preprint.

[LR3] E. Roanes L., L. M. Laita, E . Roanes M.: Maple V in A.I.: The Boolean Algebra Associated to a KBS. Computer Algebra Nederland, Nieuwsbrief 14, abril 1995 (pp. 65-70).

[LC] L. M. Laita, J. Couto, L. de Ledesma, A. Fernández-Margarit: Formal Model for Knowledge-Based System Verification. International Journal of Intelligent Systems, vol. 9,9, 1994 (pp. 769-786).

[Mo] D. Monk: Handbook of Boolean Algebras. North-Holland, 1989.

[MNG] A. Montes, M. Noguera, A. Grau: Apuntes de Maple V. Universitat Politècnica de Catalunya, 1994.