Looking at Cohen's success at proving independence of the Axiom of Choice and the Continuum Hypothesis, I was wondering if it was possible to mechanize forcing techniques for the purpose of proving independence (and hence undecidability) of conjectures. It would seem to be useful to test any sentence you're trying to prove or disprove with an automated theorem prover for independence. I'm imagining some automated forcing technique that constructs a model of ZFC plus the conjecture and its negation to prove it isn't a theorem of ZFC (or whatever foundation being used) rather than spinning forever on an undecidable statement, since the incompleteness theorems indicate that any statement in a sufficiently strong formal system can be undecidable.
Its not obvious to me how to automate such a method, as its probably quite a bit more complicated than just implementing resolution, but it would be nice to have automated reasoning go down three paths of searching for proof of a conjecture, proof of its negation, and proof of its independence.
Forcing is not easy to automate. A typical forcing argument requires at the very least a clever choice of the sequence of dense sets that the generic filter will meet. Unless you program a special heuristic into the search, how would it know which dense sets to consider?
In many cases there is even more work to do. For example, in the modern treatment of Cohen's proof of the independence of CH there is the concept of a ccc forcing and the proof that ccc forcings do not collapse cardinals. It would not be straightforward to automate the discovery of that sort of proof - it is not obvious how to narrow the search space for the proof in the right way.