Tjark Weber. In Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, and Cesare Tinelli, editors, Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR 2004), volume 125(3) of Electronic Notes in Theoretical Computer Science, pages 103-116. Elsevier, July 2005.
A translation from higher-order logic (on top of the simply typed $\lambda$-calculus) to propositional logic is presented, such that the resulting propositional formula is satisfiable iff the HOL formula has a model of a given finite size. A standard SAT solver can then be used to search for a satisfying assigment, and such an assignment can be transformed back into a model for the HOL formula. The algorithm has been implemented in the interactive theorem prover Isabelle/HOL, where it is used to automatically generate countermodels for non-theorems.
@inproceedings{weber05bounded,
author = {Tjark Weber},
title = {Bounded Model Generation for {Isabelle/HOL}},
editor = {Wolfgang Ahrendt and Peter Baumgartner and Hans de Nivelle and Silvio Ranise and Cesare Tinelli},
booktitle = {Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR 2004)},
volume = {125(3)},
series = {Electronic Notes in Theoretical Computer Science},
pages = {103--116},
publisher = {Elsevier},
month = jul,
year = {2005},
url = {http://dx.doi.org/10.1016/j.entcs.2004.10.027}
}