Finite algebraic models for residuated logic

Using finite models to direct the search of an automated theorem prover (through the strategy known as model pruning) can significantly improve the efficiency of theorem provers, which, for nonclassical logics, often suffer from combinatorial explosions. Finding models of size n>4 is itself a difficult problem, as the number of possibilities to check rapidly becomes enormous as n increases. The paper is intended as a tutorial style introduction to algebraic semantics and the problems of finding finite models. We describe an algorithm we have developed to find the finite algebraic models for residuated logic, and present results of the search (for up to n=7); we present some structure theorems for residuated algebras; finally, we discuss the strategy we are working on to find models for n>7.