Logical matrices are generalisations of truth-tables. They provide powerful computational tools for dealing with inference systems. A matrix in which all of the axioms and rules of a theory are true (or designated) but in which some query statement is false (or undesignated) shows that the query statement cannot be derived from the given theory. In this paper we discuss the use of matrices in logical research and in automated theorem-proving, and we conjecture further uses in the area of general constraint satisfaction. The computational ease of use of matrices is partly overshadowed by the computational difficulty of selecting the best or even a suitable matrix for a given task. Little is known about the relative efficiency of various matrices. We discuss our implementation of a general matrix generate and test algorithm which is designed to assist with research into these questions.