Hilbert System - Automate Proof

Viewed 5508

I'm trying to prove the statement ~(a->~b) => a in a Hilbert style system. Unfortunately it seems like it is impossible to come up with a general algorithm to find a proof, but I'm looking for a brute force type strategy. Any ideas on how to attack this are welcome.

6 Answers
Related