The axiom schemas are countable, which is small enough for the procedure described in the grandparent to work. Unless I’m not understanding something?
The size of the search space and lack of any reasonable heuristic.
The axiom schemas are countable, which is small enough for the procedure described in the grandparent to work. Unless I’m not understanding something?
The size of the search space and lack of any reasonable heuristic.