Automated Paraconsistent Reasoning via Model Checking

Abstract

Inconsistency is a pervasive problem in software engineering, where different aspects of a system are described in separate models. Resolving all the inconsistencies in a large set of models is often infeasible, in which case automated reasoning tools based on classical logic have limited application. In this paper we describe an automated tool for paraconsistent reasoning, using multi-valued logics. The reasoning engine is an adaptation of classical model checking, and works for any multi-valued logic whose truth values form a quasi-boolean lattice. We describe the design of the model checker, and show how it can be used to reason about models created by merging information from multiple conflicting sources.