Tjark Weber. In 2nd International Joint Conference on Automated Reasoning (IJCAR 2004) Workshop W1: Workshop on Disproving - Non-Theorems, Non-Validity, Non-Provability, Cork, Ireland, July 2004.
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{weber04bounded,
author = {Tjark Weber},
title = {Bounded Model Generation for {Isabelle/HOL}},
booktitle = {2nd International Joint Conference on Automated Reasoning (IJCAR 2004) Workshop W1: Workshop on Disproving -- Non-Theorems, Non-Validity, Non-Provability},
address = {Cork, Ireland},
month = jul,
year = {2004}
}
A revised version of this paper is available.