Una interpretación algebraica de la verificación de sistemas basados en el conocimiento

Resumen Garantizar la calidad de un Sistema Basado en el Conocimiento es un objetivo prioritario en el proceso de desarrollo de este tipo de sistemas. Por ello, durante los últimos quince años, se ha venido trabajando en una nueva disciplina a la que se ha dado en llamar Validación, y cuyo objetivo es asegurar la calidad de un Sistema Basado en el Conocimiento, entendiendo el término calidad en un sentido muy amplio, que abarca desde la satisfacción de las necesidades del usuario hasta la precisión o credibilidad de los resultados obtenidos por el sistema. Esta disciplina ha evolucionado enormemente durante los últimos años, aunque aún no se puede decir que haya alcanzado madurez y estabilidad. De hecho, en un estudio reciente [Nazareth,1993] fue clasificada como una materia en estado de formalización. Una muestra significativa de esta inmadurez es la inexistencia de una terminología comúnmente aceptada por los investigadores del área. El trabajo que aquí se presenta se puede considerar un avance en el proceso de formalización de esta disciplina. Se centra en un aspecto de la Validación, comúnmente denominado Verificación, que tiene que ver con la comprobación del cumplimiento, por parte del sistema, de una serie de especificaciones formales. Una de las propiedades más importantes y críticas que el proceso de Verificación debe garantizar es la consistencia de la base de conocimientos del sistema. Con este trabajo se ha pretendido dar un soporte formal al proceso de Verificación y, para ello, se ha recurrido a la Matemática y, más concretamente, al Álgebra. Se han reformulado adecuadamente los conceptos propios de la Lógica Algebraica haciendo posible su aplicación en la representación de Sistemas Basados en el Conocimiento. Se ha construido un modelo formal que, no sólo permite expresar el conocimiento contenido en la base y su evolución durante el razonamiento del sistema, sino también expresar formalmente las propiedades deseadas y analizar su cumplimiento. Se ha conseguido, de esta forma, una interpretación algebraica del concepto de consistencia de una base de conocimientos que ha conducido, a su vez, a la formulación de un método de detección de inconsistencias, al que se ha llamado MÁDISON. Dicho método es capaz de detectar cualquier tipo de contradicción, tanto las lógicas como las derivadas de incompatibilidades semánticas. El estudio se ha centrado en los sistemas basados en reglas con lógica proposicional como lógica subyacente, aunque esto no resta generalidad a los resultados alcanzados, puesto que se ha desarrollado también un método que permite reducir al caso proposicional el problema de la detección de inconsistencias en lógica de predicados. Se han superado limitaciones y restricciones impuestas por otros métodos de Verificación existentes hasta la fecha. En este sentido cabe destacar que se han contemplado los Sistemas Basados en el Conocimiento que razonan con conocimiento disyuntivo, y que el método es capaz de aceptar la adición dinámica de reglas a la base de conocimientos. Abstract A priority objective in the Knowledge-Based System development process is quality assurance. Thus, over the past fifteen years, work has been going on in a new discipline, known as Validation, the objective of which is to ensure the Knowledge-Based System quality, the term quality being understood in a very broad sense, ranging from the satisfaction of user needs to the accuracy or credibility of the results produced by the system. Enormous progress has been made in this field over recent years, although it still cannot be said to have reached maturity or stability. Indeed, it was classed in a recent study (Nazareth, 1993) as an issue in the process of formalization. A major sign of such immaturity is the absence of terminology widely accepted among the researchers in the área. The thesis presented here can be considered as an advance in the process of formalizing this discipline. It centres on one aspect of Validation, usually referred to as Verification, which is related with establishing whether the system meets a series of formal specifications. One of the most important and critical properties to be guaranteed by the Verification process is the consistency of the system's knowledge base. This thesis seeks to provide a formal support for the Verification process on the basis of Mathematics and, more specifically, Algebra. Concepts proper to Algebraic Logic have been suitably reformulated to make them applicable to Knowledge-Based System representation. A formal model has been constructed which provides both for expression of knowledge contained in the base and its evolution as the system reasons and for formal expression of the desired properties and analysis of their achievement. In this manner, an algebraic interpretation of the concept of knowledge-base consistency has been produced, which has led, in turn, to the formulation of a inconsistency detection method, called MADISON. This method is able to detect any kind of contradiction, logical as well as those derived from semantical incompatibilities. The research centred on rule-based systems with propositional calculus as the underlying logic. This does not, however, detract from the generality of the results obtained, as another method has been developed to reduce the problem of inconsistency detection in predícate calculus to propositional calculus terms. It has been possible to overeóme some restrictions and constraints imposed by other Verification methods. In this respect, it is important to note that the possibility of handling disjunctive knowledge and dynamic rule addition has also been accounted for