Abstract
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.