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 …