Multivalued logics: a uniform approach to reasoning in artificial intelligence

This paper describes a uniform formalization of much of the current work in artificial intelligence on inference systems. We show that many of these systems, including first-order theorem provers, assumption-based truth maintenance systems (atmss), and unimplemented formal systems such as default logic or circumscription, can be subsumed under a single general framework. We begin by defining this framework, which is based on a mathematical structure known as a bilattice. We present a formal definition of inference using this structure and show that this definition generalizes work involving atmss and some simple nonmonotonic logics. Following the theoretical description, we describe a constructive approach to inference in this setting; the resulting generalization of both conventional inference and atmss is achieved without incurring any substantial computational overhead. We show that our approach can also be used to implement a default reasoner, and discuss a combination of default and atms methods that enables us to formally describe an “incremental” default reasoning system. This incremental system does not need to perform consistency checks before drawing tentative conclusions, but can instead adjust its beliefs when a default premise or conclusion is overturned in the face of convincing contradictory evidence. The system is therefore much more computationally viable than earlier approaches. Finally, we discuss the implementation of our ideas. We begin by considering general issues that need to be addressed when implementing a multivalued approach such as that we are proposing, and then turn to specific examples showing the results of an existing implementation. This single implementation is used to solve a digital simulation task using first-order logic, a diagnostic task using atmss as suggested by de Kleer and Williams, a problem in default reasoning as in Reiter's default logic or McCarthy's circumscription, and to solve the same problem more efficiently by combining default methods with justification information. All of these applications use the same general-purpose bilattice theorem prover and differ only in the choice of bilattice being considered. Le present article decrit la formalisation uniforme d'une grande partie du travail courant dans le domain des systemes d'inference. L'article montre que bon nombre de ces systemes, dont les demonstrateurs de theoreme de premier ordre, les systemes de verites logiques basees sur des hypotheses (ATMS) et les systemes formels qui ne sont pas mis en oeuvre, telle la logique implicite et la circonscription, peuvent ětre subsumes dans un seul cadre general. Nous commencons par definir ce cadre, qui est base sur une structure mathematique appelee treillis bidimensionnel. Nous donnons ensuite une definition formelle de l'inference en utilisant cette structure, et montrons que cette definition generalise le travail mettant. en jeu les ATMS et une certaine forme de logique non monotone. Nous poursuivons, apres cette description theorique, par la presentation d'une approche constructive de l'inference vue dans ce cadre; il en resulte une generalisation a la fois de l'inference conventionnelle et des ATMS, qui s'obtient sans necessiter aucun temps systeme substantiel. Nous montrons que notre methode peut egalement servir a mettre en oeuvre un systeme de raisonnement implicite et discutons de la combinaison de methodes implicites et basees sur les ATMS, qui nous permet de faire la description formelle d'un systeme de raisonnement implicite et incrementiel. Ce systeme incrementiel n'a pas besoin d'effectuer des verifications de coherence avant de tirer des conclusions preliminaires; il peut, au lieu de cela, adapter ses croyances lorsque des premisses ou des conclusions implicites sont renversees en depit d'une evidence constradictoire persuasive. De ce fait, ce systeme est, du point de vue informatique, bien plus viable que les premieres methodes. Enfin, nous discutons de la mise en oeuvre de nos idees. Nous presentons d'abord les questions qu'il faut analyser lorsque l'on veut mettre en oeuvre une methode multivaluee, comme celle que nous proposons, puis nous passons a des exemples specifiques qui montrent les resultats d'une mise en oeuvre existante. Celle-ci sert a resoudre une tache de simulation numerique ayant recours a la logique de premier ordre, un tache de diagnostic ayant recours aux ATMS, tel que propose par de Kleer et Williams, un probleme de raisonnement implicite tel qu'en comportent la logique implicite de Reiter et la circonscription de McCarthy, et a resoudre ce měme probleme de facon plus efficace en combinant les methodes implicites avec des donnees justificatives. Toutes ces applications font appel au měme demonstrateur universel de theoreme de treillis bidimensionnel et ne different que par le choix de du treillis bidimensionnel etudie.