In the past ten years a wide variety of proof tools, interactive or automated, has overwhelmed the union (intersection?) of mathematicians, logicians, computer scientists and industry. All promote their advantages, some mention the shortcomings. This all makes it very difficult to choose the right theorem prover.

The choice can be guided by overviews of existing theorem provers[1] or by the experience of colleagues, but in any case, once you have decided, you have to go for it and take the consequences.

We will describe that process from our experience with a three-valued logic, the Partial Predicate Logic[2], and the theorem prover Isabelle[3].

[1] P.A. Lindsay, A survey of mechanical support for formal reasoning Software Engineering Journal, January 1988.
[2] A. Hoogewijs, Partial Predicate Logic in Computer Science Acta Informatica 24, pp.381-393, Springer-Verlag, 1987.
[3] L. Paulson, Isabelle - A Generic Theorem Prover Lecture Notes in Computer Science, Springer-Verlag, 1994.