Multivalued logics: a uniform approach to reasoning in artificial intelligence

Publisher Website
Google Scholar
Abstract
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 abilattice.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.

This publication has 27 references indexed in Scilit: