Matrix proof method in annotated paraconsistent logic

Abstract

The matrix connection method (MCM) is an alternative procedure for theorem proving than the usual resolution technique. We already have used the MCM for finding models in a real-time knowledge-based system generator. In this paper, we adapt the MCM to the particular case of sorne annotated propositional paraconsistent logics. Further developments related to these ideas are also outlined.