Comment by bubblyworld

Not Gödel's theorem, but inference for first-order logic is undecidable in general for other reasons. You can still get pretty far with heuristics though. Don't let perfect be the enemy of good =P