Bibel´s matrix connection method in paraconsistent logic: general concepts and implementation

Bibel´s matrix connection method is an alternative to resolution for the mechanized proof of logical statements. Bibel´s method was originally defined for classical logic. In this work, an adaptation of the method for annotated propositional logic is given, followed by a simple case study. Some implementation details are also presented