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.