The problem of a machine search for a proof is that the branching factor is enormous. Use an aggressive heuristic for "neat" proofs only. The proof system is no longer complete, but that's OK, we don't like ugly proofs anyway.
The heuristic may be learned by giving examples of human-generated "neat" proofs.
No comments :
Post a Comment